Potential completeness issue on a simple instance involving `str.replace_all`

[merlinsun]

Hi,
For the following instance, z3 (fa7fc8e, debug build) gives unknown.

$ cat unknown.smt2 
(declare-fun a () String)
(assert (= a (str.replace_all "" a "")))
(check-sat)
$ z3 unknown.smt2 
unknown

If (str.replace_all "" a "") can be simplified to "", z3 returns sat.

$ cat pass.smt2 
(declare-fun a () String)
(assert (= a ""))
(check-sat)
$ z3 pass.smt2 
sat