[607] % cvc5 -q --dump-models small.smt2
sat
(
(define-fun a () String "")
(define-fun b () String "AC")
(define-fun c () String "A")
(define-fun d () String "A")
)
[608] % cvc5 -q --ext-rew-prep small.smt2
unsat
[609] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(assert (= (str.++ "A" a "CBA" b "BA" d) (str.++ b "BA" d a "CBA" c)))
(check-sat)
[610] %