$ cvc5 -q --check-proofs bug.smt2
Fatal failure within cvc5::internal::Node cvc5::internal::ProofChecker::check(cvc5::ProofRule,
const std::vector<std::shared_ptr<cvc5::internal::ProofNode> >&, const std::vector<cvc5::internal::
NodeTemplate<true> >&, cvc5::internal::Node) at
/home/x59011dw/reduce-bisect/cvc5/src/proof/proof_checker.cpp:106
Unreachable code reached ProofChecker::check: failed, result does not match expected value.
ProofRule: ARITH_MULT_NEG
arg: @purify_2
arg: (> (* skoX skoY) (+ (/ 2 3) (* (/ 1 3) (* skoX skoX))))
result: (let ((_let_1 (+ (/ 2 3) (* (/ 1 3) (* skoX skoX))))) (let ((_let_2 (* skoX skoY)))
(=> (and (< @purify_2 0) (> _let_2 _let_1)) (< (* @purify_2 _let_2) (* @purify_2 _let_1)))))
expected: (let ((_let_1 (+ (/ 2 3) (* (/ 1 3) (* skoX skoX))))) (let ((_let_2 (to_real @purify_8)))
(let ((_let_3 (* skoX skoY))) (=> (and (< @purify_8 0) (> _let_3 _let_1)) (< (* _let_2 _let_3) (* _let_2 _let_1))))))
Aborted (core dumped)
$ cat bug.smt2
(set-option :proof-check eager)
(declare-fun skoX () Real) (declare-fun skoY () Real) (declare-fun skoZ () Real)
(assert (let ((?v_2 (<= 0 skoY))(?v_0 (* skoX (- 1)))) (let ((?v_3 0)(?v_4 (<= (* skoZ
(+ 0 (* skoY skoX))) 0))) (let ((?v_1 (not ?v_4))(?v_5 0)) (let ((?v_6 (* skoY (* skoX (+ (- 3) ?v_5)))))
(and (<= 0 0) (and ?v_1 (and (or ?v_1 ?v_2) (and (< (+ (+ 3 (* skoX skoX)) ?v_6) 1) (and
(or (not ?v_2) (or (< 0 ?v_0) (<= (* (to_real (- (to_int ?v_0))) (* (+ (+ 3 (* skoX skoX)) ?v_6) (- 3)))
(+ (+ (+ (* skoX ?v_5) (* skoY (+ (* skoX (* skoX (- 3))) ?v_6))) (+ ?v_0 (* skoY (- 1)))) (to_real (+
(- 1) ?v_0)))))) (and (< (- 1) (+ (+ 1 ?v_0) (* skoY (+ (- 1) (* (* skoY (+ (- 3) (+ 1 ?v_0))) ?v_5)))))
(and (not (<= (+ ?v_5 skoY) (- 1))) (and (not (=> (<= ?v_0 skoY) (<= skoZ 0))) (not (<= skoY ?v_6)))))))))))))))
(check-sat)
(exit)
```
