From f5eb204df574d8f680e802601ca279f82eaf0146 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 29 Jul 2020 20:15:44 -0500
Subject: [PATCH] (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.
---
 src/expr/proof_node_algorithm.cpp | 2 ++
 1 file changed, 2 insertions(+)

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)
-- 
2.30.2