diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-29 20:15:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-29 20:15:44 -0500 |
| commit | f5eb204df574d8f680e802601ca279f82eaf0146 (patch) | |
| tree | 8d92e66d81fb0d024a459a04653bd0cfb54e4427 | |
| parent | 24710c2f7f754cd8297409f82b5cb0789e16ee18 (diff) | |
(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.
| -rw-r--r-- | src/expr/proof_node_algorithm.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
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) |