[532] % cvc4-1.8 -q --check-unsat-cores small.smt2
(define-fun d () Bool (= b a))
[533] % cvc5 -q --check-unsat-cores small.smt2
Fatal failure within void cvc5::theory::EagerProofGenerator::setProofFor(cvc5::Node, std::shared_ptr<cvc5::ProofNode>) at /local/suz-local/software/CVC4/src/theory/eager_proof_generator.cpp:35
Check failure

 pf->getResult() == f
EagerProofGenerator::setProofFor: unexpected result
Expected: (>= rsk_11 1)
Actual: (not (not (>= rsk_11 1)))

Aborted
[534] % 
[534] % cat small.smt2
(set-option :produce-abducts true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= (>= b c) (>= 0 a)))
(assert (= c a))
(get-abduct d (<= a b))
[535] %