Seq/regex soundness bug with random seed depdendency #4258
Description
Hi,
For this case, Z3 gives an incorrect answer:
[835] % for f in $(seq 1 10) ; do z3release small.smt2; done
unsat
unsat
unsat
sat
unsat
unsat
sat
unsat
sat
sat
[836] %
[836] % cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :smt.arith.solver 6)
(set-option :smt.random_seed 11)
(set-option :smt.threads 2)
(declare-fun a () String)
(assert
(xor
(distinct (str.in.re a (re.union (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.inter (re.union (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)
[837] %
OS: Ubuntu 18.04
Commit: becf423