[646] % z3release small.smt2
sat
[647] % z3release smt.threads=2 small.smt2
unsat
[648] % cvc4 -q small.smt2
sat
[649] % 
[649] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in.re (str.++ "z" b) (re.++ (re.* (re.union (str.to.re "z") (str.to.re "") (str.to.re "b"))) (re.union (str.to.re "") (str.to.re "a")))))
(assert (not (str.in.re (str.++ a "a") (re.inter (re.* (str.to.re "")) (str.to.re "")))))
(check-sat)
[650] %