Bug #5100
Error: No support for "big" (> 32 bit) integers so far.
0%
Description
~/hi-bench/main-bench/Funfrog15_bench$ ./hifrog --claim 44 --theoref --bitwidth 32
RESULT in CUF: SAT - doesn't hold
Trying to refine with CUF+BitBlast
(driven by iterative CE-analysis)
No support for "big" (> 32 bit) integers so far.
History
#1 Updated by Sepideh Asadi about 7 years ago
the same problem with claim 50, claim 66 s3.c
CBMC verifies such cases
#2 Updated by Karine Even Mendoza about 7 years ago
Fixed
- INLINING function: main
Processing a deferred function: __CPROVER_initialize
Processing a deferred function: main - INLINING function: ssl3_connect
Processing a deferred function: ssl3_connect
SYMEX TIME: 0.157
All SSA steps: 155
Ignored SSA steps after slice: 90
SLICER TIME: 0.001
CONVERSION TIME: 0
; theory refiner query time so far: 0.000000
; 0 | 0 0 | 1.156 s | 116.410 MB
SOLVER TIME: 0.001
RESULT: SAT - doesn't hold
Trying to refine with CUF+BitBlast
(all statements at once)
; theory refiner query time so far: 0.000000
; 0 | 0 0 | 1.160 s | 116.410 MB
ASSERTION DOES NOT HOLD
VERIFICATION FAILED
TOTAL TIME FOR CHECKING THIS CLAIM: 0.162
Checked Assertion:
file ../../../../../../hi-bench/main-bench/Funfrog15_bench/s3.c line 1154 function ssl3_connect
assertion
tmp___9 == 140737488346048l
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hifrog_theory_ref/hifrog/trunk/cprover/src/funfrog$ ./hifrog ../../../../../../hi-bench/main-bench/Funfrog15_bench/s3.c --logic qfcuf --theoref --bitwidth 64 --force --claim 44 --unwind 10 --force
#3 Updated by Karine Even Mendoza about 7 years ago
- Status changed from New to Closed
- Assignee set to Karine Even Mendoza