[proofs] Alethe: Add ALETHE_RULE to builtin proof checker (#8409)

Proofs would fail because the internal proof checker would return null and the alethe check is not trusted.

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 1c714b856830067853473cd42a0742e62f2239fe..4aa676e3914e9ae439f8e180c7f34323931a7d0b 100644 (file)
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -382,6 +382,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     Assert(args[0].getType().isBoolean());
     return args[0];
   }
+  else if (id == PfRule::ALETHE_RULE)
+  {
+    Assert(args.size() > 1);
+    Assert(args[0].getType().isInteger());
+    return args[1];
+  }
   else if (id == PfRule::ANNOTATION)
   {
     Assert(children.size() == 1);