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 40f0d35bbb41d24af3e2b1f1336668991c8f6e58..50ab353ad53163902858c75a1a7d8d47feb1e6d2 100644 (file)
--- 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());