ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp Line: 583

[merlinsun]

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

$ cat small.smt2 
(declare-const x (Array Bool Int))
(assert (forall ((v (Array Bool Int))) (distinct 0 (select (store x (= x v) 0) false))))
(check-sat-using qsat)
$ z3 small.smt2 
ASSERTION VIOLATION
File: ../src/qe/qe_mbp.cpp
Line: 583
!eval.is_false(fml)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a