[552] % cvc4-1.8 -q --check-unsat-cores small.smt2
unsat
[553] % cvc5 -q --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 encounteredTConvProofGenerator::getProofFor: TheoryPreprocessor::rtf (policy=FIXPOINT, cache policy=NEVER, term-context-sensitive): failed, mismatch (see -t tconv-pf-gen-debug for details)
                   source: (let ((_let_1 (ite a 0 1))) (and (>= (mod _let_1 2) 2) (>= _let_1 0) (not (>= _let_1 2))))
     requested conclusion: (and (>= (+ termITE_1 (* (- 2) linearIntDiv_2)) 2) (>= termITE_1 0) (not (>= termITE_1 2)))
conclusion from generator: (and (not (not (>= (+ termITE_1 (* (- 2) linearIntDiv_2)) 2))) (>= termITE_1 0) (not (>= termITE_1 2)))

Aborted
[554] % 
[554] % cat small.smt2
(declare-fun a () Bool)
(assert (> (mod (ite a 0 1) 2) 1))
(check-sat)
[555] %