[598] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/qe/qe_mbp.cpp
Line: 215
m.is_true(val) || m.is_false(val)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[599] % 
[599] % cat small.smt2
(set-option :model_evaluator.array_equalities false)
(declare-fun a () (Array Bool Bool))
(declare-fun b () (Array Bool Bool))
(assert (select a (= a b)))
(check-sat-using qe2)
[600] %