Project

General

Profile

Actions
Copy link

Bug #5218

open

Wrong result in ECA with global vars for Problem01_label38_false-unreach-call.c

Added by Sepideh Asadi over 7 years ago. Updated over 7 years ago.

Status:
Feedback
Priority:
Normal
Assignee:
Antti Hyvärinen
Start date:
28/05/2017
Due date:
% Done:

80%

Estimated time:

Description

/hifrog/trunk/cprover/src/funfrog/hifrog --claim 1 --bitwidth 32 --unwind 10 --no-itp ~/hi-bench/challenge-bench/sv-comp16/c/eca-rers2012/Problem01_label38_false-unreach-call.c --logic prop
result with prop: UNSAT, 54 sec
--------------------------------------------------------

/hifrog/trunk/cprover/src/funfrog/hifrog --claim 1 --bitwidth 32 --unwind 10 --no-itp ~/hi-bench/challenge-bench/sv-comp16/c/eca-rers2012/Problem01_label38_false-unreach-call.c --theoref
Result with CUF: UNSAT, 27 sec

--------------------------------------------------------
./cbmc --unwind 10
Result with CBMC: SAT , 20 sec

cbmc log:
91898 variables, 294206 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 8.099s

  • Results:
    [calculate_output.assertion.1] : FAILURE
  • 1 of 1 failed (1 iteration)
    VERIFICATION FAILED
    Command exited with non-zero status 10
    real 20.52
Actions
Copy link
 #1

Updated by Karine Even Mendoza over 7 years ago

  • Assignee set to Karine Even Mendoza
Actions
Copy link
 #2

Updated by Karine Even Mendoza over 7 years ago

  • % Done changed from 0 to 50

Prop version is SAT now.

Actions
Copy link
 #3

Updated by Karine Even Mendoza over 7 years ago

  • % Done changed from 50 to 80

The theoref version - killed

Actions
Copy link
 #4

Updated by Karine Even Mendoza over 7 years ago

  • Status changed from New to Feedback
  • Assignee changed from Karine Even Mendoza to Antti Hyvärinen

Seems to be OK now. But it is a good candidate for theoref new heuristics.
Theoref - killed.

=====
ASSERTION DON'T HOLD
A real bug found

VERIFICATION FAILED
Initial unwinding bound: 10
Total number of steps: 1
TOTAL TIME FOR CHECKING THIS CLAIM: 81.555

Main Checked Assertion:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/eca-rers2012/Problem01_label38_false-unreach-call.c line 422 function calculate_output
assertion
FALSE
; -------------------------
; STATISTICS FOR SAT SOLVER
; -------------------------
; Restarts.................: 17
; Conflicts................: 3587
; Decisions................: 12005
; Propagations.............: 38193667
; Conflict literals........: 178550
; T-Lemmata learnt.........: 0
; T-Lemmata perm learnt....: 0
; Conflicts learnt.........: 3587
; T-conflicts learnt.......: 0
; Average learnts size.....: 49.7418
; Top level literals.......: 6686
; Search time..............: 0 s
; TSolvers time............: 0.02 s
; Init clauses.............: 603447
; Variables................: 127354
; -------------------------
; STATISTICS FOR EUF SOLVER
; -------------------------
; Satisfiable calls........: 0
; Unsatisfiable calls......: 0
; egraph time..............: 0 s
; backtrack time...........: 0 s
; explain time.............: 0 s
; # eq classes at the end..: 0
; -------------------------
; STATISTICS FOR LOGICS
; -------------------------
; Substitutions............: 0
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog$ ./hifrog --claim 1 --logic prop --unwind 10 ../../../../../../hi-bench/challenge-bench/sv-comp16/c/eca-rers2012/Problem01_label38_false-unreach-call.c

Actions
Copy link

Also available in: Atom PDF