7 files changed, 16 insertions, 22 deletions
diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h
index 9a527bcd..1e5ffc2e 100644
--- a/include/klee/util/ArrayExprHash.h
+++ b/include/klee/util/ArrayExprHash.h
@@ -132,4 +132,4 @@ void ArrayExprHash<T>::hashUpdateNodeExpr(const UpdateNode* un, T& exp)
 
 }
 
-#endif
\ No newline at end of file
+#endif
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 2dbabd01..8c3e26bc 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -157,10 +157,8 @@ void RandomSearcher::update(ExecutionState *current,
 
 ///
 
-WeightedRandomSearcher::WeightedRandomSearcher(Executor &_executor,
-                                               WeightType _type) 
-  : executor(_executor),
-    states(new DiscretePDF<ExecutionState*>()),
+WeightedRandomSearcher::WeightedRandomSearcher(WeightType _type)
+  : states(new DiscretePDF<ExecutionState*>()),
     type(_type) {
   switch(type) {
   case Depth: 
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 79c233c4..3944d4b4 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -135,7 +135,6 @@ namespace klee {
     };
 
   private:
-    Executor &executor;
     DiscretePDF<ExecutionState*> *states;
     WeightType type;
     bool updateWeights;
@@ -143,7 +142,7 @@ namespace klee {
     double getWeight(ExecutionState*);
 
   public:
-    WeightedRandomSearcher(Executor &executor, WeightType type);
+    WeightedRandomSearcher(WeightType type);
     ~WeightedRandomSearcher();
 
     ExecutionState &selectState();
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index a20ae968..2c75f796 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -81,12 +81,12 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) {
   case Searcher::BFS: searcher = new BFSSearcher(); break;
   case Searcher::RandomState: searcher = new RandomSearcher(); break;
   case Searcher::RandomPath: searcher = new RandomPathSearcher(executor); break;
-  case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CoveringNew); break;
-  case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::MinDistToUncovered); break;
-  case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::Depth); break;
-  case Searcher::NURS_ICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::InstCount); break;
-  case Searcher::NURS_CPICnt: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::CPInstCount); break;
-  case Searcher::NURS_QC: searcher = new WeightedRandomSearcher(executor, WeightedRandomSearcher::QueryCost); 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_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;
   }
 
   return searcher;
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index c61b6b1c..025c70f2 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -494,8 +494,6 @@ Solver *klee::createDummySolver() {
 
 class STPSolverImpl : public SolverImpl {
 private:
-  /// The solver we are part of, for access to public information.
-  STPSolver *solver;
   VC vc;
   STPBuilder *builder;
   double timeout;
@@ -503,7 +501,7 @@ private:
   SolverRunStatus runStatusCode;
 
 public:
-  STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true);
+  STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true);
   ~STPSolverImpl();
   
   char *getConstraintLog(const Query&);
@@ -527,9 +525,8 @@ static void stp_error_handler(const char* err_msg) {
   abort();
 }
 
-STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides)
-  : solver(_solver),
-    vc(vc_createValidityChecker()),
+STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
+  : vc(vc_createValidityChecker()),
     builder(new STPBuilder(vc, _optimizeDivides)),
     timeout(0.0),
     useForkedSTP(_useForkedSTP),
@@ -566,7 +563,7 @@ STPSolverImpl::~STPSolverImpl() {
 /***/
 
 STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
-  : Solver(new STPSolverImpl(this, useForkedSTP, optimizeDivides))
+  : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides))
 {
 }
 
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 39ba8fdb..656ffeae 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -29,7 +29,7 @@ ifeq ($(ENABLE_METASMT),1)
               -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib 
   CXX.Flags += -DBOOST_HAS_GCC_TR1
   CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) 
-  LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core
+  LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lrt -lboolector -lminisat_core
 endif
 
 ifeq ($(STP_NEEDS_BOOST),1)
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index ce5a21e6..e526f2a2 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -30,7 +30,7 @@ ifeq ($(ENABLE_METASMT),1)
               -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib 
   CXX.Flags += -DBOOST_HAS_GCC_TR1
   CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) 
-  LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core
+  LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lrt -lboolector -lminisat_core
 endif
 
 ifeq ($(STP_NEEDS_BOOST),1)