Project

General

Profile

Bug #6037

Error in generating interpolant in svcomp 17

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

Status:
New
Priority:
Normal
Assignee:
-
Start date:
20/12/2017
Due date:
% Done:

0%

Estimated time:

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.092
RESULT: 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

History

#1 Updated by S A over 6 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

#2 Updated by S A over 6 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

#3 Updated by S A over 6 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.

#4 Updated by S A over 6 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

Also available in: Atom PDF