Fix EqProof memory management

10 files changed, 295 insertions, 236 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 0f0c14eb2..feee738eb 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -88,7 +88,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
   if(tb == 0) {
     Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS);
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.size() >= 2);
+    Assert(pf->num_children() >= 2);
 
     int neg = -1;
     theory::eq::EqProof subTrans;
@@ -96,16 +96,16 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
     subTrans.d_node = pf->d_node;
 
     size_t i = 0;
-    while (i < pf->d_children.size()) {
+    while (i < pf->num_children()) {
       // Look for the negative clause, with which we will form a contradiction.
-      if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) {
+      if(!pf->get_child(i)->d_node.isNull() && pf->get_child(i)->d_node.getKind() == kind::NOT) {
         Assert(neg < 0);
         neg = i;
         ++i;
       }
 
       // Handle congruence closures over equalities.
-      else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) {
+      else if (pf->get_child(i)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->get_child(i)->d_node.isNull()) {
         Debug("pf::arith") << "Handling congruence over equalities" << std::endl;
 
         // Gather the sequence of consecutive congruence closures.
@@ -113,13 +113,13 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
         unsigned count;
         Debug("pf::arith") << "Collecting congruence sequence" << std::endl;
         for (count = 0;
-             i + count < pf->d_children.size() &&
-             pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
-             pf->d_children[i + count]->d_node.isNull();
+             i + count < pf->num_children() &&
+             pf->get_child(i + count)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
+             pf->get_child(i + count)->d_node.isNull();
              ++count) {
           Debug("pf::arith") << "Found a congruence: " << std::endl;
-          pf->d_children[i+count]->debug_print("pf::arith");
-          congruenceClosures.push_back(pf->d_children[i+count]);
+          pf->get_child(i+count)->debug_print("pf::arith");
+          congruenceClosures.push_back(pf->get_child(i+count));
         }
 
         Debug("pf::arith") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
@@ -133,9 +133,9 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
           targetAppearsBefore = false;
         }
 
-        if ((i + count >= pf->d_children.size()) ||
-            (!pf->d_children[i + count]->d_node.isNull() &&
-             pf->d_children[i + count]->d_node.getKind() == kind::NOT)) {
+        if ((i + count >= pf->num_children()) ||
+            (!pf->get_child(i + count)->d_node.isNull() &&
+             pf->get_child(i + count)->d_node.getKind() == kind::NOT)) {
           Debug("pf::arith") << "Target does not appear after" << std::endl;
           targetAppearsAfter = false;
         }
@@ -149,32 +149,32 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
 
         // Insert target clause first.
         if (targetAppearsBefore) {
-          orderedEqualities.push_back(pf->d_children[i - 1]);
+          orderedEqualities.push_back(pf->get_child(i - 1));
           // The target has already been added to subTrans; remove it.
-          subTrans.d_children.pop_back();
+          subTrans.remove_last_child();
         } else {
-          orderedEqualities.push_back(pf->d_children[i + count]);
+          orderedEqualities.push_back(pf->get_child(i + count));
         }
 
         // Start with the congruence closure closest to the target clause, and work our way back/forward.
         if (targetAppearsBefore) {
           for (unsigned j = 0; j < count; ++j) {
-            if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]);
-            if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-            orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]);
+            if (pf->get_child(i + j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + j)->get_child(0));
+            if (pf->get_child(i + j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+            orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + j)->get_child(1));
           }
         } else {
           for (unsigned j = 0; j < count; ++j) {
-            if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]);
-            if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]);
+            if (pf->get_child(i + count - 1 - j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + count - 1 - j)->get_child(0));
+            if (pf->get_child(i + count - 1 - j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + count - 1 - j)->get_child(1));
           }
         }
 
         // Copy the result into the main transitivity proof.
-        subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
+        subTrans.add_children(orderedEqualities);
 
         // Increase i to skip over the children that have been processed.
         i += count;
@@ -185,7 +185,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
 
       // Else, just copy the child proof as is
       else {
-        subTrans.d_children.push_back(pf->d_children[i]);
+        subTrans.add_child(pf->get_child(i));
         ++i;
       }
     }
@@ -193,16 +193,16 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
 
     Node n1;
     std::stringstream ss;
-    //Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
-    Debug("pf::arith") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
-    if(pf->d_children.size() > 2) {
+    //Assert(subTrans.num_children() == pf->num_children() - 1);
+    Debug("pf::arith") << "\nsubtrans has " << subTrans.num_children() << " children\n";
+    if(pf->num_children() > 2) {
       n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
     } else {
-      n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
-      Debug("pf::arith") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
+      n1 = toStreamRecLFSC(ss, tp, subTrans.get_child(0), 1, map);
+      Debug("pf::arith") << "\nsubTrans unique child " << subTrans.get_child(0)->d_id << " was proven\ngot: " << n1 << std::endl;
     }
 
-    Node n2 = pf->d_children[neg]->d_node;
+    Node n2 = pf->get_child(neg)->d_node;
     Assert(n2.getKind() == kind::NOT);
     out << "(clausify_false (contra _ ";
     Debug("pf::arith") << "\nhave proven: " << n1 << std::endl;
@@ -233,22 +233,22 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
     Debug("pf::arith") << "\nok, looking at congruence:\n";
     pf->debug_print("pf::arith");
     std::stack<const theory::eq::EqProof*> stk;
-    for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
+    for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->get_child(0)) {
       Assert(!pf2->d_node.isNull());
       Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE);
-      Assert(pf2->d_children.size() == 2);
+      Assert(pf2->num_children() == 2);
       out << "(cong _ _ _ _ _ _ ";
       stk.push(pf2);
     }
-    Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
+    Assert(stk.top()->get_child(0)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
     NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
     const theory::eq::EqProof* pf2 = stk.top();
     stk.pop();
     Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
-    Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map);
+    Node n1 = toStreamRecLFSC(out, tp, pf2->get_child(0), tb + 1, map);
     out << " ";
     std::stringstream ss;
-    Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map);
+    Node n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map);
     Debug("pf::arith") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
     pf2->debug_print("pf::arith");
     Debug("pf::arith") << "looking at " << pf2->d_node << "\n";
@@ -266,7 +266,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
       //}
       if(!match(pf2->d_node, n1[1])) {
       Debug("pf::arith") << "IN BAD CASE, our first subproof is\n";
-      pf2->d_children[0]->debug_print("pf::arith");
+      pf2->get_child(0)->debug_print("pf::arith");
       }
       Assert(match(pf2->d_node, n1[1]));
       side = 1;
@@ -316,7 +316,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
       Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
       out << " ";
       ss.str("");
