From e46533cd87d21988996e1324a37a68f2e60ff8ef Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 29 Mar 2022 22:57:41 -0500 Subject: [PATCH] Add LFSC to internal proof checker (#8442) Similar to ALETHE, this was forgotten. Was not causing issues since --proof-check=eager is not used by default. --- src/theory/builtin/proof_checker.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 40f0d35bb..50ab353ad 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -58,6 +58,8 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS_EQ, this, 3); pc->registerTrustedChecker(PfRule::THEORY_INFERENCE, this, 3); + // external proof rules + pc->registerChecker(PfRule::LFSC_RULE, this); pc->registerChecker(PfRule::ALETHE_RULE, this); } @@ -382,7 +384,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(args[0].getType().isBoolean()); return args[0]; } - else if (id == PfRule::ALETHE_RULE) + else if (id == PfRule::LFSC_RULE || id == PfRule::ALETHE_RULE) { Assert(args.size() > 1); Assert(args[0].getType().isInteger()); -- 2.30.2