Bug #5327
opentime out in disk.c
0%
Description
for e.g claim 15, 16,...
gets timeout with 32, 64 bit unwind 10,...
Updated by Karine Even Mendoza over 7 years ago
1. This shall be run properly with 64 bits,there are many error messages saying it shall better be run in 64 because of the SSA encoding is in 64 bit for this benchmark
2. It is a very heavy code. We always run it with --unwind 1. But for this to run in CUF we need to work much on the performance in Opensmt...
3. there are some issues with the SSA parsing of this code.
4. It works with heuristic 4 (that's why we did it hahaha)
No support for "big" (> 32 bit) integers so far.
Data -8(width 64) is not in between -4294967296 and 4294967295
; theory refiner query time so far: 0.000000
Weak statement encodings (1) foundRefinement successful
(1 / 548 expressions bit-blasted)
Command-line options to double-check: --theoref --custom 1,
(Warning: Result holds ONLY in this bound (!) Initial unwinding bound: 10)
ASSERTION HOLDS
VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 6.518
Main Checked Assertion:
file ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c line 4425 function IofCompleteRequest
assertion
byte_extract_little_endian(pirp->Tail, 0l, KAPC).ApcListEntry.Blink == (struct _LIST_ENTRY *)byte_extract_little_endian(pirp->Tail, 0l, KAPC).SystemArgument2
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog$ ./hifrog ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c --theoref --bitwidth 32 --type-byte-constraints 2 --unwind 10 --claim 15 --heuristic 4
Updated by Karine Even Mendoza over 7 years ago
- Status changed from New to Feedback
- Assignee changed from Sepideh Asadi to Antti Hyvärinen
- Can be a candidate for performance issues once using bithwidth 64 (4=>timeout, 5=>UNSAT)
Currently, there are few new changes from opensmt, but it seems to work fine with 32 or 64 bits (but the proper way to run it is still with 64 bits).
================================== 32 bit
All SSA steps: 6637
Ignored SSA steps after slice: 4146
SLICER TIME: 0.007
CONVERSION TIME: 0.145
; theory refiner query time so far: 0.000000
; 0 | 0 0 | 6.368 s | 160.926 MB
SOLVER TIME: 0.518
RESULT: SAT - doesn't hold
Trying to refine with CUF+BitBlast
(driven by iterative CE-analysis)
; Warning: disabling SATElite preprocessing to track proof
; Forward dependency checker query time so far: 0.000000
; 0 | 0 0 | 6.608 s | 208.766 MB
No support for "big" (> 32 bit) integers so far.
Data 8(width 64) is not in between -4294967296 and 4294967295
; Forward dependency checker query time so far: 0.000000
; ------------------------
; STATISTICS FOR SAT SOLVER
; -------------------------
; Restarts.................: 1
; Conflicts................: 0
; Decisions................: 34
; Propagations.............: 162
; Conflict literals........: 0
; T-Lemmata learnt.........: 0
; T-Lemmata perm learnt....: 0
; Conflicts learnt.........: 0
; T-conflicts learnt.......: 0
; Average learnts size.....: nan
; Top level literals.......: 98
; Search time..............: 0 s
; TSolvers time............: 0 s
; Init clauses.............: 64
; Variables................: 162
; ------------------------
; STATISTICS FOR EUF SOLVER
; -------------------------
; Satisfiable calls........: 0
; Unsatisfiable calls......: 0
; egraph time..............: 0 s
; backtrack time...........: 0 s
; explain time.............: 0 s
; # eq classes at the end..: 0
; -------------------------
; STATISTICS FOR LOGICS
; -------------------------
; Substitutions............: 0No support for "big" (> 32 bit) integers so far.
Data -8(width 64) is not in between -4294967296 and 4294967295
; Added 1 equalities for bind
; theory refiner query time so far: 0.000000
Weak statement encodings (1) foundRefinement successful
(1 / 548 expressions bit-blasted)
Command-line options to double-check: --theoref --custom 1,
(Warning: Result holds ONLY in this bound (!) Initial unwinding bound: 10)
ASSERTION HOLDS
VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 6.368
Main Checked Assertion:
file ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c line 4425 function IofCompleteRequest
assertion
byte_extract_little_endian(pirp->Tail, 0l, KAPC).ApcListEntry.Blink (struct _LIST_ENTRY *)byte_extract_little_endian(pirp->Tail, 0l, KAPC).SystemArgument2
Added 15 equalities for bind
; theory refiner query time so far: 0.000000
Weak statement encodings (1) found
Weak statement encodings (5) found
Weak statement encodings (2) found
Refinement successful
(8 / 548 expressions bit-blasted)
Command-line options to double-check: --theoref --custom 525,531,532,533,534,535,536,542,
(Warning: Result holds ONLY in this bound (!) Initial unwinding bound: 10)
ASSERTION HOLDS
VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 7.914
Main Checked Assertion:
file ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c line 4425 function IofCompleteRequest
assertion
byte_extract_little_endian(pirp->Tail, 0l, KAPC).ApcListEntry.Blink == (struct _LIST_ENTRY *)byte_extract_little_endian(pirp->Tail, 0l, KAPC).SystemArgument2
./hifrog ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c --theoref --bitwidth 32 --type-byte-constraints 2 --unwind 10 --claim 15 --heuristic 5