[514] % cvc4-1.8 -q -i --check-unsat-cores small.smt2
unsat
unsat
[515] % cvc5 -q -i --check-unsat-cores small.smt2
unsat
Fatal failure within void cvc5::SmtEngine::checkUnsatCore() at /local/suz-local/software/CVC4/src/smt/smt_engine.cpp:1453
Internal error detectedSmtEngine::checkUnsatCore(): produced core was satisfiable.
Aborted
[516] % 
[516] % cat small.smt2
(declare-const a String)
(declare-const b String)
(declare-const c String)
(push)
(assert (= (str.++ a b) c))
(assert (= a "A"))
(assert (= c ""))
(check-sat)
(pop)
(assert (= (str.++ a b) (str.++ "A" c)))
(assert (= c (str.++ a b)))
(check-sat)
[517] %