Refutational soundness bug in QF_S

[wintered]

Hi,
the following trace shows a refutational soundness bug in Z3 (c49d39a).

[596] % z3release small.smt2
unsat
sat
[597] % cat small.smt2
(declare-const a String)
(assert (distinct (str.replace (str.replace a "B" a) a "AB") (str.replace (str.replace a "B" "AB") a "AB")))
(check-sat)
(reset)
(define-fun a () String "B")
(assert (distinct (str.replace (str.replace a "B" a) a "AB") (str.replace (str.replace a "B" "AB") a "AB")))
(check-sat)
[598] %