Fixing a memory leak in array info.

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index e94abe9cb6410c00468094a8d4f811942593e9bd..acc73163c03ad714634a948fe81d3bc86b34eaa4 100644 (file)
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -23,6 +23,27 @@ namespace CVC4 {
 namespace theory {
 namespace arrays {
 
+Info::Info(context::Context* c, Backtracker<TNode>* bck)
+    : isNonLinear(c, false),
+      rIntro1Applied(c, false),
+      modelRep(c,TNode()),
+      constArr(c,TNode()),
+      weakEquivPointer(c,TNode()),
+      weakEquivIndex(c,TNode()),
+      weakEquivSecondary(c,TNode()),
+      weakEquivSecondaryReason(c,TNode())
+{
+  indices = new(true)CTNodeList(c);
+  stores = new(true)CTNodeList(c);
+  in_stores = new(true)CTNodeList(c);
+}
+
+Info::~Info() {
+  indices->deleteSelf();
+  stores->deleteSelf();
+  in_stores->deleteSelf();
+}
+
 ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b)
     : ct(c), bck(b), info_map(),
       d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
@@ -115,11 +136,9 @@ void ArrayInfo::addIndex(const Node a, const TNode i) {
 
   CNodeInfoMap::iterator it = info_map.find(a);
   if(it == info_map.end()) {
-    temp_indices = new(true) CTNodeList(ct);
-    temp_indices->push_back(i);
-
     temp_info = new Info(ct, bck);
-    temp_info->indices = temp_indices;
+    temp_indices = temp_info->indices;
+    temp_indices->push_back(i);
     info_map[a] = temp_info;
   } else {
     temp_indices = (*it).second->indices;

diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 3e479e0f9fe5136d910b5eed15e63e59c37df9d7..319864c346f60f1f7bfaae3f3ce32175656e8b7a 100644 (file)
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -74,25 +74,8 @@ public:
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck)
-    : isNonLinear(c, false),
-      rIntro1Applied(c, false),
-      modelRep(c,TNode()),
-      constArr(c,TNode()),
-      weakEquivPointer(c,TNode()),
-      weakEquivIndex(c,TNode()),
-      weakEquivSecondary(c,TNode()),
-      weakEquivSecondaryReason(c,TNode()) {
-    indices = new(true)CTNodeList(c);
-    stores = new(true)CTNodeList(c);
-    in_stores = new(true)CTNodeList(c);
-  }
-
-  ~Info() {
-    indices->deleteSelf();
-    stores->deleteSelf();
-    in_stores->deleteSelf();
-  }
+  Info(context::Context* c, Backtracker<TNode>* bck);
+  ~Info();
 
   /**
    * prints the information