$ z3release small.smt2
sat
$ z3release rewriter.cache_all=true small.smt2
unsat
$ z3-4.8.10 rewriter.cache_all=true small.smt2
unsat
$ cat small.smt2
(declare-fun a () String)
(assert
(str.in_re
(str.++ a "z")
(re.++
(re.union (str.to_re "c") (str.to_re (ite (= a "") "z" "")))
(str.to_re "z")
(str.to_re (ite (= a "") "z" "")))))
(check-sat)