Z3 hangs on simple QF_S formula with str.replace and str.++

[muchang]

Hi,
In this case, Z3 latest build hangs on the formula while z3-4.8.7 produces results quickly.

[613] % time z3-4.8.7 small.smt2
unsat
real	0m0.028s
user	0m0.025s
sys	0m0.000s
[614] % timeout -s 9 10 z3release small.smt2
Killed
[615] % timeout -s 9 10 z3release smt.arith.solver=2 small.smt2
Killed
[616] % 
[616] % cat small.smt2
(declare-fun a () String)
(assert (distinct (str.replace (str.++ "A" a) "B" a) (str.++ "A" (str.replace a "B" a))))
(check-sat)
[617] %

OS: Ubuntu 18.04
Commit: 7597396