1 files changed, 12 insertions, 10 deletions

diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
index 6c10e0cc..26de37fb 100644
--- a/lib/Core/PTree.cpp
+++ b/lib/Core/PTree.cpp
@@ -19,15 +19,16 @@
 using namespace klee;
 
 PTree::PTree(ExecutionState *initialState) {
-  root = std::make_unique<PTreeNode>(nullptr, initialState);
+  root = new PTreeNode(nullptr, initialState);
+  initialState->ptreeNode = root;
 }
 
 void PTree::attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState) {
   assert(node && !node->left && !node->right);
 
   node->state = nullptr;
-  node->left = std::make_unique<PTreeNode>(node, leftState);
-  node->right = std::make_unique<PTreeNode>(node, rightState);
+  node->left = new PTreeNode(node, leftState);
+  node->right = new PTreeNode(node, rightState);
 }
 
 void PTree::remove(PTreeNode *n) {
@@ -35,13 +36,14 @@ void PTree::remove(PTreeNode *n) {
   do {
     PTreeNode *p = n->parent;
     if (p) {
-      if (n == p->left.get()) {
+      if (n == p->left) {
         p->left = nullptr;
       } else {
-        assert(n == p->right.get());
+        assert(n == p->right);
         p->right = nullptr;
       }
     }
+    delete n;
     n = p;
   } while (n && !n->left && !n->right);
 }
@@ -57,7 +59,7 @@ void PTree::dump(llvm::raw_ostream &os) {
   os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n";
   os << "\tedge [arrowsize=.3]\n";
   std::vector<const PTreeNode*> stack;
-  stack.push_back(root.get());
+  stack.push_back(root);
   while (!stack.empty()) {
     const PTreeNode *n = stack.back();
     stack.pop_back();
@@ -66,12 +68,12 @@ void PTree::dump(llvm::raw_ostream &os) {
       os << ",fillcolor=green";
     os << "];\n";
     if (n->left) {
-      os << "\tn" << n << " -> n" << n->left.get() << ";\n";
-      stack.push_back(n->left.get());
+      os << "\tn" << n << " -> n" << n->left << ";\n";
+      stack.push_back(n->left);
     }
     if (n->right) {
-      os << "\tn" << n << " -> n" << n->right.get() << ";\n";
-      stack.push_back(n->right.get());
+      os << "\tn" << n << " -> n" << n->right << ";\n";
+      stack.push_back(n->right);
     }
   }
   os << "}\n";