Assertion violation at /src/qe/mbp/mbp_arith.cpp:72

[merlinsun]

Hi,
For this instance, z3 1953165

$ cat delta.smt2
(declare-fun ar () (Array Int (Array (Array Bool Bool) Bool)))
(declare-fun r () (Array Bool Bool))
(declare-fun v () (Array (Array (Array Bool Bool) Bool) (Array (Array Bool Bool) Bool)))
(declare-fun a () (Array (Array Bool Bool) Bool))
(assert (not (distinct a (select ar 0) (select (store v a (store (select ar 0) r false)) a))))
(assert (exists ((va (Array Bool (Array Real Real)))) (forall ((V Real)) (= 1.0 (select (va true) 0.0)))))
(check-sat-using qe2)
$ z3debug delta.smt2
ASSERTION VIOLATION
File: ../src/qe/mbp/mbp_arith.cpp
Line: 72
m.limit().is_canceled() || !m.is_false(val)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB