diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-06 20:19:34 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-06 20:19:34 +0000 |
commit | 2db22ffd1f48502a2b138b9b99ba2841a581313b (patch) | |
tree | f621e9528691f9ea6c78bee824ff24302e6837f9 | |
parent | 4cdfe4a1979c6bf3f5afe7f5733fd35308710300 (diff) |
Don't eagerly collect zombies. This should speed up things for competition but might flush out some memory issues. Passes all regressions so far..
-rw-r--r-- | src/expr/node_manager.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 4d796d81c..d01e22abd 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -191,7 +191,9 @@ class NodeManager { if(!d_inReclaimZombies) {// FIXME multithreading // for now, collect eagerly. can add heuristic here later.. - reclaimZombies(); + if(d_zombies.size() > 5000) { + reclaimZombies(); + } } } |