(smt.threads=2) Soundness bug on QF_S with regular expression

[muchang]

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

[1071] % z3release small.smt2
sat
[1072] % cvc4 -q small.smt2
sat
[1073] % z3release smt.threads=2 small.smt2
unsat
[1074] % 
[1074] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in.re a (re.++ (re.* (re.union (str.to.re "z") (str.to.re "a"))) (str.to.re "a"))))
(assert (not (str.in.re (str.++ "b" b) (re.inter (re.* (re.+ (str.to.re ""))) (str.to.re "b")))))
(check-sat)
[1075] %

OS: Ubuntu 18.04
Commit: bcbe802

[NikolajBjorner]

seems fixed