-      n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map);
+      n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map);
       Debug("pf::arith") << "\nok, in cong[" << stk.size() << "]" << "\n";
       Debug("pf::arith") << "looking at " << pf2->d_node << "\n";
       Debug("pf::arith") << "           " << n1 << "\n";
@@ -374,7 +374,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
 
   case theory::eq::MERGED_THROUGH_REFLEXIVITY:
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     out << "(refl _ ";
     tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map);
     out << ")";
@@ -382,18 +382,18 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
 
   case theory::eq::MERGED_THROUGH_EQUALITY:
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     out << ProofManager::getLitName(pf->d_node.negate());
     return pf->d_node;
 
   case theory::eq::MERGED_THROUGH_TRANS: {
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.size() >= 2);
+    Assert(pf->num_children() >= 2);
     std::stringstream ss;
     Debug("pf::arith") << "\ndoing trans proof[[\n";
     pf->debug_print("pf::arith");
     Debug("pf::arith") << "\n";
-    Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
+    Node n1 = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map);
     Debug("pf::arith") << "\ndoing trans proof, got n1 " << n1 << "\n";
     if(tb == 1) {
       Debug("pf::arith") << "\ntrans proof[0], got n1 " << n1 << "\n";
@@ -405,7 +405,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
 
     std::map<size_t, Node> childToStream;
 
-    for(size_t i = 1; i < pf->d_children.size(); ++i) {
+    for(size_t i = 1; i < pf->num_children(); ++i) {
       std::stringstream ss1(ss.str()), ss2;
       ss.str("");
 
@@ -415,7 +415,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
       if (childToStream.find(i) != childToStream.end())
         n2 = childToStream[i];
       else {
-        n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map);
+        n2 = toStreamRecLFSC(ss2, tp, pf->get_child(i), tb + 1, map);
         childToStream[i] = n2;
       }
 
@@ -446,9 +446,9 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
             bool sequenceOver = false;
             size_t j = i + 1;
 
-            while (j < pf->d_children.size() && !sequenceOver) {
+            while (j < pf->num_children() && !sequenceOver) {
               std::stringstream dontCare;
-              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map );
+              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->get_child(j), tb + 1, map );
 
               if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) ||
                   ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) {
@@ -614,7 +614,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq
 
   default:
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     Debug("pf::arith") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl;
     AlwaysAssert(false);
     return pf->d_node;
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 6d1bd567d..371dda246 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -139,7 +139,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
   if(tb == 0) {
     Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS);
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.size() >= 2);
+    Assert(pf->num_children() >= 2);
 
     int neg = -1;
     theory::eq::EqProof subTrans;
@@ -147,19 +147,19 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     subTrans.d_node = pf->d_node;
 
     size_t i = 0;
-    while (i < pf->d_children.size()) {
-      if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
-        pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+    while (i < pf->num_children()) {
+      if (pf->get_child(i)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
+        pf->get_child(i)->d_node = simplifyBooleanNode(pf->get_child(i)->d_node);
 
       // Look for the negative clause, with which we will form a contradiction.
-      if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) {
+      if(!pf->get_child(i)->d_node.isNull() && pf->get_child(i)->d_node.getKind() == kind::NOT) {
         Assert(neg < 0);
         neg = i;
         ++i;
       }
 
       // Handle congruence closures over equalities.
-      else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) {
+      else if (pf->get_child(i)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->get_child(i)->d_node.isNull()) {
         Debug("pf::array") << "Handling congruence over equalities" << std::endl;
 
         // Gather the sequence of consecutive congruence closures.
@@ -167,13 +167,13 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         unsigned count;
         Debug("pf::array") << "Collecting congruence sequence" << std::endl;
         for (count = 0;
-             i + count < pf->d_children.size() &&
-               pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
-               pf->d_children[i + count]->d_node.isNull();
+             i + count < pf->num_children() &&
+               pf->get_child(i + count)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
+               pf->get_child(i + count)->d_node.isNull();
              ++count) {
           Debug("pf::array") << "Found a congruence: " << std::endl;
-          pf->d_children[i+count]->debug_print("pf::array", 0, &d_proofPrinter);
-          congruenceClosures.push_back(pf->d_children[i+count]);
+          pf->get_child(i+count)->debug_print("pf::array", 0, &d_proofPrinter);
+          congruenceClosures.push_back(pf->get_child(i+count));
         }
 
         Debug("pf::array") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
@@ -187,9 +187,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
           targetAppearsBefore = false;
         }
 
-        if ((i + count >= pf->d_children.size()) ||
-            (!pf->d_children[i + count]->d_node.isNull() &&
-             pf->d_children[i + count]->d_node.getKind() == kind::NOT)) {
+        if ((i + count >= pf->num_children()) ||
+            (!pf->get_child(i + count)->d_node.isNull() &&
+             pf->get_child(i + count)->d_node.getKind() == kind::NOT)) {
           Debug("pf::array") << "Target does not appear after" << std::endl;
           targetAppearsAfter = false;
         }
@@ -202,32 +202,32 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
         // Insert target clause first.
         if (targetAppearsBefore) {
-          orderedEqualities.push_back(pf->d_children[i - 1]);
+          orderedEqualities.push_back(pf->get_child(i - 1));
           // The target has already been added to subTrans; remove it.
-          subTrans.d_children.pop_back();
+          subTrans.remove_last_child();
         } else {
-          orderedEqualities.push_back(pf->d_children[i + count]);
+          orderedEqualities.push_back(pf->get_child(i + count));
         }
 
         // Start with the congruence closure closest to the target clause, and work our way back/forward.
         if (targetAppearsBefore) {
           for (unsigned j = 0; j < count; ++j) {
-            if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]);
-            if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]);
+            if (pf->get_child(i + j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + j)->get_child(0));
+            if (pf->get_child(i + j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + j)->get_child(1));
           }
         } else {
           for (unsigned j = 0; j < count; ++j) {
-            if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]);
-            if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]);
+            if (pf->get_child(i + count - 1 - j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + count - 1 - j)->get_child(0));
+            if (pf->get_child(i + count - 1 - j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + count - 1 - j)->get_child(1));
           }
         }
 
         // Copy the result into the main transitivity proof.
-        subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
+        subTrans.add_children(orderedEqualities);
 
         // Increase i to skip over the children that have been processed.
         i += count;
@@ -238,7 +238,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
       // Else, just copy the child proof as is
       else {
-        subTrans.d_children.push_back(pf->d_children[i]);
+        subTrans.add_child(pf->get_child(i));
         ++i;
       }
     }
@@ -254,34 +254,33 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
     Node n1;
     std::stringstream ss, ss2;
