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

Also available in: Atom PDF