[587] % cvc5 -q --strings-exp small.smt2
unsat
[588] % cvc5 -q --strings-exp --re-elim --re-elim-agg small.smt2
sat
[589] % cat small.smt2
(declare-fun a () String)
(assert (str.in_re (str.replace_re a (re.++ (str.to_re "A") (re.union (str.to_re "") (str.to_re (str.from_code (str.len a))))) "AB") (re.+ (str.to_re "A"))))
(check-sat)
[590] %