Enable subsets for RandomPathSearcher

11 files changed, 350 insertions, 32 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 7b600003..14d596fc 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -105,7 +105,6 @@ ExecutionState::ExecutionState(const ExecutionState& state):
     pathOS(state.pathOS),
     symPathOS(state.symPathOS),
     coveredLines(state.coveredLines),
-    ptreeNode(state.ptreeNode),
     symbolics(state.symbolics),
     arrayNames(state.arrayNames),
     openMergeStack(state.openMergeStack),
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index e7332472..f1b09644 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -111,7 +111,8 @@ public:
   std::map<const std::string *, std::set<std::uint32_t>> coveredLines;
 
   /// @brief Pointer to the process tree of the current state
-  PTreeNode *ptreeNode;
+  /// Copies of ExecutionState should not copy ptreeNode
+  PTreeNode *ptreeNode = nullptr;
 
   /// @brief Ordered list of symbolics: used to generate test cases.
   //
@@ -144,6 +145,10 @@ public:
   bool forkDisabled;
 
 public:
+  #ifdef KLEE_UNITTEST
+  // provide this function only in the context of unittests
+  ExecutionState(){}
+  #endif
   // only to create the initial state
   explicit ExecutionState(KFunction *kf);
   // XXX total hack, just used to make a state so solver can
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index d27fa503..31882cd4 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -16,6 +16,7 @@
 #define KLEE_EXECUTOR_H
 
 #include "ExecutionState.h"
+#include "UserSearcher.h"
 
 #include "klee/Core/Interpreter.h"
 #include "klee/Expr/ArrayCache.h"
