Bug #5305
Bug related to No support for "big" (> 32 bit)
100%
Description
./hifrog --claim 1 --theoref --no-itp --unwind 10 --bitwidth 32 --heuristic 4 --type-byte-constraints 2 ~/hi-bench/main-bench/bench_SATpaper_128/sep_true-unreach-call.c
with --bitwidth 32 it says "No support for "big" (> 32 bit) integers so far.
with --bitwidth 64 it gets timeout!
History
#1 Updated by Sepideh Asadi almost 7 years ago
same bug with soft_float_5_true-unreach-call.c.cil.c
#2 Updated by Karine Even Mendoza almost 7 years ago
- Priority changed from Normal to Low
#3 Updated by Karine Even Mendoza almost 7 years ago
- Status changed from New to Feedback
- Assignee set to Sepideh Asadi
- Priority changed from Low to Normal
For me it works just fine. Can you please re-test it?
Refinement successful
(21 / 259 expressions bit-blasted)
Command-line options to double-check: --theoref --custom 2,5,11,17,23,29,35,41,47,53,59,60,61,62,63,64,65,66,67,68,69,
(Warning: Result holds ONLY in this bound (!) Initial unwinding bound: 10)
ASSERTION HOLDS
VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 1.148
Main Checked Assertion:
file ../../../../../../hi-bench/main-bench/bench_SATpaper_128/sep_true-unreach-call.c line 56 function main
assertion
FALSE
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog$ ./hifrog ../../../../../../hi-bench/main-bench/bench_SATpaper_128/sep_true-unreach-call.c --claim 1 --theoref --no-itp --unwind 10 --bitwidth 64 --heuristic 4 --type-byte-constraints 2
Also soft_float_5_true-unreach-call.c.cil.c works very nice...
#4 Updated by Sepideh Asadi almost 7 years ago
- Status changed from Feedback to Closed
- % Done changed from 0 to 100
Conclusion:
When it is reported "No support for "big" (> 32 bit) integers so far." run it with --bitwidth 64