1 files changed, 20 insertions, 9 deletions
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h
index 10fe2853b..3c78a8790 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -133,7 +133,7 @@ public:
 private:
   typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
   NodeCountMap d_termITEHeight;
-};
+}; /* class TermITEHeightCounter */
 
 /**
  * A routine designed to undo the potentially large blow up
@@ -177,7 +177,7 @@ private:
     ~Statistics();
   };
   Statistics d_statistics;
-};
+}; /* class ITECompressor */
 
 class ITESimplifier {
 public:
@@ -302,6 +302,15 @@ public:
 
   void clear();
 private:
+
+  /**
+   * This should always equal the number of care sets allocated by
+   * this object - the number of these that have been deleted. This is
+   * initially 0 and should always be 0 at the *start* of
+   * ~ITECareSimplifier().
+   */
+  unsigned d_careSetsOutstanding;
+
   Node d_true;
   Node d_false;
 
@@ -309,12 +318,16 @@ private:
 
   class CareSetPtr;
   class CareSetPtrVal {
+   public:
+    bool safeToGarbageCollect() const { return d_refCount == 0; }
+   private:
     friend class ITECareSimplifier::CareSetPtr;
     ITECareSimplifier& d_iteSimplifier;
     unsigned d_refCount;
     std::set<Node> d_careSet;
-    CareSetPtrVal(ITECareSimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {}
-  };
+    CareSetPtrVal(ITECareSimplifier& simp)
+        : d_iteSimplifier(simp), d_refCount(1) {}
+  }; /* class ITECareSimplifier::CareSetPtrVal */
 
   std::vector<CareSetPtrVal*> d_usedSets;
   void careSetPtrGC(CareSetPtrVal* val) {
@@ -350,16 +363,14 @@ private:
       return *this;
     }
     std::set<Node>& getCareSet() { return d_val->d_careSet; }
-    static CareSetPtr mkNew(ITECareSimplifier& simp) {
-      CareSetPtrVal* val = new CareSetPtrVal(simp);
-      return CareSetPtr(val);
-    }
+
+    static CareSetPtr mkNew(ITECareSimplifier& simp);
     static CareSetPtr recycle(CareSetPtrVal* val) {
       Assert(val != NULL && val->d_refCount == 0);
       val->d_refCount = 1;
       return CareSetPtr(val);
     }
-  };
+  }; /* class ITECareSimplifier::CareSetPtr */
 
   CareSetPtr getNewSet();