ASSERTION VIOLATION, File: ../src/ast/fpa/fpa2bv_converter.cpp

[merlinsun]

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