(smt.threads=3) Soundness bug on QF_S formula with regex

[muchang]

Hi,
For this case, Z3 smt.threads=3 gives an incorrect answer:

[93] % ./z3release small.smt2 
sat
[94] % ./z3release smt.threads=3 small.smt2 
unsat
[95] % cat small.smt2 
(declare-fun a () String)
(assert (str.in.re (str.++ "z" a)(re.* (re.+ (re.++ (re.* (str.to.re "b"))(str.to.re "z"))))))
(assert (not (str.in.re a (re.inter (str.to.re "") (re.* (str.to.re "a"  )))))) 
(check-sat)                                                                                                                                   
[96] % 

OS: Ubuntu 18.04
Commit: 8fe3caa

[NikolajBjorner]

#4049