Added by Sepideh Asadi over 7 years ago. Updated over 7 years ago.
10%
Description
/hifrog --claim 1 --logic prop --bitwidth 8 --unwind 1 ~/hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c
VERIFICATION FAILED
wrong result! because claim 1 should hold
KE: can be long time bug, as the old funfrof crashes,
XXX=============================================================================
XXX Partition: 4 (ass_in_subtree: 0) - c::stub_driver_init (loc: 101, SUM)
evolcheck: sat/cnf.cpp:675: bool cnft::process_clause(const bvt&, bvt&): Assertion `l.var_no()!=literalt::unused_var_no()' failed.
Aborted (core dumped)
karinek@karinek-VirtualBox:~/workspace/tools/verify_cprover/trunk/cprover/src/funfrog$ ./evolcheck ../../../../../hi-bench/main-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c
Need larger bit-width:
Data 18446744072635809814(18446744072635809814) is not in between -256 and 255Data 18446744072635809814(18446744072635809814) is not in between -4294967296 and 4294967295
With 32 bits, but when using 64 bits - got out of memory.
Run with:
./hifrog ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c --type-constraints 2 --logic qfcuf --no-itp --theoref --force --bitwidth 32
MEM ISSUES - LOW Priority
This is not related to the goto problem, we need to check it to understand the reason. Maybe the way the assert is encoded.
Shall be with 64 bits not 8. Also I will try to use type constraints.
With 64 bits, even with unwind 1, we get "killed"...
Maybe we can minimize the number of refined instructions so we can use small register (less than 64...)?