Bug #6037
openError in generating interpolant in svcomp 17
0%
Description
Description
When Start generating interpolants the following error occurred:
How to run:
/hifrog --unwind 10 --logic qfuf --claim 1 /home/asadis/hi-bench/challenge-bench/sv-comp17/c/eca-rers2012/Problem02_label31_true-unreach-call.c
Error message:
SOLVER TIME: 26.092RESULT: UNSAT - it holds!
Start generating interpolants...
- Error in `/home/asadis/private-repo/hifrog/trunk/cprover/src/funfrog/hifrog': double free or corruption (!prev): 0x0000000011700510 ***
Command terminated by signal 6
real 35.66
Updated by S A almost 7 years ago
The same problem for:
--claim 5 ~/sv-comp17/c/product-lines/email_spec4_product29_true-unreach-call_true-termination.cil.c
--claim 2 ~/ldv-linux-3.14**linux-3.14__complex_emg__linux-usb-dev__drivers-net-wireless-rndis_wlan_true-unreach-call.cil.c_c2
Updated by S A almost 7 years ago
Sepideh Asadi wrote:
The same problem for:
--claim 5 ~/sv-comp17/c/product-lines/email_spec4_product29_true-unreach-call_true-termination.cil.c
--claim 2 ~/sv-comp17/c/ldv-linux-3.14/linux-3.14__complex_emg__linux-usb-dev__drivers-net-wireless-rndis_wlan_true-unreach-call.cil.c
Updated by S A almost 7 years ago
Sepideh Asadi wrote:
The same problem for:
--claim 5 ~/sv-comp17/c/product-lines/email_spec4_product29_true-unreach-call_true-termination.cil.c
--claim 2 ~/ldv-linux-3.14**linux-3.14__complex_emg__linux-usb-dev__drivers-net-wireless-rndis_wlan_true-unreach-call.cil.c_c2
ignor the case in the comments.
Updated by S A almost 7 years ago
/hifrog --logic qfuf --unwind 10 --claim 1 ~/hi-bench/challenge-bench/sv-comp17/c/eca-rers2012/Problem02_label08_true-unreach-call.c
Error message:
RESULT: UNSAT - it holds!
Start generating interpolants...
Killed