[539] % z3-4.8.5 small.smt2 
unsat
sat
[540] % z3-4.8.6 small.smt2 
unsat
unsat
[541] % z3-4.8.7 small.smt2 
unsat
unsat
[542] % z3-4.8.8 small.smt2 
unsat
sat
[543] % z3release small.smt2 
unsat
sat
[544] % cat small.smt2 
(declare-fun a () String)
(assert (distinct (str.in.re a (re.inter (str.to.re "B") (re.+ (str.to.re "B"))))
     (str.in.re a (str.to.re "BB"))))
(assert (= (str.in.re a (re.union (str.to.re "A") (str.to.re "B")))
     (str.in.re a (re.inter (str.to.re "") (str.to.re "B")))))
(check-sat-using (then purify-arith nnf default))
(check-sat)
[545] %