https://scm.ti-edu.ch/https://scm.ti-edu.ch/favicon.ico?15601711372017-05-30T21:48:14ZUSI & SUPSI Source Code Management (SCM)hifrog - Bug #5218: Wrong result in ECA with global vars for Problem01_label38_false-unreach-call.chttps://scm.ti-edu.ch/issues/5218?journal_id=178362017-05-30T21:48:14ZKarine Even Mendozakarine.even_mendoza@kcl.ac.uk
<ul><li><strong>Assignee</strong> set to <i>Karine Even Mendoza</i></li></ul> hifrog - Bug #5218: Wrong result in ECA with global vars for Problem01_label38_false-unreach-call.chttps://scm.ti-edu.ch/issues/5218?journal_id=179402017-06-07T13:22:31ZKarine Even Mendozakarine.even_mendoza@kcl.ac.uk
<ul><li><strong>% Done</strong> changed from <i>0</i> to <i>50</i></li></ul><p>Prop version is SAT now.</p> hifrog - Bug #5218: Wrong result in ECA with global vars for Problem01_label38_false-unreach-call.chttps://scm.ti-edu.ch/issues/5218?journal_id=179412017-06-07T13:55:14ZKarine Even Mendozakarine.even_mendoza@kcl.ac.uk
<ul><li><strong>% Done</strong> changed from <i>50</i> to <i>80</i></li></ul><p>The theoref version - killed</p> hifrog - Bug #5218: Wrong result in ECA with global vars for Problem01_label38_false-unreach-call.chttps://scm.ti-edu.ch/issues/5218?journal_id=186262017-08-08T14:48:50ZKarine Even Mendozakarine.even_mendoza@kcl.ac.uk
<ul><li><strong>Status</strong> changed from <i>New</i> to <i>Feedback</i></li><li><strong>Assignee</strong> changed from <i>Karine Even Mendoza</i> to <i>Antti Hyvärinen</i></li></ul><p>Seems to be OK now. But it is a good candidate for theoref new heuristics.<br />Theoref - killed.</p>
<p>=====<br /><abbr title="S">ASSERTION</abbr> <abbr title="ES">DO</abbr>N'T HOLD<br />A real bug found</p>
<p>VERIFICATION FAILED<br />Initial unwinding bound: 10<br />Total number of steps: 1<br />TOTAL TIME FOR CHECKING THIS CLAIM: 81.555</p>
<p>Main Checked Assertion: <br /> file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/eca-rers2012/Problem01_label38_false-unreach-call.c line 422 function calculate_output<br /> assertion<br /> FALSE<br />; -------------------------<br />; STATISTICS FOR SAT SOLVER<br />; -------------------------<br />; Restarts.................: 17<br />; Conflicts................: 3587<br />; Decisions................: 12005<br />; Propagations.............: 38193667<br />; Conflict literals........: 178550<br />; T-Lemmata learnt.........: 0<br />; T-Lemmata perm learnt....: 0<br />; Conflicts learnt.........: 3587<br />; T-conflicts learnt.......: 0<br />; Average learnts size.....: 49.7418<br />; Top level literals.......: 6686<br />; Search time..............: 0 s<br />; TSolvers time............: 0.02 s<br />; Init clauses.............: 603447<br />; Variables................: 127354<br />; -------------------------<br />; STATISTICS FOR EUF SOLVER<br />; -------------------------<br />; Satisfiable calls........: 0<br />; Unsatisfiable calls......: 0<br />; egraph time..............: 0 s<br />; backtrack time...........: 0 s<br />; explain time.............: 0 s<br />; # eq classes at the end..: 0<br />; -------------------------<br />; STATISTICS FOR LOGICS<br />; -------------------------<br />; Substitutions............: 0<br />#X: Done.<br />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</p>