Bug #5008
theoref BuG: tcas_asrt
0%
Description
Funfrog15_bench/tcas_asrt.c --claim 1
History
#1 Updated by Sepideh Asadi about 7 years ago
Sepideh Asadi wrote:
Funfrog15_bench/tcas_asrt.c --claim 50
#2 Updated by Karine Even Mendoza about 7 years ago
- Status changed from New to Feedback
- Assignee set to Sepideh Asadi
I get this error:
hifrog: solvers/smtcheck_opensmt2_cuf.h:126: int mp_integer2int(const mp_integer&): Assertion `"Framework currently does not support numbers larger than ints" && ll <= std::numeric_limits<int>::max()' failed.
Aborted (core dumped)
Is it correct?
#3 Updated by Karine Even Mendoza about 7 years ago
This is the issue now:
SYMEX TIME: 1.793
All SSA steps: 2972
Ignored SSA steps after slice: 1424
SLICER TIME: 0.024
CONVERSION TIME: 1.736
; theory refiner query time so far: 0.000000
; 0 | 0 0 | 5.288 s | 117.809 MB
; 210 | 168 168 | 5.656 s | 113.555 MB
; 331 | 270 270 | 5.960 s | 113.691 MB
SOLVER TIME: 0.944
RESULT: SAT - doesn't hold
Trying to refine with CUF+BitBlast
(all statements at once)
No support for "big" (> 1024 bit) integers so far.
#4 Updated by Karine Even Mendoza about 7 years ago
- Status changed from Feedback to Closed
Now works, claim 1 is UNSAT?