Checking failed with rule 'assume': term was not in original problem's assumptions

[rodrigo7491]

Hi,

When trying to check the proof produced by cvc5 for the files in ex.zip, I get the following error:

[ERROR] checking failed on step 'a2' with rule 'assume': term '(and (and (inv_main5 H K A J L) (and (= G 0) (= F A) (= E H) (= D 0) (= C B) (= N J) (= M K) (<= 1 B) (or (and (<= 1 B) (= D 1)) (and (not (<= 1 B)) (= D 0))) (= I 0) (= v_14 D))) (not (inv_main21 E M F N C I G D v_14)))' was not in original problem's assumptions
invalid

The only difference I can see between the term assumed in the proof and the one asserted in the .smt2 file is the inlining of the let statement. I'm running cvc5 v1.0.5 and carcara v1.0.0, CLI commands below.

cvc5 --produce-proofs --proof-format=alethe --proof-granularity=theory-rewrite --flatten-ho-chains ex.smt2 carcara check --skip-unknown-rules --allow-int-real-subtyping ex.proof ex.smt2

[HanielB]

Hi Rodrigo. Can you try with passing the option --expand-let-bindings to Carcara? The issue here is that cvc5 does not keep track of the expansion of let bindings in the input (which is against the Alethe standard). With that option Carcara is lenient with that and compares the assume steps to the assertions module let binding expansion.

[rodrigo7491]

Hi @HanielB, thanks for the response and the explanation. Using the option you mentioned does fix the issue. Since there is an interplay between cvc5 and carcara, this was not obvious to me.