From 016892c3ac5a17dad880fe361f7766ff86bdeb9c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 7 Apr 2022 07:29:53 -0500 Subject: [PATCH] Fix proof checker for SUBS (#8578) Could lead to proof checking failures when using `--proof-granularity=rewrite` --- src/theory/builtin/proof_checker.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) 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(); -- 2.30.2