[549] % cvc5 -q --strings-exp --check-models 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 (re.* re.allchar ))) (not (= a (str.replace_re_all a (re.++ _let_1 (str.to_re a) _let_1) a))))
simplifies to: false
expected `true'.
Run with `--check-models -v' for additional diagnostics.
Aborted
[550] % 
[550] % cat small.smt2
(declare-fun a () String)
(assert (not (= a (str.replace_re_all a (re.++ (re.* re.allchar) (str.to_re a) (re.* re.allchar)) a))))
(check-sat)
[551] %