Assertion violation at ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:140

[merlinsun]

Hi, For this instance, z3 https://github.com/Z3Prover/z3/commit/e423fabf6a8808c36d906cdd62dda9c90773992d

$ cat small.smt2
(declare-fun var810 () String)
(assert (and (forall ((va String)) (or (= "B" var810) (not (str.in_re va (re.union (str.to_re "z") (str.to_re (str.substr "z" 0 (str.len var810))))))))))
(check-sat-using ctx-solver-simplify)
$ z3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp
Line: 140
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a

[merlinsun]

Another case:

$ cat case.smt2
(declare-const x Bool)
(declare-fun v () (Seq (Seq Int)))
(assert (forall ((a (Seq Int)) (va (Seq (Seq Int)))) (and (not x) (distinct v (seq.++ (seq.unit a) va)))))
(check-sat-using ctx-solver-simplify)
$ z3 case.smt2
ASSERTION VIOLATION
File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp
Line: 140
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a