[522] % cvc4-1.8 -q --re-elim --re-elim-agg --check-unsat-cores small.smt2
unsat
[523] % cvc5 -q --re-elim --re-elim-agg --check-unsat-cores small.smt2
Fatal failure within virtual std::shared_ptr<cvc5::ProofNode> cvc5::TConvProofGenerator::getProofFor(cvc5::Node) at /local/suz-local/software/CVC4/src/proof/conv_proof_generator.cpp:229
Unhandled case encountered TConvProofGenerator::getProofFor: TheoryPreprocessor::preprocess_rewrite (policy=FIXPOINT, cache policy=NEVER, term-context-sensitive): failed, mismatch (see -t tconv-pf-gen-debug for details)
                   source: (let ((_let_1 (re.comp (re.* re.allchar )))) (let ((_let_2 (str.to_re a))) (let ((_let_3 (re.++ _let_2 _let_1))) (str.in_re "" (re.++ (re.inter _let_1 (re.comp _let_3)) (str.to_re (ite (str.in_re "" (re.++ (str.to_re (ite (str.in_re "" _let_3) a "")) (re.inter _let_2 _let_3))) a "")))))))
     requested conclusion: false
conclusion from generator: (let ((_let_1 (re.comp (re.* re.allchar )))) (str.in_re "" (re.++ (re.inter _let_1 (re.comp (re.++ (str.to_re a) _let_1))) (str.to_re (ite (and (= a "") false) a "")))))

Aborted
[524] % 
[524] % cat small.smt2
(declare-fun a () String)
(assert
 (str.in_re ""
  (re.++ (re.diff (re.comp re.all) (re.++ (str.to_re a) (re.comp re.all)))
   (str.to_re
    (ite
     (str.in_re ""
      (re.++ (str.to_re (ite (str.in_re "" (re.++ (str.to_re a) (re.comp re.all))) a ""))
       (re.inter (str.to_re a)
        (re.++ (str.to_re a)
         (re.comp (re.union (re.++ (str.to_re a) (re.comp re.all)) re.all))))))
     a "")))))
(check-sat)
[525] %