Don't eagerly collect zombies. This should speed up things for competition but might...

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 4d796d81c2b086af1cfceaf3a807ff603c17c956..d01e22abd41f47a6089bd6e93a2e32191abf2ec1 100644 (file)
--- 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();
+      }
     }
   }