ASSERTION VIOLATION, File: ../src/ast/fpa/fpa2bv_converter.cpp #7661
Description
Hi,
For the following instance, z3 80c553d debug build throws out an assertion violation
$ cat test.smt2
(declare-const r Real)
(assert (fp.isNormal ((_ to_fp 60 39) RTP r)))
(check-sat)
$ z3 test.smt2
ASSERTION VIOLATION
File: ../src/ast/fpa/fpa2bv_converter.cpp
Line: 2814
m_mpz_manager.is_uint(max_exp_z)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a