[515] % cvc5 -q small.smt2
sat
[516] % cvc5 -q --re-elim --re-elim-agg small.smt2
unknown
[517] % cvc5 -q --re-elim --re-elim-agg --check-unsat-cores small.smt2
Fatal failure within cvc5::Node cvc5::TConvProofGenerator::registerRewriteStep(cvc5::Node, cvc5::Node, uint32_t, bool) at /local/suz-local/software/CVC4/src/proof/conv_proof_generator.cpp:157
Check failure

 getRewriteStepInternal(thash, isPre) == s
TheoryPreprocessor::preprocess_rewrite rewriting (str.in_re a (re.* (str.to_re "A"))) to both (forall ((BOUND_VARIABLE_725 Int)) (or (not (and (<= 0 BOUND_VARIABLE_725) (< BOUND_VARIABLE_725 (str.len a)))) (= "A" (str.substr a BOUND_VARIABLE_725 1)))) and (forall ((BOUND_VARIABLE_599 Int)) (or (not (and (<= 0 BOUND_VARIABLE_599) (< BOUND_VARIABLE_599 (str.len a)))) (= "A" (str.substr a BOUND_VARIABLE_599 1))))
Aborted
[518] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert
 (str.in_re (str.++ a (ite (str.in_re (str.++ a "BA" b) (re.++ (re.* (str.to_re "A")) (str.to_re "B"))) b a))
  (re.diff (re.* (str.to_re "A")) (str.to_re ""))))
(check-sat)
[519] %