Assertion Violation at /src/util/mpf.cpp:907

[merlinsun]

Hi,
For this instance, z3 9061ca5 debug build

$ z3 delta.smt2
ASSERTION VIOLATION
File: ../src/util/mpf.cpp
Line: 907
exp(res) < mk_max_exp(x.ebits)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
^C
$ cat delta.smt2
(declare-const x Bool)
(declare-const x1 Bool)
(declare-fun ar () Bool)
(declare-fun var () Bool)
(declare-fun ar8 () (_ FloatingPoint 2 6))
(declare-fun r837 () (_ FloatingPoint 2 6))
(declare-fun r2 () Bool)
(declare-fun r13 () Bool)
(declare-fun r18 () Bool)
(declare-fun ar1 () Bool)
(declare-fun r7 () (_ BitVec 12))
(declare-fun r1 () (_ BitVec 13))
(declare-fun var1 () (_ BitVec 3))
(declare-fun r83 () (_ FloatingPoint 2 6))
(declare-fun r16 () Bool)
(declare-fun r15 () Bool)
(declare-fun r132 () (_ BitVec 3))
(declare-fun r29 () Real)
(declare-fun r88 () Bool)
(declare-fun va () Bool)
(declare-fun r8 () (_ FloatingPoint 2 6))
(declare-fun r () Bool)
(declare-fun v () Bool)
(declare-fun a () (_ BitVec 40))
(assert (or (= x1 va) (distinct ar8 (fp.sub RTZ r83 r837)) (distinct r7 (_ bv0 12)) (and x x1 (= a (_ bv0 40))) v (distinct (bvmul r1 r1) r1)))
(assert (or (or (= ar8 (fp.fma RTZ r83 r837 r8)) (not (= r13 x1)) (and r88 r2 (= ar1 (= 1 1)) (= r18 (is_int r29)))) (= r (ite r16 true x)) (= r132 (ite (not ar) (_ bv0 3) (ite var (_ bv0 3) (ite va (ite (or var r15) (_ bv0 3) (bvadd var1 (_ bv1 3))) (_ bv0 3)))))))
(check-sat-using (then aig qsat))

OS: Ubuntu 20.04

[NikolajBjorner]

Hits an NYI.

        if (m_mpz_manager.ge(res.significand(), m_powers2(2 * x.sbits + 3)))
        {
            SASSERT(exp(res) < mk_max_exp(x.ebits)); // NYI.

Though is masked during standard tactics that use pre-processing simplify.

------------------------------------------------
-------- [mpf_dbg] mpf_manager::fma ..\src\util\mpf.cpp:899 ---------
-------- [mpf_dbg] mpf_manager::fma ..\src\util\mpf.cpp:817 ---------
A = -2.8125 1
B = -2.9375 1
C = 2.96875 0
A = #b1 #b10 #b01.11010
B = #b1 #b10 #b01.11110
C = #b0 #b01 #b01.11111
------------------------------------------------
-------- [mpf_dbg] mpf_manager::fma ..\src\util\mpf.cpp:830 ---------
M = 4.51171875 2
M = #b0 #b1001 #b11.1000001100
------------------------------------------------
-------- [mpf_dbg] mpf_manager::fma ..\src\util\mpf.cpp:844 ---------
C_= 2.96875 0
C_= #b0 #b0111 #b01.1111100000000
------------------------------------------------
-------- [mpf_dbg] mpf_manager::fma ..\src\util\mpf.cpp:867 ---------
alignment shift by delta=2 -> sig = 4032 sticky_rem = 0
------------------------------------------------
-------- [mpf_dbg] mpf_manager::fma ..\src\util\mpf.cpp:871 ---------
M'= 28768
M'= #b0 #b1001 #b11.1000001100000
------------------------------------------------
-------- [mpf_dbg] mpf_manager::fma ..\src\util\mpf.cpp:873 ---------
C'= 4032
C'= #b0 #b0111 #b00.0111111000000
------------------------------------------------
-------- [mpf_dbg] mpf_manager::fma ..\src\util\mpf.cpp:891 ---------
ADDING
------------------------------------------------
S'= 32800
S'= #b0 #b1001 #b100.0000000100000
------------------------------------------------