[598] % cvc5 -q --strings-exp small.smt2
sat
[599] % cvc5 -q --strings-exp --ext-rewrite-quant --full-saturate-quant small.smt2
unsat
[600] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (= b (str.replace_re a (str.to_re "A") "A")))
(assert (not (str.prefixof (str.++ b b) a)))
(check-sat)
[601] %