[708] % z3 small.smt2
(smt.diff_logic: non-diff logic expression (+ 1 (str.len s)))
unsat
sat
[709] % 
[709] % cat small.smt2
(set-option :smt.arith.solver 1)
(declare-fun s () String)
(assert (str.in.re (str.++ "a" s) (re.* (str.to.re "b"))))
(check-sat)
(check-sat-using unit-subsume-simplify)
[710] %