-    //Assert(subTrans.d_children.size() == pf->d_children.size() - 1);
-    Debug("mgdx") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
-    if(!disequalityFound || pf->d_children.size() > 2) {
+    Debug("mgdx") << "\nsubtrans has " << subTrans.num_children() << " children\n";
+    if(!disequalityFound || pf->num_children() > 2) {
       n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
     } else {
-      n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
-      Debug("mgdx") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
+      n1 = toStreamRecLFSC(ss, tp, subTrans.get_child(0), 1, map);
+      Debug("mgdx") << "\nsubTrans unique child " << subTrans.get_child(0)->d_id << " was proven\ngot: " << n1 << std::endl;
     }
 
     out << "(clausify_false (contra _ ";
 
     if (disequalityFound) {
-      Node n2 = pf->d_children[neg]->d_node;
+      Node n2 = pf->get_child(neg)->d_node;
       Assert(n2.getKind() == kind::NOT);
       Debug("mgdx") << "\nhave proven: " << n1 << std::endl;
       Debug("mgdx") << "n2 is " << n2 << std::endl;
-      Debug("mgdx") << "n2->d_id is " << pf->d_children[neg]->d_id << std::endl;
+      Debug("mgdx") << "n2->d_id is " << pf->get_child(neg)->d_id << std::endl;
       Debug("mgdx") << "n2[0] is " << n2[0] << std::endl;
 
       if (n2[0].getNumChildren() > 0) { Debug("mgdx") << "\nn2[0]: " << n2[0][0] << std::endl; }
       if (n1.getNumChildren() > 1) { Debug("mgdx") << "n1[1]: " << n1[1] << std::endl; }
 
-      if ((pf->d_children[neg]->d_id == d_reasonExt) ||
-          (pf->d_children[neg]->d_id == theory::eq::MERGED_THROUGH_TRANS)) {
+      if ((pf->get_child(neg)->d_id == d_reasonExt) ||
+          (pf->get_child(neg)->d_id == theory::eq::MERGED_THROUGH_TRANS)) {
         // Ext case: The negative node was created by an EXT rule; e.g. it is a[k]!=b[k], due to a!=b.
         out << ss.str();
         out << " ";
-        toStreamRecLFSC(ss2, tp, pf->d_children[neg], 1, map);
+        toStreamRecLFSC(ss2, tp, pf->get_child(neg), 1, map);
         out << ss2.str();
       } else if (n2[0].getKind() == kind::APPLY_UF) {
         out << "(trans _ _ _ _ ";
@@ -321,7 +320,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     Debug("mgd") << "\nok, looking at congruence:\n";
     pf->debug_print("mgd", 0, &d_proofPrinter);
     std::stack<const theory::eq::EqProof*> stk;
-    for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
+    for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->get_child(0)) {
       Debug("mgd") << "Looking at pf2 with d_node: " << pf2->d_node << std::endl;
 
       Assert(!pf2->d_node.isNull());
@@ -333,28 +332,28 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
              pf2->d_node.getKind() == kind::PARTIAL_SELECT_1 ||
              pf2->d_node.getKind() == kind::STORE);
 
-      Assert(pf2->d_children.size() == 2);
+      Assert(pf2->num_children() == 2);
       out << "(cong _ _ _ _ _ _ ";
       stk.push(pf2);
     }
-    Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
+    Assert(stk.top()->get_child(0)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
     //    NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
     NodeBuilder<> b1, b2;
 
     const theory::eq::EqProof* pf2 = stk.top();
     stk.pop();
     Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
-    Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map);
+    Node n1 = toStreamRecLFSC(out, tp, pf2->get_child(0), tb + 1, map);
     out << " ";
     std::stringstream ss;
-    Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map);
+    Node n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map);
 
 
     Debug("mgd") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
     pf2->debug_print("mgd", 0, &d_proofPrinter);
     // Temp
-    Debug("mgd") << "n1 is a proof for: " << pf2->d_children[0]->d_node << ". It is: " << n1 << std::endl;
-    Debug("mgd") << "n2 is a proof for: " << pf2->d_children[1]->d_node << ". It is: " << n2 << std::endl;
+    Debug("mgd") << "n1 is a proof for: " << pf2->get_child(0)->d_node << ". It is: " << n1 << std::endl;
+    Debug("mgd") << "n2 is a proof for: " << pf2->get_child(1)->d_node << ". It is: " << n2 << std::endl;
     //
     Debug("mgd") << "looking at " << pf2->d_node << "\n";
     Debug("mgd") << "           " << n1 << "\n";
@@ -368,7 +367,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       Debug("mgd") << "SIDE IS 1\n";
       if(!match(pf2->d_node, n1[1])) {
         Debug("mgd") << "IN BAD CASE, our first subproof is\n";
-        pf2->d_children[0]->debug_print("mgd", 0, &d_proofPrinter);
+        pf2->get_child(0)->debug_print("mgd", 0, &d_proofPrinter);
       }
       Assert(match(pf2->d_node, n1[1]));
       side = 1;
@@ -463,7 +462,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
       out << " ";
       ss.str("");
-      n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map);
+      n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map);
 
       Debug("mgd") << "\nok, in cong[" << stk.size() << "]" << "\n";
       Debug("mgd") << "looking at " << pf2->d_node << "\n";
@@ -566,7 +565,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
   else if (pf->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     out << "(refl _ ";
     tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map);
     out << ")";
@@ -575,7 +574,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
   else if (pf->d_id == theory::eq::MERGED_THROUGH_EQUALITY) {
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     Debug("pf::array") << "ArrayProof::toStream: getLitName( " << pf->d_node.negate() << " ) = " <<
       ProofManager::getLitName(pf->d_node.negate()) << std::endl;
     out << ProofManager::getLitName(pf->d_node.negate());
@@ -602,15 +601,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     bool secondNeg = false;
 
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.size() >= 2);
+    Assert(pf->num_children() >= 2);
     std::stringstream ss;
     Debug("mgd") << "\ndoing trans proof[[\n";
     pf->debug_print("mgd", 0, &d_proofPrinter);
     Debug("mgd") << "\n";
 
-    pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node);
+    pf->get_child(0)->d_node = simplifyBooleanNode(pf->get_child(0)->d_node);
 
