mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

fixed memory error

Browse source
This commit is contained in:
Ken McMillan 2013-12-15 17:24:51 -08:00
parent ebc8a43fe3
commit 852f53d6a6
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/duality/duality_solver.cpp
View file

@ -1780,9 +1780,12 @@ namespace Duality {
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end()) if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!"; throw "help!";
} }
}
RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
RemoveExpansion(node); RemoveExpansion(node);
} }
RemoveLeaves(leaves_to_remove);
stack.pop_back(); stack.pop_back();
if(prev_level_used || stack.size() == 1) break; if(prev_level_used || stack.size() == 1) break;
RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list