Bug #5006
Theoref openSMT BUG: Opensmt supports only up to int size, not more!
100%
Description
./hifrog --theoref Funfrog15_bench/s3.c - -claim 28
bug:
hifrog: solvers/smtcheck_opensmt2_cuf.h:115: int mp_integer2int(const mp_integer&): Assertion `ll <= std::numeric_limits<int>::max()' failed.
Aborted (core dumped)
~
History
#1 Updated by Sepideh Asadi about 7 years ago
the same bug with --claim 34 cafe.c
hifrog: solvers/smtcheck_opensmt2_cuf.h:117: int mp_integer2int(const mp_integer&): Assertion `"Framework currently does not support numbers larger than ints" && ll <= std::numeric_limits<int>::max()' failed.
#2 Updated by Sepideh Asadi about 7 years ago
the same bug with --claim 34 tcas_asrt.c
#3 Updated by Karine Even Mendoza about 7 years ago
In file: src/logics/BVLogic.h in OpenSMT.
The fix is in this method:
PTRef mkBVConst (const int c)
{ char* num; opensmt::wordToBinary(c, num, getBitWidth()); PTRef tr = Logic::mkConst(sort_BVNUM, num); free(num); return tr; } // Convert the int c to binary
As long as this is not supporting anything larger than int, we cannot do much. The assert is a check before the call for this method.
#4 Updated by Karine Even Mendoza about 7 years ago
- Status changed from New to Closed
- % Done changed from 0 to 100
but resolved. We have new bugs now!