-    Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
+    Node n1 = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map);
     Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n";
     if(tb == 1) {
       Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n";
@@ -622,7 +621,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
     std::map<size_t, Node> childToStream;
 
-    for(size_t i = 1; i < pf->d_children.size(); ++i) {
+    for(size_t i = 1; i < pf->num_children(); ++i) {
       std::stringstream ss1(ss.str()), ss2;
       ss.str("");
 
@@ -630,8 +629,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       // and not turn them into (a[x]=true), because that will mess up the congruence application
       // later.
 
-      if (pf->d_children[i]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
-        pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+      if (pf->get_child(i)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE)
+        pf->get_child(i)->d_node = simplifyBooleanNode(pf->get_child(i)->d_node);
 
       // It is possible that we've already converted the i'th child to stream. If so,
       // use previously stored result. Otherwise, convert and store.
@@ -639,7 +638,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       if (childToStream.find(i) != childToStream.end())
         n2 = childToStream[i];
       else {
-        n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map);
+        n2 = toStreamRecLFSC(ss2, tp, pf->get_child(i), tb + 1, map);
         childToStream[i] = n2;
       }
 
@@ -673,9 +672,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
             bool sequenceOver = false;
             size_t j = i + 1;
 
-            while (j < pf->d_children.size() && !sequenceOver) {
+            while (j < pf->num_children() && !sequenceOver) {
               std::stringstream dontCare;
-              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map );
+              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->get_child(j), tb + 1, map );
 
               if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) ||
                   ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) {
@@ -917,9 +916,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       // inner index != outer index
       // t3 is the outer index
 
-      Assert(pf->d_children.size() == 1);
+      Assert(pf->num_children() == 1);
       std::stringstream ss;
-      Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
+      Node subproof = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map);
 
       out << "(row _ _ ";
       tp->printTerm(t2.toExpr(), out, map);
@@ -932,7 +931,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       out << " ";
 
 
-      Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node
+      Debug("pf::array") << "pf->get_child(0)->d_node is: " << pf->get_child(0)->d_node
                          << ". t3 is: " << t3 << std::endl
                          << "subproof is: " << subproof << std::endl;
 
@@ -1005,7 +1004,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     } else {
       Debug("pf::array") << "In the case of NEGATIVE ROW" << std::endl;
 
-      Debug("pf::array") << "pf->d_children[0]->d_node is: " << pf->d_children[0]->d_node << std::endl;
+      Debug("pf::array") << "pf->get_child(0)->d_node is: " << pf->get_child(0)->d_node << std::endl;
 
       // This is the case where (i == k), and the sub-proof explains why ((a[i]:=t)[k] != a[k])
 
@@ -1022,15 +1021,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       t1 = pf->d_node[0];
       t2 = pf->d_node[1];
 
-      // pf->d_children[0]->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))),
+      // pf->get_child(0)->d_node will have the form: (not (= (select (store a_565 i7 e_566) i1) (select a_565 i1))),
       // or its symmetrical version.
 
       unsigned side;
-      if (pf->d_children[0]->d_node[0][0].getKind() == kind::SELECT &&
-          pf->d_children[0]->d_node[0][0][0].getKind() == kind::STORE) {
+      if (pf->get_child(0)->d_node[0][0].getKind() == kind::SELECT &&
+          pf->get_child(0)->d_node[0][0][0].getKind() == kind::STORE) {
         side = 0;
-      } else if (pf->d_children[0]->d_node[0][1].getKind() == kind::SELECT &&
-                 pf->d_children[0]->d_node[0][1][0].getKind() == kind::STORE) {
+      } else if (pf->get_child(0)->d_node[0][1].getKind() == kind::SELECT &&
+                 pf->get_child(0)->d_node[0][1][0].getKind() == kind::STORE) {
         side = 1;
       }
       else {
@@ -1040,18 +1039,18 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       Debug("pf::array") << "Side is: " << side << std::endl;
 
       // The array's index and element types will come from the subproof...
-      t3 = pf->d_children[0]->d_node[0][side][0][0];
-      t4 = pf->d_children[0]->d_node[0][side][0][2];
+      t3 = pf->get_child(0)->d_node[0][side][0][0];
+      t4 = pf->get_child(0)->d_node[0][side][0][2];
       ret = pf->d_node;
 
       // The order of indices needs to match; we might have to swap t1 and t2 and then apply symmetry.
-      bool swap = (t2 == pf->d_children[0]->d_node[0][side][0][1]);
+      bool swap = (t2 == pf->get_child(0)->d_node[0][side][0][1]);
 
       Debug("mgd") << "t1 " << t1 << "\nt2 " << t2 << "\nt3 " << t3 << "\nt4 " << t4 << "\n";
 
-      Assert(pf->d_children.size() == 1);
+      Assert(pf->num_children() == 1);
       std::stringstream ss;
-      Node subproof = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
+      Node subproof = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map);
 
       Debug("pf::array") << "Subproof is: " << ss.str() << std::endl;
 
@@ -1125,9 +1124,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
     Assert(pf->d_node.getKind() == kind::NOT);
     Assert(pf->d_node[0].getKind() == kind::EQUAL);
-    Assert(pf->d_children.size() == 1);
+    Assert(pf->num_children() == 1);
 
-    child_proof = pf->d_children[0];
+    child_proof = pf->get_child(0);
     Assert(child_proof->d_node.getKind() == kind::NOT);
     Assert(child_proof->d_node[0].getKind() == kind::EQUAL);
 
@@ -1151,7 +1150,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
 
   else {
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     Debug("mgd") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl;
     AlwaysAssert(false);
     return pf->d_node;
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
index c87ccd37c..376f3ce1d 100644
--- a/src/proof/proof_output_channel.cpp
+++ b/src/proof/proof_output_channel.cpp
@@ -16,6 +16,12 @@ namespace CVC4 {
 
 ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
 
+ProofOutputChannel::~ProofOutputChannel() {
+  if (d_proof != NULL) {
+    delete d_proof;
+  }
+}
+
 void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() {
   Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl;
   Assert(d_conflict.isNull());
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
index b44689fe5..f3ef572a1 100644
--- a/src/proof/proof_output_channel.h
+++ b/src/proof/proof_output_channel.h
@@ -16,13 +16,13 @@ namespace CVC4 {
 class ProofOutputChannel : public theory::OutputChannel {
 public:
   Node d_conflict;
+  // ProofOutputChannel owns d_proof
   Proof* d_proof;
   Node d_lemma;
   std::set<Node> d_propagations;
 
   ProofOutputChannel();
-
-  virtual ~ProofOutputChannel() throw() {}
+  virtual ~ProofOutputChannel();
 
   virtual void conflict(TNode n, Proof* pf) throw();
   virtual bool propagate(TNode x) throw();
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 9f77f3bdd..ca757b61f 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -236,6 +236,12 @@ template <class Solver>
 TSatProof<Solver>::~TSatProof() {
   delete d_proxy;
 
+  typename IdToConflicts::const_iterator debug_it = d_assumptionConflictsDebug.begin();
+  typename IdToConflicts::const_iterator debug_end = d_assumptionConflictsDebug.end();
+  for (; debug_it != debug_end; ++debug_it) {
+    delete debug_it->second;
+  }
+
   // FIXME: double free if deleted clause also appears in d_seenLemmas?
   IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin();
   IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end();
@@ -267,16 +273,6 @@ TSatProof<Solver>::~TSatProof() {
   for (; resolution_it != resolution_it_end; ++resolution_it) {
     delete *resolution_it;
   }
-
-  // It could be the case that d_resStack is not empty at destruction time
-  // (for example in the SAT case).
-  typename ResStack::const_iterator resolution_stack_it = d_resStack.begin();
-  typename ResStack::const_iterator resolution_stack_it_end = d_resStack.end();
-  for (; resolution_stack_it != resolution_stack_it_end;
-       ++resolution_stack_it) {
-    ResChain<Solver>* current = *resolution_stack_it;
-    delete current;
-  }
 }
 
 template <class Solver>
@@ -807,6 +803,7 @@ template <class Solver>
 void TSatProof<Solver>::cancelResChain() {
   Assert(d_resStack.size() > 0);
   ResolutionChain* back = d_resStack.back();
+  d_existingResolutionChains.erase(back);
   delete back;
   d_resStack.pop_back();
 }
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index cea873b6d..e150ab5ca 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -66,6 +66,9 @@ inline static bool match(TNode n1, TNode n2) {
   return true;
 }
 
+ProofUF::~ProofUF() {
+  delete d_proof;
+}
 
 void ProofUF::toStream(std::ostream& out) {
   ProofLetMap map;
@@ -103,7 +106,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
     Assert(pf->d_id == theory::eq::MERGED_THROUGH_TRANS);
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.size() >= 2);
+    Assert(pf->num_children() >= 2);
 
     int neg = -1;
     theory::eq::EqProof subTrans;
@@ -112,19 +115,19 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
     size_t i = 0;
 
-    while (i < pf->d_children.size()) {
-      pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+    while (i < pf->num_children()) {
+      pf->get_child(i)->d_node = simplifyBooleanNode(pf->get_child(i)->d_node);
 
       // Look for the negative clause, with which we will form a contradiction.
-      if(!pf->d_children[i]->d_node.isNull() && pf->d_children[i]->d_node.getKind() == kind::NOT) {
+      if(!pf->get_child(i)->d_node.isNull() && pf->get_child(i)->d_node.getKind() == kind::NOT) {
         Assert(neg < 0);
-        Node node = pf->d_children[i]->d_node[0];
+        Node node = pf->get_child(i)->d_node[0];
         neg = i;
         ++i;
       }
 
       // Handle congruence closures over equalities.
-      else if (pf->d_children[i]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->d_children[i]->d_node.isNull()) {
+      else if (pf->get_child(i)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE && pf->get_child(i)->d_node.isNull()) {
         Debug("pf::uf") << "Handling congruence over equalities" << std::endl;
 
         // Gather the sequence of consecutive congruence closures.
@@ -132,13 +135,13 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
         unsigned count;
         Debug("pf::uf") << "Collecting congruence sequence" << std::endl;
         for (count = 0;
-             i + count < pf->d_children.size() &&
-               pf->d_children[i + count]->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
-               pf->d_children[i + count]->d_node.isNull();
+             i + count < pf->num_children() &&
+               pf->get_child(i + count)->d_id==theory::eq::MERGED_THROUGH_CONGRUENCE &&
+               pf->get_child(i + count)->d_node.isNull();
              ++count) {
           Debug("pf::uf") << "Found a congruence: " << std::endl;
-          pf->d_children[i+count]->debug_print("pf::uf");
-          congruenceClosures.push_back(pf->d_children[i+count]);
+          pf->get_child(i+count)->debug_print("pf::uf");
+          congruenceClosures.push_back(pf->get_child(i+count));
         }
 
         Debug("pf::uf") << "Total number of congruences found: " << congruenceClosures.size() << std::endl;
@@ -152,9 +155,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
           targetAppearsBefore = false;
         }
 
-        if ((i + count >= pf->d_children.size()) ||
-            (!pf->d_children[i + count]->d_node.isNull() &&
-             pf->d_children[i + count]->d_node.getKind() == kind::NOT)) {
+        if ((i + count >= pf->num_children()) ||
+            (!pf->get_child(i + count)->d_node.isNull() &&
+             pf->get_child(i + count)->d_node.getKind() == kind::NOT)) {
           Debug("pf::uf") << "Target does not appear after" << std::endl;
           targetAppearsAfter = false;
         }
@@ -171,32 +174,32 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
         // Insert target clause first.
         if (targetAppearsBefore) {
-          orderedEqualities.push_back(pf->d_children[i - 1]);
+          orderedEqualities.push_back(pf->get_child(i - 1));
           // The target has already been added to subTrans; remove it.
-          subTrans.d_children.pop_back();
+          subTrans.remove_last_child();
         } else {
-          orderedEqualities.push_back(pf->d_children[i + count]);
+          orderedEqualities.push_back(pf->get_child(i + count));
         }
 
         // Start with the congruence closure closest to the target clause, and work our way back/forward.
         if (targetAppearsBefore) {
           for (unsigned j = 0; j < count; ++j) {
-            if (pf->d_children[i + j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + j]->d_children[0]);
-            if (pf->d_children[i + j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + j]->d_children[1]);
+            if (pf->get_child(i + j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + j)->get_child(0));
+            if (pf->get_child(i + j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + j)->get_child(1));
           }
         } else {
           for (unsigned j = 0; j < count; ++j) {
-            if (pf->d_children[i + count - 1 - j]->d_children[0]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.begin(), pf->d_children[i + count - 1 - j]->d_children[0]);
-            if (pf->d_children[i + count - 1 - j]->d_children[1]->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
-              orderedEqualities.insert(orderedEqualities.end(), pf->d_children[i + count - 1 - j]->d_children[1]);
+            if (pf->get_child(i + count - 1 - j)->get_child(0)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.begin(), pf->get_child(i + count - 1 - j)->get_child(0));
+            if (pf->get_child(i + count - 1 - j)->get_child(1)->d_id != theory::eq::MERGED_THROUGH_REFLEXIVITY)
+              orderedEqualities.insert(orderedEqualities.end(), pf->get_child(i + count - 1 - j)->get_child(1));
           }
         }
 
         // Copy the result into the main transitivity proof.
-        subTrans.d_children.insert(subTrans.d_children.end(), orderedEqualities.begin(), orderedEqualities.end());
+        subTrans.add_children(orderedEqualities);
 
         // Increase i to skip over the children that have been processed.
         i += count;
@@ -207,7 +210,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
       // Else, just copy the child proof as is
       else {
-        subTrans.d_children.push_back(pf->d_children[i]);
+        subTrans.add_child(pf->get_child(i));
         ++i;
       }
     }
@@ -223,13 +226,13 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
     Node n1;
     std::stringstream ss;
-    Debug("pf::uf") << "\nsubtrans has " << subTrans.d_children.size() << " children\n";
+    Debug("pf::uf") << "\nsubtrans has " << subTrans.num_children() << " children\n";
 
-    if(!disequalityFound || subTrans.d_children.size() >= 2) {
+    if(!disequalityFound || subTrans.num_children() >= 2) {
       n1 = toStreamRecLFSC(ss, tp, &subTrans, 1, map);
     } else {
-      n1 = toStreamRecLFSC(ss, tp, subTrans.d_children[0], 1, map);
-      Debug("pf::uf") << "\nsubTrans unique child " << subTrans.d_children[0]->d_id << " was proven\ngot: " << n1 << std::endl;
+      n1 = toStreamRecLFSC(ss, tp, subTrans.get_child(0), 1, map);
+      Debug("pf::uf") << "\nsubTrans unique child " << subTrans.get_child(0)->d_id << " was proven\ngot: " << n1 << std::endl;
     }
 
     Debug("pf::uf") << "\nhave proven: " << n1 << std::endl;
@@ -237,7 +240,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
     out << "(clausify_false (contra _ ";
 
     if (disequalityFound) {
-      Node n2 = pf->d_children[neg]->d_node;
+      Node n2 = pf->get_child(neg)->d_node;
       Assert(n2.getKind() == kind::NOT);
 
       Debug("pf::uf") << "n2 is " << n2[0] << std::endl;
@@ -287,22 +290,22 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
     Debug("pf::uf") << "\nok, looking at congruence:\n";
     pf->debug_print("pf::uf");
     std::stack<const theory::eq::EqProof*> stk;
-    for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->d_children[0]) {
+    for(const theory::eq::EqProof* pf2 = pf; pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE; pf2 = pf2->get_child(0)) {
       Assert(!pf2->d_node.isNull());
       Assert(pf2->d_node.getKind() == kind::PARTIAL_APPLY_UF || pf2->d_node.getKind() == kind::BUILTIN || pf2->d_node.getKind() == kind::APPLY_UF || pf2->d_node.getKind() == kind::SELECT || pf2->d_node.getKind() == kind::STORE);
-      Assert(pf2->d_children.size() == 2);
+      Assert(pf2->num_children() == 2);
       out << "(cong _ _ _ _ _ _ ";
       stk.push(pf2);
     }
-    Assert(stk.top()->d_children[0]->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
+    Assert(stk.top()->get_child(0)->d_id != theory::eq::MERGED_THROUGH_CONGRUENCE);
     NodeBuilder<> b1(kind::PARTIAL_APPLY_UF), b2(kind::PARTIAL_APPLY_UF);
     const theory::eq::EqProof* pf2 = stk.top();
     stk.pop();
     Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
-    Node n1 = toStreamRecLFSC(out, tp, pf2->d_children[0], tb + 1, map);
+    Node n1 = toStreamRecLFSC(out, tp, pf2->get_child(0), tb + 1, map);
     out << " ";
     std::stringstream ss;
-    Node n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map);
+    Node n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map);
     Debug("pf::uf") << "\nok, in FIRST cong[" << stk.size() << "]" << "\n";
     pf2->debug_print("pf::uf");
     Debug("pf::uf") << "looking at " << pf2->d_node << "\n";
@@ -320,7 +323,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       //}
       if(!match(pf2->d_node, n1[1])) {
         Debug("pf::uf") << "IN BAD CASE, our first subproof is\n";
-        pf2->d_children[0]->debug_print("pf::uf");
+        pf2->get_child(0)->debug_print("pf::uf");
       }
       Assert(match(pf2->d_node, n1[1]));
       side = 1;
@@ -370,7 +373,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       Assert(pf2->d_id == theory::eq::MERGED_THROUGH_CONGRUENCE);
       out << " ";
       ss.str("");
-      n2 = toStreamRecLFSC(ss, tp, pf2->d_children[1], tb + 1, map);
+      n2 = toStreamRecLFSC(ss, tp, pf2->get_child(1), tb + 1, map);
       Debug("pf::uf") << "\nok, in cong[" << stk.size() << "]" << "\n";
       Debug("pf::uf") << "looking at " << pf2->d_node << "\n";
       Debug("pf::uf") << "           " << n1 << "\n";
@@ -428,7 +431,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
   case theory::eq::MERGED_THROUGH_REFLEXIVITY:
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     out << "(refl _ ";
     tp->printTerm(NodeManager::currentNM()->toExpr(pf->d_node), out, map);
     out << ")";
@@ -436,21 +439,21 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
   case theory::eq::MERGED_THROUGH_EQUALITY:
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     out << ProofManager::getLitName(pf->d_node.negate());
     return pf->d_node;
 
   case theory::eq::MERGED_THROUGH_TRANS: {
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.size() >= 2);
+    Assert(pf->num_children() >= 2);
     std::stringstream ss;
     Debug("pf::uf") << "\ndoing trans proof[[\n";
     pf->debug_print("pf::uf");
     Debug("pf::uf") << "\n";
 
-    pf->d_children[0]->d_node = simplifyBooleanNode(pf->d_children[0]->d_node);
+    pf->get_child(0)->d_node = simplifyBooleanNode(pf->get_child(0)->d_node);
 
-    Node n1 = toStreamRecLFSC(ss, tp, pf->d_children[0], tb + 1, map);
+    Node n1 = toStreamRecLFSC(ss, tp, pf->get_child(0), tb + 1, map);
     Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n";
     if(tb == 1) {
       Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n";
@@ -462,11 +465,11 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
     std::map<size_t, Node> childToStream;
 
-    for(size_t i = 1; i < pf->d_children.size(); ++i) {
+    for(size_t i = 1; i < pf->num_children(); ++i) {
       std::stringstream ss1(ss.str()), ss2;
       ss.str("");
 
-      pf->d_children[i]->d_node = simplifyBooleanNode(pf->d_children[i]->d_node);
+      pf->get_child(i)->d_node = simplifyBooleanNode(pf->get_child(i)->d_node);
 
       // It is possible that we've already converted the i'th child to stream. If so,
       // use previously stored result. Otherwise, convert and store.
@@ -474,7 +477,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
       if (childToStream.find(i) != childToStream.end())
         n2 = childToStream[i];
       else {
-        n2 = toStreamRecLFSC(ss2, tp, pf->d_children[i], tb + 1, map);
+        n2 = toStreamRecLFSC(ss2, tp, pf->get_child(i), tb + 1, map);
         childToStream[i] = n2;
       }
 
@@ -505,9 +508,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
             bool sequenceOver = false;
             size_t j = i + 1;
 
-            while (j < pf->d_children.size() && !sequenceOver) {
+            while (j < pf->num_children() && !sequenceOver) {
               std::stringstream dontCare;
-              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->d_children[j], tb + 1, map );
+              nodeAfterEqualitySequence = toStreamRecLFSC(dontCare, tp, pf->get_child(j), tb + 1, map );
 
               if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) ||
                   ((nodeAfterEqualitySequence[0] == n1[1]) && (nodeAfterEqualitySequence[1] == n1[0]))) {
@@ -707,7 +710,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E
 
   default:
     Assert(!pf->d_node.isNull());
-    Assert(pf->d_children.empty());
+    Assert(pf->num_children() == 0);
     Debug("pf::uf") << "theory proof: " << pf->d_node << " by rule " << int(pf->d_id) << std::endl;
     AlwaysAssert(false);
     return pf->d_node;
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index c4bd28dc5..bfc242ea8 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -31,6 +31,8 @@ private:
   static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
 public:
   ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {}
+  ~ProofUF();
+
   //it is simply an equality engine proof
   theory::eq::EqProof * d_proof;
   void toStream(std::ostream& out);
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 5ecccdd53..56cfd501f 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -50,7 +50,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
       // recursively, to explain this.
       eq::EqProof* childProof = new eq::EqProof;
       childProof->d_node = reason;
-      proof->d_children.push_back(childProof);
+      proof->add_child(childProof);
     }
   }
 
@@ -108,40 +108,40 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
         // It could be that the guard condition is a constant disequality. In this case,
         // we need to change it to a different format.
         bool haveNegChild = false;
-        for (unsigned i = 0; i < childProof->d_children.size(); ++i) {
-          if (childProof->d_children[i]->d_node.getKind() == kind::NOT)
+        for (unsigned i = 0; i < childProof->num_children(); ++i) {
+          if (childProof->get_child(i)->d_node.getKind() == kind::NOT)
             haveNegChild = true;
         }
 
-        if ((childProof->d_children.size() != 0) &&
+        if ((childProof->num_children() != 0) &&
             (childProof->d_id == theory::eq::MERGED_THROUGH_CONSTANTS || !haveNegChild)) {
           // The proof has two children, explaining why each index is a (different) constant.
-          Assert(childProof->d_children.size() == 2);
+          Assert(childProof->num_children() == 2);
 
           Node constantOne, constantTwo;
           // Each subproof explains why one of the indices is constant.
 
-          if (childProof->d_children[0]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
-            constantOne = childProof->d_children[0]->d_node;
+          if (childProof->get_child(0)->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
+            constantOne = childProof->get_child(0)->d_node;
           } else {
-            Assert(childProof->d_children[0]->d_node.getKind() == kind::EQUAL);
-            if ((childProof->d_children[0]->d_node[0] == indexOne) ||
-                (childProof->d_children[0]->d_node[0] == indexTwo)) {
-              constantOne = childProof->d_children[0]->d_node[1];
+            Assert(childProof->get_child(0)->d_node.getKind() == kind::EQUAL);
+            if ((childProof->get_child(0)->d_node[0] == indexOne) ||
+                (childProof->get_child(0)->d_node[0] == indexTwo)) {
+              constantOne = childProof->get_child(0)->d_node[1];
             } else {
-              constantOne = childProof->d_children[0]->d_node[0];
+              constantOne = childProof->get_child(0)->d_node[0];
             }
           }
 
-          if (childProof->d_children[1]->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
-            constantTwo = childProof->d_children[1]->d_node;
+          if (childProof->get_child(1)->d_id == theory::eq::MERGED_THROUGH_REFLEXIVITY) {
+            constantTwo = childProof->get_child(1)->d_node;
           } else {
-            Assert(childProof->d_children[1]->d_node.getKind() == kind::EQUAL);
-            if ((childProof->d_children[1]->d_node[0] == indexOne) ||
-                (childProof->d_children[1]->d_node[0] == indexTwo)) {
-              constantTwo = childProof->d_children[1]->d_node[1];
+            Assert(childProof->get_child(1)->d_node.getKind() == kind::EQUAL);
+            if ((childProof->get_child(1)->d_node[0] == indexOne) ||
+                (childProof->get_child(1)->d_node[0] == indexTwo)) {
+              constantTwo = childProof->get_child(1)->d_node[1];
             } else {
-              constantTwo = childProof->d_children[1]->d_node[0];
+              constantTwo = childProof->get_child(1)->d_node[0];
             }
           }
 
@@ -150,18 +150,15 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
           constantDisequalityProof->d_node =
             NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
 
-          // Middle is where we need to insert the new disequality
-          std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin();
-          ++middle;
-
-          childProof->d_children.insert(middle, constantDisequalityProof);
+          // We need to insert the new disequality at position 1
+          childProof->insert_child(1, constantDisequalityProof);
 
           childProof->d_id = theory::eq::MERGED_THROUGH_TRANS;
           childProof->d_node =
             NodeManager::currentNM()->mkNode(kind::EQUAL, indexOne, indexTwo).negate();
         }
 
-        proof->d_children.push_back(childProof);
+        proof->add_child(childProof);
       } else {
         // This is the case of (i == k) because ((a[i]:=t)[k] != a[k]),
 
@@ -176,7 +173,7 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
 
         eq::EqProof* childProof = new eq::EqProof;
         d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false, equalities, childProof);
-        proof->d_children.push_back(childProof);
+        proof->add_child(childProof);
       }
     }
 
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index f7084bec3..7a6e0bdfc 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -963,41 +963,41 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
         if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) {
           std::vector<EqProof *> orderedChildren;
           bool nullCongruenceFound = false;
-          for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
-            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE &&
-                eqpc->d_children[i]->d_node.isNull()) {
+          for (unsigned i = 0; i < eqpc->num_children(); ++i) {
+            if (eqpc->get_child(i)->d_id==eq::MERGED_THROUGH_CONGRUENCE &&
+                eqpc->get_child(i)->d_node.isNull()) {
               nullCongruenceFound = true;
               Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl;
-              orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]);
-              orderedChildren.push_back(eqpc->d_children[i]->d_children[1]);
+              orderedChildren.insert(orderedChildren.begin(), eqpc->get_child(i)->get_child(0));
+              orderedChildren.push_back(eqpc->get_child(i)->get_child(1));
             } else {
-              orderedChildren.push_back(eqpc->d_children[i]);
+              orderedChildren.push_back(eqpc->get_child(i));
             }
           }
 
           if (nullCongruenceFound) {
-            eqpc->d_children = orderedChildren;
+            eqpc->add_children(orderedChildren);
             Debug("pf::ee") << "Child proof's children have been reordered. It is now:" << std::endl;
             eqpc->debug_print("pf::ee", 1);
           }
         }
 
-        eqp->d_children.push_back(eqpc);
+        eqp->add_child(eqpc);
       }
     }
 
     if (eqp) {
-      if (eqp->d_children.size() == 0) {
+      if (eqp->num_children() == 0) {
         // Corner case where this is actually a disequality between two constants
         Debug("pf::ee") << "Encountered a constant disequality (not a transitivity proof): "
                         << eqp->d_node << std::endl;
         Assert(eqp->d_node[0][0].isConst());
         Assert(eqp->d_node[0][1].isConst());
         eqp->d_id = MERGED_THROUGH_CONSTANTS;
-      } else if (eqp->d_children.size() == 1) {
+      } else if (eqp->num_children() == 1) {
         // The transitivity proof has just one child. Simplify.
-        EqProof* temp = eqp->d_children[0];
-        eqp->d_children.clear();
+        EqProof* temp = eqp->get_child(0);
+        eqp->remove_all_children();
         *eqp = *temp;
         delete temp;
       }
@@ -1126,8 +1126,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               EqProof * eqpc2 = eqpc ? new EqProof : NULL;
               getExplanation(f1.b, f2.b, equalities, eqpc2);
               if( eqpc ){
-                eqpc->d_children.push_back( eqpc1 );
-                eqpc->d_children.push_back( eqpc2 );
+                eqpc->add_child( eqpc1 );
+                eqpc->add_child( eqpc2 );
                 if( d_nodes[currentNode].getKind()==kind::EQUAL ){
                   //leave node null for now
                   eqpc->d_node = Node::null();
@@ -1141,10 +1141,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
                       eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]);
                       // The first child is a PARTIAL_SELECT_0.
                       // Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
-                      Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0);
-                      Assert(eqpc->d_children[0]->d_children.size() == 0);
+                      Assert(eqpc->get_child(0)->d_node.getKind() == kind::PARTIAL_SELECT_0);
+                      Assert(eqpc->get_child(0)->num_children() == 0);
 
-                      eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0,
+                      eqpc->get_child(0)->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0,
                                                                                      d_nodes[f1.b]);
                     } else {
                       eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF,
@@ -1170,7 +1170,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               EqProof * eqpc1 = eqpc ? new EqProof : NULL;
               getExplanation(eq.a, eq.b, equalities, eqpc1);
               if( eqpc ){
-                eqpc->d_children.push_back( eqpc1 );
+                eqpc->add_child( eqpc1 );
               }
               Debug("equality") << pop;
 
@@ -1195,7 +1195,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
                 EqProof * eqpcc = eqpc ? new EqProof : NULL;
                 getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc);
                 if( eqpc ) {
-                  eqpc->d_children.push_back( eqpcc );
+                  eqpc->add_child( eqpcc );
 
                   Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl;
                   eqpc->debug_print("pf::ee", 1);
@@ -1248,12 +1248,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             //---from Morgan---
             if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
               if(eqpc->d_node.isNull()) {
-                Assert(eqpc->d_children.size() == 1);
+                Assert(eqpc->num_children() == 1);
                 EqProof *p = eqpc;
-                eqpc = p->d_children[0];
+                eqpc = p->take_child(0);
+                p->discard_children();
                 delete p;
               } else {
-                Assert(eqpc->d_children.empty());
+                Assert(eqpc->num_children() == 0);
               }
             }
             //---end from Morgan---
@@ -1264,10 +1265,11 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
           if (eqp) {
             if(eqp_trans.size() == 1) {
               *eqp = *eqp_trans[0];
+              eqp_trans[0]->discard_children();
               delete eqp_trans[0];
             } else {
               eqp->d_id = MERGED_THROUGH_TRANS;
-              eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
+              eqp->add_children(eqp_trans);
               eqp->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]);
             }
 
@@ -2217,6 +2219,11 @@ bool EqClassIterator::isFinished() const {
   return d_current == null_id;
 }
 
+EqProof::~EqProof() {
+Assert(this->refs == 0);
+this->remove_all_children();
+}
+
 void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const {
   for(unsigned i=0; i<tb; i++) { Debug( c ) << "  "; }
 
@@ -2232,10 +2239,10 @@ void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrint
       for( unsigned i=0; i<tb+1; i++ ) { Debug( c ) << "  "; }
       Debug( c ) << d_node;
     }
-    for( unsigned i=0; i<d_children.size(); i++ ){
+    for( unsigned i=0; i<num_children(); i++ ){
       if( i>0 || !d_node.isNull() ) Debug( c ) << ",";
       Debug( c ) << std::endl;
-      d_children[i]->debug_print( c, tb+1, prettyPrinter );
+      get_child(i)->debug_print( c, tb+1, prettyPrinter );
     }
   }
   Debug( c ) << ")" << std::endl;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 46ec7403b..2354aa76e 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -901,6 +901,9 @@ public:
 
 class EqProof
 {
+private:
+  std::vector< EqProof * > d_children;
+
 public:
   class PrettyPrinter {
   public:
@@ -908,10 +911,55 @@ public:
     virtual std::string printTag(unsigned tag) = 0;
   };
 
-  EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
+  EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY), refs(0) {}
+  ~EqProof();
   unsigned d_id;
+  unsigned refs;
   Node d_node;
-  std::vector< EqProof * > d_children;
+  void add_child(EqProof* child) {
+   child->refs++;
+   d_children.push_back(child);
+  }
+  void insert_child(size_t i, EqProof* child) {
+   child->refs++;
+   std::vector<eq::EqProof *>::iterator middle = d_children.begin();
+   middle += i;
+   d_children.insert(middle, child);
+  }
+  void add_children(const std::vector<EqProof*> children) {
+    for (size_t i = 0; i < children.size(); i++) {
+      this->add_child(children[i]);
+    }
+  }
+  void remove_all_children() {
+  for( unsigned i=0; i<d_children.size(); i++ ){
+    d_children[i]->refs--;
+    if (d_children[i]->refs == 0) {
+    delete d_children[i];
+}
+  }
+  }
+  void discard_children() {
+    d_children.clear();
+  }
+  void remove_last_child() {
+    EqProof* last_child = d_children[d_children.size() - 1];
+    last_child->refs--;
+    if (last_child->refs == 0) {
+      delete last_child;
+    }
+    d_children.pop_back();
+  }
+  size_t num_children() const {
+    return d_children.size();
+  }
+  EqProof* get_child(size_t n) const {
+    return d_children[n];
+  }
+  EqProof* take_child(size_t i) {
+   d_children[i]->refs--;
+return d_children[i];
+  }
   void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const;
 };/* class EqProof */