search

cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Error: The type expected for an application does not match the computed type #87

Open rodrigo7491 opened 1 year ago

rodrigo7491 commented 1 year ago

Hi,

When trying to check the proof produced by cvc5 for the files in ex.zip, I get the following error (see the zip file for the full output):

Error: ex.proof at 26984:1-26984:2
The type expected for an application does not match the computed type.
1. The expected type: (holds ((\ t1 (\ t2 (apply (apply f_= t1) t2))) (apply ...
2. The computed type: (holds ((\ t1 (\ t2 (apply (apply f_= t1) t2))) ((\ t1 (\ t2 (apply ...

Unfortunately I was not able to reproduce the error with a smaller instance. I'm running cvc5 v1.0.5 and lfscc from commit 9aab068dec2c5a9f5f2bf465590005c638078e95, with signatures from commit c09fa26fdd3b114351789f252311c6ea02f69e56. CLI commands below.

cvc5 --produce-proofs --proof-format=lfsc --proof-granularity=theory-rewrite ex.smt2
lfscc core_defs.plf util_defs.plf theory_def.plf nary_programs.plf boolean_programs.plf boolean_rules.plf cnf_rules.plf equality_rules.plf arith_programs.plf arith_rules.plf strings_programs.plf strings_rules.plf quantifiers_rules.plf ex.proof

The error only happens with proofs produced using the --proof-granularity=theory-rewrite cvc5 flag.