[662] % z3 small.smt2
sat
[663] % z3 smt.arith.solver=1 small.smt2
unsat
[664] % 
[664] % cat small.smt2
(declare-fun s () String)
(assert (not (str.in.re s (re.* (str.to.re "a")))))
(check-sat)
[665] %