Soundness bug on QF_S formula

[muchang]

Hi,
For this case, Z3 gives an incorrect answer:

[689] % z3-4.8.8 small.smt2
sat
[690] % z3release small.smt2
unsat
[691] % cat small.smt2
(declare-fun a () String)
(assert
 (or
 (distinct (str.in.re a (re.inter (str.to.re "B") (re.+ (str.to.re "B"))))
  (str.in.re a (re.union (str.to.re "B") (str.to.re "BB"))))
 (distinct (str.in.re a (re.union (re.inter (str.to.re "A") re.allchar) (str.to.re "B")))
  (str.in.re a (re.union (str.to.re "A") (str.to.re "B"))))))
(check-sat)
[692] %

OS: Ubuntu 18.04
Commit: a14c2a3

[NikolajBjorner]

appended to duplicate