From 7c794bd260cd2d6d2660f3137b79ee23a26106f7 Mon Sep 17 00:00:00 2001 From: Lachnitt Date: Mon, 28 Mar 2022 11:44:44 -0700 Subject: [PATCH] [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. --- src/theory/builtin/proof_checker.cpp | 6 ++++++ 1 file changed, 6 insertions(+) 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); -- 2.30.2