@@ -84,12 +85,12 @@ namespace klee {
   /// removedStates, and haltExecution, among others.
 
 class Executor : public Interpreter {
-  friend class RandomPathSearcher;
   friend class OwningSearcher;
   friend class WeightedRandomSearcher;
   friend class SpecialFunctionHandler;
   friend class StatsTracker;
   friend class MergeHandler;
+  friend klee::Searcher *klee::constructUserSearcher(Executor &executor);
 
 public:
   typedef std::pair<ExecutionState*,ExecutionState*> StatePair;
diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
index 2962e3c2..244e8520 100644
--- a/lib/Core/PTree.cpp
+++ b/lib/Core/PTree.cpp
@@ -14,20 +14,29 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprPPrinter.h"
 
+#include <bitset>
 #include <vector>
 
 using namespace klee;
 
-PTree::PTree(ExecutionState *initialState) {
-  root = new PTreeNode(nullptr, initialState);
-  initialState->ptreeNode = root;
+PTree::PTree(ExecutionState *initialState)
+    : root(PTreeNodePtr(new PTreeNode(nullptr, initialState))) {
+  initialState->ptreeNode = root.getPointer();
 }
 
 void PTree::attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState) {
   assert(node && !node->left.getPointer() && !node->right.getPointer());
+  assert(node == rightState->ptreeNode &&
+         "Attach assumes the right state is the current state");
   node->state = nullptr;
   node->left = PTreeNodePtr(new PTreeNode(node, leftState));
-  node->right = PTreeNodePtr(new PTreeNode(node, rightState));
+  // The current node inherits the tag
+  uint8_t currentNodeTag = root.getInt();
+  if (node->parent)
+    currentNodeTag = node->parent->left.getPointer() == node
+                         ? node->parent->left.getInt()
+                         : node->parent->right.getInt();
+  node->right = PTreeNodePtr(new PTreeNode(node, rightState), currentNodeTag);
 }
 
 void PTree::remove(PTreeNode *n) {
@@ -58,7 +67,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);
+  stack.push_back(root.getPointer());
   while (!stack.empty()) {
     const PTreeNode *n = stack.back();
     stack.pop_back();
@@ -67,11 +76,15 @@ void PTree::dump(llvm::raw_ostream &os) {
       os << ",fillcolor=green";
     os << "];\n";
     if (n->left.getPointer()) {
-      os << "\tn" << n << " -> n" << n->left.getPointer() << ";\n";
+      os << "\tn" << n << " -> n" << n->left.getPointer();
+      os << " [label=0b"
+         << std::bitset<PtrBitCount>(n->left.getInt()).to_string() << "];\n";
       stack.push_back(n->left.getPointer());
     }
     if (n->right.getPointer()) {
-      os << "\tn" << n << " -> n" << n->right.getPointer() << ";\n";
+      os << "\tn" << n << " -> n" << n->right.getPointer();
+      os << " [label=0b"
+         << std::bitset<PtrBitCount>(n->right.getInt()).to_string() << "];\n";
       stack.push_back(n->right.getPointer());
     }
   }
diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index 115ea83f..b1b6e9fc 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -11,13 +11,19 @@
 #define KLEE_PTREE_H
 
 #include "klee/Expr/Expr.h"
+#include "klee/Support/ErrorHandling.h"
 #include "llvm/ADT/PointerIntPair.h"
 
 namespace klee {
   class ExecutionState;
   class PTreeNode;
-  using PTreeNodePtr = llvm::PointerIntPair<PTreeNode*,3,uint8_t>;
-
+  /* PTreeNodePtr is used by the Random Path Searcher object to efficiently
+  record which PTreeNode belongs to it. PTree is a global structure that
+  captures all  states, whereas a Random Path Searcher might only care about
+  a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which
+  Random Path Searchers PTreeNode belongs to. */
+  constexpr int PtrBitCount = 3;
+  using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>;
 
   class PTreeNode {
   public:
@@ -33,14 +39,26 @@ namespace klee {
   };
 
   class PTree {
+    // Number of registered ID
+    int registeredIds = 0;
+
   public:
-    PTreeNode * root = nullptr;
+    PTreeNodePtr root;
     explicit PTree(ExecutionState *initialState);
     ~PTree() = default;
 
-    static void attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState);
+    void attach(PTreeNode *node, ExecutionState *leftState,
+                ExecutionState *rightState);
     static void remove(PTreeNode *node);
     void dump(llvm::raw_ostream &os);
+    std::uint8_t getNextId() {
+      std::uint8_t id = 1 << registeredIds++;
+      if (registeredIds > PtrBitCount) {
+        klee_error("PTree cannot support more than %d RandomPathSearchers",
+                   PtrBitCount);
+      }
+      return id;
+    }
   };
 }
 
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 27a92b49..6b7e9e49 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -259,21 +259,29 @@ bool WeightedRandomSearcher::empty() {
   return states->empty(); 
 }
 
-///
-RandomPathSearcher::RandomPathSearcher(Executor &_executor)
-  : executor(_executor) {
-}
+RandomPathSearcher::RandomPathSearcher(PTree &_processTree)
+    : processTree(_processTree), idBitMask(_processTree.getNextId()) {}
 
 RandomPathSearcher::~RandomPathSearcher() {
 }
+// Check if n is a valid pointer and a node belonging to us
+#define IS_OUR_NODE_VALID(n)                                                   \
+  (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0))
 
 ExecutionState &RandomPathSearcher::selectState() {
   unsigned flips=0, bits=0;
-  PTreeNode *n = executor.processTree->root;
+  assert(processTree.root.getInt() & idBitMask &&
+         "Root should belong to the searcher");
+  PTreeNode *n = processTree.root.getPointer();
   while (!n->state) {
-    if (!n->left.getPointer()) {
+    if (!IS_OUR_NODE_VALID(n->left)) {
+      assert(IS_OUR_NODE_VALID(n->right) &&
+             "Both left and right nodes invalid");
+      assert(n != n->right.getPointer());
       n = n->right.getPointer();
-    } else if (!n->right.getPointer()) {
+    } else if (!IS_OUR_NODE_VALID(n->right)) {
+      assert(IS_OUR_NODE_VALID(n->left) && "Both right and left nodes invalid");
+      assert(n != n->left.getPointer());
       n = n->left.getPointer();
     } else {
       if (bits==0) {
@@ -281,7 +289,7 @@ ExecutionState &RandomPathSearcher::selectState() {
         bits = 32;
       }
       --bits;
-      n = (flips&(1<<bits)) ? n->left.getPointer() : n->right.getPointer();
+      n = ((flips & (1 << bits)) ? n->left : n->right).getPointer();
     }
   }
 
@@ -292,10 +300,46 @@ void
 RandomPathSearcher::update(ExecutionState *current,
                            const std::vector<ExecutionState *> &addedStates,
                            const std::vector<ExecutionState *> &removedStates) {
+  for (auto es : addedStates) {
+    PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
+    PTreeNodePtr *childPtr;
+
+    childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left
+                                                              : &parent->right)
+                      : &processTree.root;
+    while (pnode && !IS_OUR_NODE_VALID(*childPtr)) {
+      childPtr->setInt(childPtr->getInt() | idBitMask);
+      pnode = parent;
+      if (pnode)
+        parent = pnode->parent;
+
+      childPtr = parent
+                     ? ((parent->left.getPointer() == pnode) ? &parent->left
+                                                             : &parent->right)
+                     : &processTree.root;
+    }
+  }
+
+  for (auto es : removedStates) {
+    PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
+
+    while (pnode && !IS_OUR_NODE_VALID(pnode->left) &&
+           !IS_OUR_NODE_VALID(pnode->right)) {
+      auto childPtr =
+          parent ? ((parent->left.getPointer() == pnode) ? &parent->left
+                                                         : &parent->right)
+                 : &processTree.root;
+      assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours");
+      childPtr->setInt(childPtr->getInt() & ~idBitMask);
+      pnode = parent;
+      if (pnode)
+        parent = pnode->parent;
+    }
+  }
 }
 
-bool RandomPathSearcher::empty() { 
-  return executor.states.empty(); 
+bool RandomPathSearcher::empty() {
+  return !IS_OUR_NODE_VALID(processTree.root);
 }
 
 ///
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index b369057b..baeafd84 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_SEARCHER_H
 #define KLEE_SEARCHER_H
 
+#include "PTree.h"
 #include "klee/System/Time.h"
 
 #include "llvm/Support/CommandLine.h"
@@ -170,11 +171,32 @@ namespace klee {
     }
   };
 
+  /* RandomPathSearcher performs a random walk of the PTree to
+     select a state. PTree is a global data structure, however
+     a searcher can sometimes only select from a subset of all states
+     (depending on the update calls).
+
+     To support this RandomPathSearcher has a subgraph view of PTree, in that it
+     only
+     walks the PTreeNodes that it "owns". Ownership is stored in the
+     getInt method of PTreeNodePtr class (which hides it in the pointer itself).
+
+     The current implementation of PTreeNodePtr supports only 3 instances of the
+     RandomPathSearcher. This is because current PTreeNodePtr implementation
+     conforms to C++ and only steals the last 3 alligment bits. This restriction
+     could be relaxed  slightly by an architecture specific implementation of
+     PTreeNodePtr, that also steals the top bits of the pointer.
+
+     The ownership bits are maintained in the update method.
+  */
   class RandomPathSearcher : public Searcher {
-    Executor &executor;
+    PTree &processTree;
+
+    // Unique bitmask of this searcher
+    const uint8_t idBitMask;
 
   public:
-    RandomPathSearcher(Executor &_executor);
+    RandomPathSearcher(PTree &processTree);
     ~RandomPathSearcher();
 
     ExecutionState &selectState();
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 8dc32a40..42d6b334 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -104,14 +104,15 @@ bool klee::userSearcherRequiresMD2U() {
 	  std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end());
 }
 
-
-Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
+Searcher *getNewSearcher(Searcher::CoreSearchType type, PTree &processTree) {
   Searcher *searcher = NULL;
   switch (type) {
   case Searcher::DFS: searcher = new DFSSearcher(); break;
   case Searcher::BFS: searcher = new BFSSearcher(); break;
   case Searcher::RandomState: searcher = new RandomSearcher(); break;
-  case Searcher::RandomPath: searcher = new RandomPathSearcher(executor); break;
+  case Searcher::RandomPath:
+    searcher = new RandomPathSearcher(processTree);
+    break;
   case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew); break;
   case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered); break;
   case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth); break;
@@ -126,14 +127,13 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
 
 Searcher *klee::constructUserSearcher(Executor &executor) {
 
-  Searcher *searcher = getNewSearcher(CoreSearch[0], executor);
-
+  Searcher *searcher = getNewSearcher(CoreSearch[0], *executor.processTree);
   if (CoreSearch.size() > 1) {
     std::vector<Searcher *> s;
     s.push_back(searcher);
 
     for (unsigned i = 1; i < CoreSearch.size(); i++)
-      s.push_back(getNewSearcher(CoreSearch[i], executor));
+      s.push_back(getNewSearcher(CoreSearch[i], *executor.processTree));
 
     searcher = new InterleavedSearcher(s);
   }
diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt
index ef052f9b..75c4d892 100644
--- a/unittests/CMakeLists.txt
+++ b/unittests/CMakeLists.txt
@@ -166,6 +166,7 @@ add_subdirectory(Assignment)
 add_subdirectory(Expr)
 add_subdirectory(Ref)
 add_subdirectory(Solver)
+add_subdirectory(Searcher)
 add_subdirectory(TreeStream)
 add_subdirectory(DiscretePDF)
 add_subdirectory(Time)
diff --git a/unittests/Searcher/CMakeLists.txt b/unittests/Searcher/CMakeLists.txt
new file mode 100644
index 00000000..29358470
--- /dev/null
+++ b/unittests/Searcher/CMakeLists.txt
@@ -0,0 +1,4 @@
+add_klee_unit_test(SearcherTest
+  SearcherTest.cpp)
+target_link_libraries(SearcherTest PRIVATE kleeCore)
+target_include_directories(SearcherTest BEFORE PUBLIC "../../lib")
diff --git a/unittests/Searcher/SearcherTest.cpp b/unittests/Searcher/SearcherTest.cpp
new file mode 100644
index 00000000..e9e7c043
--- /dev/null
+++ b/unittests/Searcher/SearcherTest.cpp
@@ -0,0 +1,211 @@
+//===-- SearcherTest.cpp ----------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#define KLEE_UNITTEST
+
+#include "gtest/gtest.h"
+
+#include "Core/ExecutionState.h"
+#include "Core/PTree.h"
+#include "Core/Searcher.h"
+#include "llvm/Support/raw_ostream.h"
+
+using namespace klee;
+
+namespace {
+
+TEST(SearcherTest, RandomPath) {
+  // First state
+  ExecutionState es;
+  PTree processTree(&es);
+  es.ptreeNode = processTree.root.getPointer();
+
+  RandomPathSearcher rp(processTree);
+  EXPECT_TRUE(rp.empty());
+
+  rp.update(nullptr, {&es}, {});
+  EXPECT_FALSE(rp.empty());
+  EXPECT_EQ(&rp.selectState(), &es);
+
+  // Two states
+  ExecutionState es1(es);
+  processTree.attach(es.ptreeNode, &es1, &es);
+  rp.update(&es, {&es1}, {});
+
+  // Random path seed dependant
+  EXPECT_EQ(&rp.selectState(), &es1);
+  EXPECT_EQ(&rp.selectState(), &es);
+  EXPECT_EQ(&rp.selectState(), &es1);
+
+  rp.update(&es, {}, {&es1});
+  for (int i = 0; i < 100; i++) {
+    EXPECT_EQ(&rp.selectState(), &es);
+  }
+
+  rp.update(&es, {&es1}, {&es});
+  processTree.remove(es.ptreeNode);
+  for (int i = 0; i < 100; i++) {
+    EXPECT_EQ(&rp.selectState(), &es1);
+  }
+
+  rp.update(&es1, {}, {&es1});
+  processTree.remove(es1.ptreeNode);
+  EXPECT_TRUE(rp.empty());
+}
+
+TEST(SearcherTest, TwoRandomPath) {
+  // Root state
+  ExecutionState root;
+  PTree processTree(&root);
+  root.ptreeNode = processTree.root.getPointer();
+
+  ExecutionState es(root);
+  processTree.attach(root.ptreeNode, &es, &root);
+
+  RandomPathSearcher rp(processTree);
+  RandomPathSearcher rp1(processTree);
+  EXPECT_TRUE(rp.empty());
+  EXPECT_TRUE(rp1.empty());
+
+  rp.update(nullptr, {&es}, {});
+  EXPECT_FALSE(rp.empty());
+  EXPECT_TRUE(rp1.empty());
+  EXPECT_EQ(&rp.selectState(), &es);
+
+  // Two states
+  ExecutionState es1(es);
+  processTree.attach(es.ptreeNode, &es1, &es);
+
+  rp.update(&es, {}, {});
+  rp1.update(nullptr, {&es1}, {});
+  EXPECT_FALSE(rp1.empty());
+
+  for (int i = 0; i < 100; i++) {
+    EXPECT_EQ(&rp.selectState(), &es);
+    EXPECT_EQ(&rp1.selectState(), &es1);
+  }
+
+  rp.update(&es, {&es1}, {&es});
+  rp1.update(nullptr, {&es}, {&es1});
+
+  for (int i = 0; i < 100; i++) {
+    EXPECT_EQ(&rp1.selectState(), &es);
+    EXPECT_EQ(&rp.selectState(), &es1);
+  }
+
+  rp1.update(&es, {}, {&es});
+  processTree.remove(es.ptreeNode);
+  EXPECT_TRUE(rp1.empty());
+  EXPECT_EQ(&rp.selectState(), &es1);
+
+  rp.update(&es1, {}, {&es1});
+  processTree.remove(es1.ptreeNode);
+  EXPECT_TRUE(rp.empty());
+  EXPECT_TRUE(rp1.empty());
+
+  processTree.remove(root.ptreeNode);
+}
+
+TEST(SearcherTest, TwoRandomPathDot) {
+  std::stringstream modelPTreeDot;
+  PTreeNode *rootPNode, *rightLeafPNode, *esParentPNode, *es1LeafPNode,
+      *esLeafPNode;
+
+  // Root state
+  ExecutionState root;
+  PTree processTree(&root);
+  root.ptreeNode = processTree.root.getPointer();
+  rootPNode = root.ptreeNode;
+
+  ExecutionState es(root);
+  processTree.attach(root.ptreeNode, &es, &root);
+  rightLeafPNode = root.ptreeNode;
+  esParentPNode = es.ptreeNode;
+
+  RandomPathSearcher rp(processTree);
+  RandomPathSearcher rp1(processTree);
+
+  rp.update(nullptr, {&es}, {});
+
+  ExecutionState es1(es);
+  processTree.attach(es.ptreeNode, &es1, &es);
+  esLeafPNode = es.ptreeNode;
+  es1LeafPNode = es1.ptreeNode;
+
+  rp.update(&es, {}, {});
+  rp1.update(nullptr, {&es1}, {});
+
+  // Compare PTree to model PTree
+  modelPTreeDot
+      << "digraph G {\n"
+      << "\tsize=\"10,7.5\";\n"
+      << "\tratio=fill;\n"
+      << "\trotate=90;\n"
+      << "\tcenter = \"true\";\n"
+      << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"
+      << "\tedge [arrowsize=.3]\n"
+      << "\tn" << rootPNode << " [shape=diamond];\n"
+      << "\tn" << rootPNode << " -> n" << esParentPNode << " [label=0b011];\n"
+      << "\tn" << rootPNode << " -> n" << rightLeafPNode << " [label=0b000];\n"
+      << "\tn" << rightLeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << esParentPNode << " [shape=diamond];\n"
+      << "\tn" << esParentPNode << " -> n" << es1LeafPNode
+      << " [label=0b010];\n"
+      << "\tn" << esParentPNode << " -> n" << esLeafPNode << " [label=0b001];\n"
+      << "\tn" << esLeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << es1LeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "}\n";
+  std::string pTreeDot;
+  llvm::raw_string_ostream pTreeDotStream(pTreeDot);
+  processTree.dump(pTreeDotStream);
+  EXPECT_EQ(modelPTreeDot.str(), pTreeDotStream.str());
+
+  rp.update(&es, {&es1}, {&es});
+  rp1.update(nullptr, {&es}, {&es1});
+
+  rp1.update(&es, {}, {&es});
+  processTree.remove(es.ptreeNode);
+
+  modelPTreeDot.str("");
+  modelPTreeDot
+      << "digraph G {\n"
+      << "\tsize=\"10,7.5\";\n"
+      << "\tratio=fill;\n"
+      << "\trotate=90;\n"
+      << "\tcenter = \"true\";\n"
+      << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"
+      << "\tedge [arrowsize=.3]\n"
+      << "\tn" << rootPNode << " [shape=diamond];\n"
+      << "\tn" << rootPNode << " -> n" << esParentPNode << " [label=0b001];\n"
+      << "\tn" << rootPNode << " -> n" << rightLeafPNode << " [label=0b000];\n"
+      << "\tn" << rightLeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "\tn" << esParentPNode << " [shape=diamond];\n"
+      << "\tn" << esParentPNode << " -> n" << es1LeafPNode
+      << " [label=0b001];\n"
+      << "\tn" << es1LeafPNode << " [shape=diamond,fillcolor=green];\n"
+      << "}\n";
+
+  pTreeDot = "";
+  processTree.dump(pTreeDotStream);
+  EXPECT_EQ(modelPTreeDot.str(), pTreeDotStream.str());
+  processTree.remove(es1.ptreeNode);
+  processTree.remove(root.ptreeNode);
+}
+TEST(SearcherDeathTest, TooManyRandomPaths) {
+  // First state
+  ExecutionState es;
+  PTree processTree(&es);
+  es.ptreeNode = processTree.root.getPointer();
+  processTree.remove(es.ptreeNode); // Need to remove to avoid leaks
+
+  RandomPathSearcher rp(processTree);
+  RandomPathSearcher rp1(processTree);
+  RandomPathSearcher rp2(processTree);
+  ASSERT_DEATH({ RandomPathSearcher rp3(processTree); }, "");
+}
+}