[549] % z3release small.smt2
unsat
[550] % z3release smt.string_solver=z3str3 small.smt2
sat
[551] % cat small.smt2
(declare-fun a () String)
(assert (str.in.re a (re.inter (re.opt re.allchar) (str.to.re "ab"))))
(check-sat-using ctx-solver-simplify)
[552] %