From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 30 Jul 2020 01:15:44 +0000 (-0500)
Subject: (proof-new) Fixes for getFreeAssumptions (#4802)
X-Git-Tag: cvc5-1.0.0~3071
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f5eb204df574d8f680e802601ca279f82eaf0146;p=cvc5.git

(proof-new) Fixes for getFreeAssumptions (#4802)

Free assumptions weren't getting cleaned up due to not doing a postorder traversal. This issue came up when doing subproof sharing involving SCOPE proofs.
---

diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 45dc2d995..9e1018024 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -86,6 +86,7 @@ void getFreeAssumptionsMap(ProofNode* pn,
           }
           // will need to unbind the variables below
           visited[cur] = false;
+          visit.push_back(cur);
         }
         // The following loop cannot be merged with the loop above because the
         // same subproof
@@ -98,6 +99,7 @@ void getFreeAssumptionsMap(ProofNode* pn,
     }
     else if (!it->second)
     {
+      visited[cur] = true;
       Assert(cur->getRule() == PfRule::SCOPE);
       // unbind its assumptions
       for (const Node& a : cargs)