[537] % cvc5 -q --strings-exp --check-models small.smt2
sat
[538] % cvc5 -q --strings-exp --check-models --re-elim --re-elim-agg 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 detectedSmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:
assertion:     (let ((_let_1 (str.++ b "a"))) (str.in_re (str.replace_re b (str.to_re (str.replace_all a _let_1 b)) _let_1) (re.+ (str.to_re "b"))))
simplifies to: false
expected `true'.
Run with `--check-models -v' for additional diagnostics.
Aborted
[539] % 
[539] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (str.in_re (str.replace_re b (str.to_re (str.replace_all a (str.++ b "a") b)) (str.++ b "a")) (re.+ (str.to_re "b"))))
(assert (str.in_re a (re.* (re.range "a" "b"))))
(check-sat)
[540] %