3 files changed, 19 insertions, 17 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";
diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index 01632ebf..6456b57f 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -18,8 +18,8 @@ namespace klee {
   class PTreeNode {
   public:
     PTreeNode *parent = nullptr;
-    std::unique_ptr<PTreeNode> left;
-    std::unique_ptr<PTreeNode> right;
+    PTreeNode *left = nullptr;
+    PTreeNode *right = nullptr;
     ExecutionState *state = nullptr;
 
     PTreeNode(const PTreeNode&) = delete;
@@ -29,7 +29,7 @@ namespace klee {
 
   class PTree {
   public:
-    std::unique_ptr<PTreeNode> root;
+    PTreeNode * root = nullptr;
     explicit PTree(ExecutionState *initialState);
     ~PTree() = default;
 
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index a9c7d318..0a1e6152 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -269,19 +269,19 @@ RandomPathSearcher::~RandomPathSearcher() {
 
 ExecutionState &RandomPathSearcher::selectState() {
   unsigned flips=0, bits=0;
-  PTreeNode *n = executor.processTree->root.get();
+  PTreeNode *n = executor.processTree->root;
   while (!n->state) {
     if (!n->left) {
-      n = n->right.get();
+      n = n->right;
     } else if (!n->right) {
-      n = n->left.get();
+      n = n->left;
     } else {
       if (bits==0) {
         flips = theRNG.getInt32();
         bits = 32;
       }
       --bits;
-      n = (flips&(1<<bits)) ? n->left.get() : n->right.get();
+      n = (flips&(1<<bits)) ? n->left : n->right;
     }
   }