From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 7 Apr 2022 12:29:53 +0000 (-0500)
Subject: Fix proof checker for SUBS (#8578)
X-Git-Tag: cvc5-1.0.1~290
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=016892c3ac5a17dad880fe361f7766ff86bdeb9c;p=cvc5.git

Fix proof checker for SUBS (#8578)

Could lead to proof checking failures when using `--proof-granularity=rewrite`
---

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 9c73779e3..104420789 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -226,9 +226,14 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
   else if (id == PfRule::SUBS)
   {
     Assert(children.size() > 0);
-    Assert(1 <= args.size() && args.size() <= 2);
+    Assert(1 <= args.size() && args.size() <= 3) << "Args: " << args;
     MethodId ids = MethodId::SB_DEFAULT;
-    if (args.size() == 2 && !getMethodId(args[1], ids))
+    if (args.size() >= 2 && !getMethodId(args[1], ids))
+    {
+      return Node::null();
+    }
+    MethodId ida = MethodId::SBA_SEQUENTIAL;
+    if (args.size() >= 3 && !getMethodId(args[2], ida))
     {
       return Node::null();
     }
@@ -237,7 +242,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     {
       exp.push_back(children[i]);
     }
-    Node res = applySubstitution(args[0], exp, ids);
+    Node res = applySubstitution(args[0], exp, ids, ida);
     if (res.isNull())
     {
       return Node::null();