(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 45dc2d995bef9ec4e65640a4afb0147f2181bf3b..9e10180241db68cba9229d5f3cd4ace1ec1bf3ac 100644 (file)
--- 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)