(z3str3 ctx-solver-simplify) Soundness bug on QF_SLIA formula

[muchang]

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

[504] % z3release smt.string_solver=z3str3 small.smt2
sat
unsat
[505] % 
[505] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () String)
(assert (= a 1))
(assert (str.in.re b (re.inter (str.to.re "") (str.to.re "a"))))
(check-sat-using ctx-solver-simplify)
(check-sat)
[506] %

OS: Ubuntu 18.04
Commit: fc8dfe3

[zhendongsu]

A simpler, almost identical test:

[614] % z3 smt.string_solver=z3str3 small.smt2
sat
unsat
[615] % 
[615] % cat small.smt2
(declare-fun a () String)
(assert (str.in.re a (re.+ (re.inter (str.to.re "") (str.to.re "a")))))
(check-sat-using ctx-solver-simplify)
(check-sat)
[616] %