8 files changed, 57 insertions, 10 deletions

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index e3c7e155c..492dc7939 100644
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -138,9 +138,15 @@ public:
    * Destructor: delete the list
    */
   ~CDList() throw(AssertionException) {
-    T* list = d_list;
     destroy();
-    free(list);
+
+    if(d_callDestructor) {
+      for(unsigned i = 0; i < d_size; ++i) {
+        d_list[i].~T();
+      }
+    }
+
+    free(d_list);
   }
 
   /**
diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 460f917ff..1dc44d087 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -201,13 +201,13 @@ public:
 
   ~CDMap() throw(AssertionException) {
     // Delete all the elements and clear the map
-    for(typename table_type::iterator
-	  i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
-      /*
+    /*for(typename table_type::iterator
+          i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
+
         delete (*i).second;
         free((*i).second);
-      */
-    }
+
+    }*/
     d_map.clear();
     emptyTrash();
   }
diff --git a/src/context/context.h b/src/context/context.h
index 6b9f9fd6d..87e4e5fa1 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -399,7 +399,7 @@ public:
   /**
    * Destructor does nothing: subclass must explicitly call destroy() instead.
    */
-  virtual ~ContextObj() {}
+  virtual ~ContextObj() { Debug("contextgc") << "context obj dest" << std::endl; }
 
   /**
    * If you want to allocate a ContextObj object on the heap, use this
@@ -426,6 +426,7 @@ public:
    * ContextMemoryManager as an argument.
    */
   void deleteSelf() {
+    this->~ContextObj();
     ::operator delete(this);
   }
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 25990cedf..f7cef5a4c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -522,7 +522,9 @@ NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
   if(ref_count) {
     d_nv->dec();
   }
-  Assert(ref_count || d_nv->d_rc > 0,
+  Assert(ref_count ||
+         d_nv->d_rc > 0 ||
+         d_nv->isBeingDeleted(),
          "Temporary node pointing to an expired node");
 }
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 7b171a48b..ee370f682 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -61,6 +61,19 @@ struct Reclaim {
   }
 };
 
+struct NVReclaim {
+  NodeValue*& d_reclaimField;
+  NVReclaim(NodeValue*& reclaim) :
+    d_reclaimField(reclaim) {
+
+    Debug("gc") << ">> setting NVRECLAIM field\n";
+  }
+  ~NVReclaim() {
+    Debug("gc") << "<< clearing NVRECLAIM field\n";
+    d_reclaimField = NULL;
+  }
+};
+
 void NodeManager::reclaimZombies() {
   // FIXME multithreading
 
@@ -104,6 +117,8 @@ void NodeManager::reclaimZombies() {
       if(nv->getKind() != kind::VARIABLE) {
         poolRemove(nv);
       }
+      NVReclaim rc(d_underTheShotgun);
+      d_underTheShotgun = nv;
 
       // remove attributes
       d_attrManager.deleteAllAttributes(nv);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index a3be61e48..044deac7f 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -72,6 +72,12 @@ class NodeManager {
   friend class NodeManagerScope;
   friend class expr::NodeValue;
 
+  bool isCurrentlyDeleting(const expr::NodeValue *nv) const{
+    return d_underTheShotgun == nv;
+  }
+
+  expr::NodeValue* d_underTheShotgun;
+
   bool d_reclaiming;
   ZombieSet d_zombies;
 
@@ -105,7 +111,10 @@ public:
 
   NodeManager(context::Context* ctxt) :
     d_attrManager(ctxt),
-    d_reclaiming(false) {
+    d_underTheShotgun(NULL),
+    d_reclaiming(false)
+
+  {
     poolInsert( &expr::NodeValue::s_null );
   }
 
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index cbe4e718a..9f1063715 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -141,6 +141,8 @@ private:
   /** Decrement ref counts of children */
   inline void decrRefCounts();
 
+  bool isBeingDeleted() const;
+
 public:
 
   template <bool ref_count>
@@ -266,6 +268,9 @@ inline void NodeValue::decrRefCounts() {
 }
 
 inline void NodeValue::inc() {
+  Assert(!isBeingDeleted(),
+         "NodeValue is currently being deleted "
+         "and increment is being called on it. Don't Do That!");
   // FIXME multithreading
   if(EXPECT_TRUE( d_rc < MAX_RC )) {
     ++d_rc;
@@ -301,6 +306,13 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
+
+inline bool NodeValue::isBeingDeleted() const
+{
+  return NodeManager::currentNM() != NULL &&
+    NodeManager::currentNM()->isCurrentlyDeleting(this);
+}
+
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index 199b09164..248e1e545 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -175,6 +175,8 @@ public:
    */
   ECData(context::Context* context, TNode n);
 
+  ~ECData() { Debug("ufgc") << "Calling ECData destructor" << std::endl;}
+
   /**
    * An ECData takes over the watch list of another ECData.
    * This is the second step in the union operator for ECData.