Project

General

Profile

Bug #4681

wrong result/core dump in Directory:main-bench/funfrog_regression/06_globals

Added by Sepideh Asadi about 7 years ago. Updated almost 7 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Karine Even Mendoza
Start date:
07/03/2017
Due date:
% Done:

100%

Estimated time:

Description

Hifrog fails (verification failed) for the following benchmarks, while CBMC verifies correctly.

Directory:main-bench/funfrog_regression/06_globals/main3
/main4
/main5
/main6
/main7
/main8

global-main7-prop.png (408 KB) global-main7-prop.png Sepideh Asadi, 16/03/2017 06:49
global_main5_pop.png (404 KB) global_main5_pop.png Sepideh Asadi, 16/03/2017 06:55

History

#1 Updated by Karine Even Mendoza about 7 years ago

Horrible bug related to renaming in new CPROVER framework.

#2 Updated by Karine Even Mendoza about 7 years ago

  • Assignee set to Karine Even Mendoza
  • % Done changed from 0 to 100

Hopefully it is done now

#3 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from New to Resolved

#4 Updated by Sepideh Asadi about 7 years ago

new bugs:

./hifrog ~/dev/hi-bench/main-bench/funfrog_regression/06_globals/main8.c --claim 1 --logic qflra >> failed >> what it supposed to be in LRA?UNSAT?

-----------------------------------------------------------------------------------
./hifrog ~/dev/hi-bench/main-bench/funfrog_regression/06_globals/main7.c --claim 1 --logic prop >> core dumped >>screenshot attached.

Interpolant for function: __CPROVER_initialize is trivial.
hifrog: solvers/prop_itp.cpp:365: void prop_itpt::generalize(const prop_conv_solvert&, const std::vector<symbol_exprt>&): Assertion `idx >= 0' failed.
Aborted (core dumped)

./hifrog ~/dev/hi-bench/main-bench/funfrog_regression/06_globals/main7.c --claim 1 --logic qflra >>failed

./hifrog ~/dev/hi-bench/main-bench/funfrog_regression/06_globals/main5.c --claim 1 --logic qflra >>failed

./hifrog ~/dev/hi-bench/main-bench/funfrog_regression/06_globals/main5.c --claim 1 --logic prop >> core dumped >>screenshot attached.

#5 Updated by Karine Even Mendoza about 7 years ago

  • % Done changed from 50 to 70

Left only with main5.c - the rest is working.

hifrog: solvers/prop_itp.cpp:369: void prop_itpt::generalize(const prop_conv_solvert&, const std::vector<symbol_exprt>&): Assertion `idx >= 0' failed.
./../hifrog_theory_ref/hifrog/trunk/cprover/src/funfrog/hifrog --claim 1 main-bench/funfrog_regression/06_globals/main5.c --logic prop

#6 Updated by Karine Even Mendoza about 7 years ago

  • % Done changed from 70 to 80

main5.c --logic prop fails in cnf.

The rest is working

#7 Updated by Karine Even Mendoza about 7 years ago

Verification failed for all theories for main5.c as well main7.c

#8 Updated by Karine Even Mendoza about 7 years ago

All ok but main5

RESULT
SOLVER TIME: 0.625
UNSAT - it holds!
ASSERTION IS TRUE
Start generating interpolants...
hifrog: solvers/prop_itp.cpp:370: void prop_itpt::generalize(const prop_conv_solvert&, const std::vector<symbol_exprt>&): Assertion `idx >= 0 && "Failed to generalize interpolant; Index of represented_symbol is out of bound"' failed.
Aborted (core dumped)

#9 Updated by Karine Even Mendoza almost 7 years ago

Works good for all, except this test case:

./hifrog ../../../../../../hi-bench/main-bench/funfrog_regression/06_globals/main5.c --logic prop --claim 2

But for ./hifrog ../../../../../../hi-bench/main-bench/funfrog_regression/06_globals/main5.c --logic prop, will work just fine.

#10 Updated by Karine Even Mendoza almost 7 years ago

fixed. Was a bug of cutting the code after the line of assert

#11 Updated by Karine Even Mendoza almost 7 years ago

  • Status changed from In Progress to Closed
  • % Done changed from 80 to 100

Also available in: Atom PDF