Bug #4998
openbug 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
Updated by Karine Even Mendoza over 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
Updated by Karine Even Mendoza over 7 years ago
- Assignee set to Karine Even Mendoza
Updated by Karine Even Mendoza over 7 years ago
Need larger bit-width:
Data 18446744072635809814(18446744072635809814) is not in between -256 and 255Updated by Karine Even Mendoza over 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
Updated by Karine Even Mendoza over 7 years ago
- Priority changed from Normal to Low
- % Done changed from 0 to 10
MEM ISSUES - LOW Priority
Updated by Karine Even Mendoza over 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.
Updated by Karine Even Mendoza over 7 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...)?