fix bug #134: infinite deallocation loop

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 6c97854132f17be25259fbf9fee1fb3e39176eb2..7c8fb229acdd7f85aa43fa57b0b2ac1fb21b5920 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -24,6 +24,7 @@
 #include "theory/bv/theory_bv_type_rules.h"
 
 #include <ext/hash_set>
+#include <algorithm>
 
 using namespace std;
 using namespace CVC4::expr;
@@ -140,9 +141,10 @@ void NodeManager::reclaimZombies() {
 
   vector<NodeValue*> zombies;
   zombies.reserve(d_zombies.size());
-  std::copy(d_zombies.begin(),
-            d_zombies.end(),
-            std::back_inserter(zombies));
+  std::remove_copy_if(d_zombies.begin(),
+                      d_zombies.end(),
+                      std::back_inserter(zombies),
+                      NodeValueReferenceCountNonZero());
   d_zombies.clear();
 
   for(vector<NodeValue*>::iterator i = zombies.begin();

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 098694c3d640d8e45464f77f12939d82485e4606..a5f82b489950b55b11d9047952663994ea0736f3 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -54,6 +54,11 @@ class NodeManager {
   friend class NodeManagerScope;
   friend class expr::NodeValue;
 
+  /** Predicate for use with STL algorithms */
+  struct NodeValueReferenceCountNonZero {
+    bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
+  };
+
   typedef __gnu_cxx::hash_set<expr::NodeValue*,
                               expr::NodeValuePoolHashFcn,
                               expr::NodeValuePoolEq> NodeValuePool;