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 /src/expr | |
| 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..
Diffstat (limited to 'src/expr')
| -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(); + } } } |