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 9c73779e36bd49c0817dab63f4078d2978d5bd40..104420789bb257088c27144aca170c95acbeeb9a 100644 (file)
--- 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();