5 files changed, 35 insertions, 31 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 041a4e6a..3dbb5a66 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -414,10 +414,6 @@ cl::opt<bool> DebugCheckForImpliedValues(
 
 } // namespace
 
-namespace klee {
-  RNG theRNG;
-}
-
 // XXX hack
 extern "C" unsigned dumpStates, dumpPTree;
 unsigned dumpStates = 0, dumpPTree = 0;
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 31882cd4..25a874cd 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -18,6 +18,7 @@
 #include "ExecutionState.h"
 #include "UserSearcher.h"
 
+#include "klee/ADT/RNG.h"
 #include "klee/Core/Interpreter.h"
 #include "klee/Expr/ArrayCache.h"
 #include "klee/Expr/ArrayExprOptimizer.h"
@@ -111,6 +112,9 @@ public:
     Unhandled
   };
 
+  /// The random number generator.
+  RNG theRNG;
+
 private:
   static const char *TerminateReasonNames[];
 
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 765784c5..d6cf8dfd 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -41,10 +41,6 @@ using namespace klee;
 using namespace llvm;
 
 
-namespace klee {
-  extern RNG theRNG;
-}
-
 Searcher::~Searcher() {
 }
 
@@ -166,9 +162,10 @@ RandomSearcher::update(ExecutionState *current,
 
 ///
 
-WeightedRandomSearcher::WeightedRandomSearcher(WeightType _type)
+WeightedRandomSearcher::WeightedRandomSearcher(WeightType type, RNG &rng)
   : states(new DiscretePDF<ExecutionState*>()),
-    type(_type) {
+    theRNG{rng},
+    type(type) {
   switch(type) {
   case Depth:
   case RP:
@@ -261,8 +258,10 @@ bool WeightedRandomSearcher::empty() {
   return states->empty(); 
 }
 
-RandomPathSearcher::RandomPathSearcher(PTree &_processTree)
-    : processTree(_processTree), idBitMask(_processTree.getNextId()) {}
+///
+RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng)
+  : processTree{processTree}, theRNG{rng}, idBitMask{processTree.getNextId()} {
+}
 
 RandomPathSearcher::~RandomPathSearcher() {
 }
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index baeafd84..fa0440b8 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -11,6 +11,7 @@
 #define KLEE_SEARCHER_H
 
 #include "PTree.h"
+#include "klee/ADT/RNG.h"
 #include "klee/System/Time.h"
 
 #include "llvm/Support/CommandLine.h"
@@ -116,8 +117,10 @@ namespace klee {
 
   class RandomSearcher : public Searcher {
     std::vector<ExecutionState*> states;
+    RNG &theRNG;
 
   public:
+    explicit RandomSearcher(RNG &rng) : theRNG{rng} {}
     ExecutionState &selectState();
     void update(ExecutionState *current,
                 const std::vector<ExecutionState *> &addedStates,
@@ -142,13 +145,14 @@ namespace klee {
 
   private:
     DiscretePDF<ExecutionState*> *states;
+    RNG &theRNG;
     WeightType type;
     bool updateWeights;
     
     double getWeight(ExecutionState*);
 
   public:
-    WeightedRandomSearcher(WeightType type);
+    WeightedRandomSearcher(WeightType type, RNG &rng);
     ~WeightedRandomSearcher();
 
     ExecutionState &selectState();
@@ -191,12 +195,13 @@ namespace klee {
   */
   class RandomPathSearcher : public Searcher {
     PTree &processTree;
+    RNG &theRNG;
 
     // Unique bitmask of this searcher
     const uint8_t idBitMask;
 
   public:
-    RandomPathSearcher(PTree &processTree);
+    RandomPathSearcher(PTree &processTree, RNG &rng);
     ~RandomPathSearcher();
 
     ExecutionState &selectState();
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index 42d6b334..7acca58e 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -104,22 +104,21 @@ bool klee::userSearcherRequiresMD2U() {
 	  std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end());
 }
 
-Searcher *getNewSearcher(Searcher::CoreSearchType type, PTree &processTree) {
-  Searcher *searcher = NULL;
+
+Searcher *getNewSearcher(Searcher::CoreSearchType type, RNG &rng, PTree &processTree) {
+  Searcher *searcher = nullptr;
   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(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;
-  case Searcher::NURS_RP: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::RP); break;
-  case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::InstCount); break;
-  case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CPInstCount); break;
-  case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::QueryCost); break;
+    case Searcher::DFS: searcher = new DFSSearcher(); break;
+    case Searcher::BFS: searcher = new BFSSearcher(); break;
+    case Searcher::RandomState: searcher = new RandomSearcher(rng); break;
+    case Searcher::RandomPath: searcher = new RandomPathSearcher(processTree, rng); break;
+    case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew, rng); break;
+    case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered, rng); break;
+    case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth, rng); break;
+    case Searcher::NURS_RP: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::RP, rng); break;
+    case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::InstCount, rng); break;
+    case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CPInstCount, rng); break;
+    case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::QueryCost, rng); break;
   }
 
   return searcher;
@@ -127,13 +126,14 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, PTree &processTree) {
 
 Searcher *klee::constructUserSearcher(Executor &executor) {
 
-  Searcher *searcher = getNewSearcher(CoreSearch[0], *executor.processTree);
+  Searcher *searcher = getNewSearcher(CoreSearch[0], executor.theRNG, *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.processTree));
+      s.push_back(getNewSearcher(CoreSearch[i], executor.theRNG, *executor.processTree));
 
     searcher = new InterleavedSearcher(s);
   }