z3str3 incorrect answer on QF_S formula with str.replace

Hi,
For this formula,
```
(declare-fun a () String)
(declare-fun b () String)
(assert (distinct (str.replace (str.replace "A" b a) "B" "A")
          (str.replace "A" b (str.replace a "B" "A"))))
(check-sat)
```
`z3 smt.string_solver=z3str3` incorrectly gives `sat`, while this formula should be `unsat`.

OS: Ubuntu 18.04
Revision: 140926e

