Potential completeness issue on a simple instance involving str.replace_all #7391
Description
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