From: Lachnitt <lachnitt@stanford.edu>
Date: Mon, 28 Mar 2022 18:44:44 +0000 (-0700)
Subject: [proofs] Alethe: Add ALETHE_RULE to builtin proof checker (#8409)
X-Git-Tag: cvc5-1.0.0~153
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7c794bd260cd2d6d2660f3137b79ee23a26106f7;p=cvc5.git

[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 1c714b856..4aa676e39 100644
--- 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);