(z3str3, dom-simplify, ctx-solver-simplify, smt.str.fixed_length_refinement) Assertion violation at ../src/smt/theory_str_mc.cpp Line: 1162

[muchang]

Hi, For this formula, Z3 throws out an assertion violation:

[582] % z3release smt.string_solver=z3str3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/theory_str_mc.cpp
Line: 1162
NOT IMPLEMENTED YET!
Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[583] % z3debug smt.string_solver=z3str3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/theory_str_mc.cpp
Line: 1162
NOT IMPLEMENTED YET!
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[584] % 
[584] % cat small.smt2
(set-option :smt.str.fixed_length_refinement true)
(declare-fun a () String)
(declare-fun b () Int)
(assert (= (str.replace "B" (str.at "A" b) "") "B" a))
(check-sat-using (then dom-simplify ctx-solver-simplify))
[585] %

OS: Ubuntu 18.04 Commit: fc8dfe3