ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_basic_tg.cpp, Line: 139

[merlinsun]

Hi,
For this following instance, z3 f678861 debug build

$ cat delta.smt2 
(declare-fun a () (Seq Int))
(declare-fun r () (Seq (Seq Int)))
(declare-fun ar () (Seq (Seq Int)))
(assert (exists ((v String)) (= "" (str.replace "" v (int.to.str 0)))))
(assert (distinct r ar (seq.unit a)))
(check-sat-using qe2)
$ z3 delta.smt2 
ASSERTION VIOLATION
File: ../src/qe/mbp/mbp_basic_tg.cpp
Line: 139
m_mdl.is_false(e)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

[hgvk94]

The problem is that in MBP, we want the model to evaluate expressions as true or false but model evaluation is not always complete (expected). Here, we reduce an expression to (= (seq.nth_i r 0) (seq.unit 2) but cannot reduce it to false. I guess, for now, the best action is to revert to earlier behavior when such things happen.