[517] % cvc4-1.8 --strings-exp -q small.smt2
unsat
[518] % z3release small.smt2
unsat
[519] % cvc5 --strings-exp -q small.smt2
sat
[520] % cvc5 --strings-exp --check-models -q small.smt2
Fatal failure within void cvc5::smt::CheckModels::checkModel(cvc5::smt::Model*, cvc5::context::CDList<cvc5::NodeTemplate<true> >*, bool) at /local/suz-local/software/CVC4/src/smt/check_models.cpp:125
Internal error detected SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:
assertion:     (let ((_let_1 (str.len a))) (= (str.++ a "0" (str.at (str.substr (str.++ a a a) 0 3) _let_1) "A") (str.++ "0" (str.from_code _let_1) (str.replace "AA" (str.++ a "AA") a))))
simplifies to: false
expected `true'.
Run with `--check-models -v' for additional diagnostics.
Aborted
[521] % 
[521] % cat small.smt2
(declare-fun a () String)
(assert
 (= (str.++ a "0" (str.at (str.substr (str.++ a a a) 0 3) (str.len a)) "A")
  (str.++ "0" (str.from_code (str.len a)) (str.replace "AA" (str.++ a "AA") a))))
(check-sat)
[522] %