2 files changed, 4 insertions, 3 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index d6cf8dfd..32a1e1bd 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -163,7 +163,7 @@ RandomSearcher::update(ExecutionState *current,
 ///
 
 WeightedRandomSearcher::WeightedRandomSearcher(WeightType type, RNG &rng)
-  : states(new DiscretePDF<ExecutionState*>()),
+  : states(new DiscretePDF<ExecutionState*, ExecutionStateIDCompare>()),
     theRNG{rng},
     type(type) {
   switch(type) {
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index fa0440b8..437cf01f 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_SEARCHER_H
 #define KLEE_SEARCHER_H
 
+#include "ExecutionState.h"
 #include "PTree.h"
 #include "klee/ADT/RNG.h"
 #include "klee/System/Time.h"
@@ -30,7 +31,7 @@ namespace llvm {
 }
 
 namespace klee {
-  template<class T> class DiscretePDF;
+  template<class T, class Comparator> class DiscretePDF;
   class ExecutionState;
   class Executor;
 
@@ -144,7 +145,7 @@ namespace klee {
     };
 
   private:
-    DiscretePDF<ExecutionState*> *states;
+    DiscretePDF<ExecutionState*, ExecutionStateIDCompare> *states;
     RNG &theRNG;
     WeightType type;
     bool updateWeights;