From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 30 Mar 2022 03:57:41 +0000 (-0500)
Subject: Add LFSC to internal proof checker (#8442)
X-Git-Tag: cvc5-1.0.0~129
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e46533cd87d21988996e1324a37a68f2e60ff8ef;p=cvc5.git

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.
---

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());