search

cvc5 / cvc5-projects

1 stars 0 forks source link

SymFPU issues about supporting special floating variables #228

Open rainoftime opened 4 years ago

rainoftime commented 4 years ago

Hi, CVC4 commit 3075a8e throws errors on a formula from z3 regression tests

$ ./cvc4  -q f.smt2
/CVC4/deps/install/include/symfpu/core/unpackedFloat.h:175:38: runtime error: shift exponent 52 is too large for 32-bit type 'int'
Fatal failure within static void CVC4::symfpuLiteral::traits::precondition(const prop&) at /CVC4/src/util/floatingpoint.cpp:445
Check failure

 p

Aborted

$ cat f.smt2
(declare-fun f (Int) (_ FloatingPoint 53 11))
(assert (= (f 1) (_ +oo 53 11)))
(check-sat)
martin-cs commented 4 years ago

I have done some work on this and will hopefully be doing more over the next few months.