Bug #4998
bug in QF_BOOL: wrong result for prop in benchs in directrory ntdrivers-simplified
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
History
#1 Updated by Karine Even Mendoza about 7 years ago
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
#2 Updated by Karine Even Mendoza about 7 years ago
- Assignee set to Karine Even Mendoza
#3 Updated by Karine Even Mendoza almost 7 years ago
Need larger bit-width:
Data 18446744072635809814(18446744072635809814) is not in between -256 and 255#4 Updated by Karine Even Mendoza almost 7 years ago
Data 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
#5 Updated by Karine Even Mendoza almost 7 years ago
- Priority changed from Normal to Low
- % Done changed from 0 to 10
MEM ISSUES - LOW Priority
#6 Updated by Karine Even Mendoza almost 7 years ago
- Status changed from New to In Progress
- Priority changed from Low to Normal
This is not related to the goto problem, we need to check it to understand the reason. Maybe the way the assert is encoded.
#7 Updated by Karine Even Mendoza over 6 years ago
- Status changed from In Progress to Feedback
- Assignee changed from Karine Even Mendoza to Antti Hyvärinen
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...)?