ASSERTION VIOLATION, File: ../src/qe/qsat.cpp Line: 655

[merlinsun]

Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/2682c2ef2b3f31f065cc54b83e91f6d42c60db2f debug build

$ cat small.smt2 
(declare-fun b () (_ FloatingPoint 3 2))
(assert (exists ((a (_ FloatingPoint 3 2)) (a (_ FloatingPoint 3 2)) (a (_ FloatingPoint 3 2))) (= (fp (_ bv0 1) (_ bv0 3) (_ bv0 1)) (fp.fma roundNearestTiesToEven b b (fp (_ bv0 1) (_ bv0 3) (_ bv0 1)))))) 
(check-sat-using qsat) 
(check-sat-using qsat)
$ z3 small.smt2 
sat
ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 655
validate_defs("check_sat")
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a