use unique_ptr all throughout the solver chain

29 files changed, 213 insertions, 167 deletions

diff --git a/include/klee/Solver/Common.h b/include/klee/Solver/Common.h
index 7b244158..626ea55a 100644
--- a/include/klee/Solver/Common.h
+++ b/include/klee/Solver/Common.h
@@ -24,13 +24,10 @@ namespace klee {
     const char ALL_QUERIES_KQUERY_FILE_NAME[]="all-queries.kquery";
     const char SOLVER_QUERIES_KQUERY_FILE_NAME[]="solver-queries.kquery";
 
-    Solver *constructSolverChain(Solver *coreSolver,
-                                 std::string querySMT2LogPath,
-                                 std::string baseSolverQuerySMT2LogPath,
-                                 std::string queryKQueryLogPath,
-                                 std::string baseSolverQueryKQueryLogPath);
-}
-
-
+std::unique_ptr<Solver> constructSolverChain(
+    std::unique_ptr<Solver> coreSolver, std::string querySMT2LogPath,
+    std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath,
+    std::string baseSolverQueryKQueryLogPath);
+} // namespace klee
 
 #endif /* KLEE_COMMON_H */
diff --git a/include/klee/Solver/IncompleteSolver.h b/include/klee/Solver/IncompleteSolver.h
index b8ef1929..8bcf7f88 100644
--- a/include/klee/Solver/IncompleteSolver.h
+++ b/include/klee/Solver/IncompleteSolver.h
@@ -91,10 +91,11 @@ class StagedSolverImpl : public SolverImpl {
 private:
   std::unique_ptr<IncompleteSolver> primary;
   std::unique_ptr<Solver> secondary;
-  
+
 public:
-  StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary);
-    
+  StagedSolverImpl(std::unique_ptr<IncompleteSolver> primary,
+                   std::unique_ptr<Solver> secondary);
+
   bool computeTruth(const Query&, bool &isValid);
   bool computeValidity(const Query&, Solver::Validity &result);
   bool computeValue(const Query&, ref<Expr> &result);
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
index 2689d19c..c50b17d8 100644
--- a/include/klee/Solver/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -71,7 +71,7 @@ namespace klee {
 
     std::unique_ptr<SolverImpl> impl;
 
-    Solver(SolverImpl *impl);
+    Solver(std::unique_ptr<SolverImpl> impl);
     virtual ~Solver();
 
     /// evaluate - Determine for a particular state if the query
@@ -215,19 +215,22 @@ namespace klee {
   ///
   /// \param s - The primary underlying solver to use.
   /// \param oracle - The solver to check query results against.
-  Solver *createValidatingSolver(Solver *s, Solver *oracle, bool ownsOracle = false);
+  std::unique_ptr<Solver> createValidatingSolver(std::unique_ptr<Solver> s,
+                                                 Solver *oracle,
+                                                 bool ownsOracle);
 
   /// createAssignmentValidatingSolver - Create a solver that when requested
   /// for an assignment will check that the computed assignment satisfies
   /// the Query.
   /// \param s - The underlying solver to use.
-  Solver *createAssignmentValidatingSolver(Solver *s);
+  std::unique_ptr<Solver>
+  createAssignmentValidatingSolver(std::unique_ptr<Solver> s);
 
   /// createCachingSolver - Create a solver which will cache the queries in
   /// memory (without eviction).
   ///
   /// \param s - The underlying solver to use.
-  Solver *createCachingSolver(Solver *s);
+  std::unique_ptr<Solver> createCachingSolver(std::unique_ptr<Solver> s);
 
   /// createCexCachingSolver - Create a counterexample caching solver. This is a
   /// more sophisticated cache which records counterexamples for a constraint
@@ -235,41 +238,40 @@ namespace klee {
   /// quickly find satisfying assignments.
   ///
   /// \param s - The underlying solver to use.
-  Solver *createCexCachingSolver(Solver *s);
+  std::unique_ptr<Solver> createCexCachingSolver(std::unique_ptr<Solver> s);
 
   /// createFastCexSolver - Create a "fast counterexample solver", which tries
   /// to quickly compute a satisfying assignment for a constraint set using
   /// value propogation and range analysis.
   ///
   /// \param s - The underlying solver to use.
-  Solver *createFastCexSolver(Solver *s);
+  std::unique_ptr<Solver> createFastCexSolver(std::unique_ptr<Solver> s);
 
   /// createIndependentSolver - Create a solver which will eliminate any
   /// unnecessary constraints before propogating the query to the underlying
   /// solver.
   ///
   /// \param s - The underlying solver to use.
-  Solver *createIndependentSolver(Solver *s);
-  
+  std::unique_ptr<Solver> createIndependentSolver(std::unique_ptr<Solver> s);
+
   /// createKQueryLoggingSolver - Create a solver which will forward all queries
   /// after writing them to the given path in .kquery format.
-  Solver *createKQueryLoggingSolver(Solver *s, std::string path,
-                                    time::Span minQueryTimeToLog,
-                                    bool logTimedOut);
+  std::unique_ptr<Solver>
+  createKQueryLoggingSolver(std::unique_ptr<Solver> s, std::string path,
+                            time::Span minQueryTimeToLog, bool logTimedOut);
 
   /// createSMTLIBLoggingSolver - Create a solver which will forward all queries
   /// after writing them to the given path in .smt2 format.
-  Solver *createSMTLIBLoggingSolver(Solver *s, std::string path,
-                                    time::Span minQueryTimeToLog,
-                                    bool logTimedOut);
-
+  std::unique_ptr<Solver>
+  createSMTLIBLoggingSolver(std::unique_ptr<Solver> s, std::string path,
+                            time::Span minQueryTimeToLog, bool logTimedOut);
 
   /// createDummySolver - Create a dummy solver implementation which always
   /// fails.
-  Solver *createDummySolver();
+  std::unique_ptr<Solver> createDummySolver();
 
   // Create a solver based on the supplied ``CoreSolverType``.
-  Solver *createCoreSolver(CoreSolverType cst);
-}
+  std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst);
+  } // namespace klee
 
 #endif /* KLEE_SOLVER_H */
diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h
index f03db964..b73370b9 100644
--- a/include/klee/Solver/SolverImpl.h
+++ b/include/klee/Solver/SolverImpl.h
@@ -23,12 +23,12 @@ namespace klee {
 
   /// SolverImpl - Abstract base clase for solver implementations.
   class SolverImpl {
-    // DO NOT IMPLEMENT.
-    SolverImpl(const SolverImpl&);
-    void operator=(const SolverImpl&);
-    
   public:
-    SolverImpl() {}
+    SolverImpl() = default;
+
+    SolverImpl(const SolverImpl&) = delete;
+    SolverImpl& operator=(const SolverImpl&) = delete;
+
     virtual ~SolverImpl();
 
     enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE,
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b13afb6a..0b28d608 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -481,19 +481,19 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
 
   coreSolverTimeout = time::Span{MaxCoreSolverTime};
   if (coreSolverTimeout) UseForkedCoreSolver = true;
-  Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
+  std::unique_ptr<Solver> coreSolver = klee::createCoreSolver(CoreSolverToUse);
   if (!coreSolver) {
     klee_error("Failed to create core solver\n");
   }
 
-  Solver *solver = constructSolverChain(
-      coreSolver,
+  std::unique_ptr<Solver> solver = constructSolverChain(
+      std::move(coreSolver),
       interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME),
       interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME),
       interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME),
       interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME));
 
-  this->solver = new TimingSolver(solver, EqualitySubstitution);
+  this->solver = std::make_unique<TimingSolver>(std::move(solver), EqualitySubstitution);
   memory = new MemoryManager(&arrayCache);
 
   initializeSearchOptions();
@@ -593,7 +593,6 @@ Executor::~Executor() {
   delete externalDispatcher;
   delete specialFunctionHandler;
   delete statsTracker;
-  delete solver;
 }
 
 /***/
@@ -1236,7 +1235,7 @@ void Executor::addConstraint(ExecutionState &state, ref<Expr> condition) {
       assert(success && "FIXME: Unhandled solver failure");
       (void) success;
       if (res) {
-        siit->patchSeed(state, condition, solver);
+        siit->patchSeed(state, condition, solver.get());
         warn = true;
       }
     }
@@ -3895,7 +3894,7 @@ void Executor::callExternalFunction(ExecutionState &state,
       // Checking to see if the argument is a pointer to something
       if (ce->getWidth() == Context::get().getPointerWidth() &&
           state.addressSpace.resolveOne(ce, op)) {
-        op.second->flushToConcreteStore(solver, state);
+        op.second->flushToConcreteStore(solver.get(), state);
       }
       wordIndex += (ce->getWidth()+63)/64;
     } else {
@@ -4234,7 +4233,7 @@ void Executor::resolveExact(ExecutionState &state,
   p = optimizer.optimizeExpr(p, true);
   // XXX we may want to be capping this?
   ResolutionList rl;
-  state.addressSpace.resolve(state, solver, p, rl);
+  state.addressSpace.resolve(state, solver.get(), p, rl);
   
   ExecutionState *unbound = &state;
   for (ResolutionList::iterator it = rl.begin(), ie = rl.end(); 
@@ -4294,7 +4293,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   ObjectPair op;
   bool success;
   solver->setTimeout(coreSolverTimeout);
-  if (!state.addressSpace.resolveOne(state, solver, address, op, success)) {
+  if (!state.addressSpace.resolveOne(state, solver.get(), address, op, success)) {
     address = toConstant(state, address, "resolveOne failure");
     success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
   }
@@ -4351,7 +4350,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   address = optimizer.optimizeExpr(address, true);
   ResolutionList rl;  
   solver->setTimeout(coreSolverTimeout);
-  bool incomplete = state.addressSpace.resolve(state, solver, address, rl,
+  bool incomplete = state.addressSpace.resolve(state, solver.get(), address, rl,
                                                0, coreSolverTimeout);
   solver->setTimeout(time::Span());
   
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 28a7d56d..40111af9 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -110,7 +110,7 @@ private:
   Searcher *searcher;
 
   ExternalDispatcher *externalDispatcher;
-  TimingSolver *solver;
+  std::unique_ptr<TimingSolver> solver;
   MemoryManager *memory;
   std::set<ExecutionState*, ExecutionStateIDCompare> states;
   StatsTracker *statsTracker;
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index 1f179e54..0b88be3c 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -16,6 +16,7 @@
 #include "klee/System/Time.h"
 
 #include <memory>
+#include <utility>
 #include <vector>
 
 namespace klee {
@@ -35,8 +36,8 @@ public:
   /// \param _simplifyExprs - Whether expressions should be
   /// simplified (via the constraint manager interface) prior to
   /// querying.
-  TimingSolver(Solver *_solver, bool _simplifyExprs = true)
-      : solver(_solver), simplifyExprs(_simplifyExprs) {}
+  TimingSolver(std::unique_ptr<Solver> solver, bool simplifyExprs = true)
+      : solver(std::move(solver)), simplifyExprs(simplifyExprs) {}
 
   void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); }
 
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
index f18f43a8..d90cf6b2 100644
--- a/lib/Solver/AssignmentValidatingSolver.cpp
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -13,6 +13,7 @@
 #include "klee/Solver/SolverImpl.h"
 
 #include <memory>
+#include <utility>
 #include <vector>
 
 namespace klee {
@@ -23,7 +24,8 @@ private:
   void dumpAssignmentQuery(const Query &query, const Assignment &assignment);
 
 public:
-  AssignmentValidatingSolver(Solver *_solver) : solver(_solver) {}
+  AssignmentValidatingSolver(std::unique_ptr<Solver> solver)
+      : solver(std::move(solver)) {}
 
   bool computeValidity(const Query &, Solver::Validity &result);
   bool computeTruth(const Query &, bool &isValid);
@@ -148,7 +150,9 @@ void AssignmentValidatingSolver::setCoreSolverTimeout(time::Span timeout) {
   return solver->impl->setCoreSolverTimeout(timeout);
 }
 
-Solver *createAssignmentValidatingSolver(Solver *s) {
-  return new Solver(new AssignmentValidatingSolver(s));
+std::unique_ptr<Solver>
+createAssignmentValidatingSolver(std::unique_ptr<Solver> s) {
+  return std::make_unique<Solver>(
+      std::make_unique<AssignmentValidatingSolver>(std::move(s)));
 }
 }
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 5d85062d..751e81c1 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -18,6 +18,7 @@
 
 #include <memory>
 #include <unordered_map>
+#include <utility>
 
 using namespace klee;
 
@@ -67,7 +68,7 @@ private:
   cache_map cache;
 
 public:
-  CachingSolver(Solver *s) : solver(s) {}
+  CachingSolver(std::unique_ptr<Solver> solver) : solver(std::move(solver)) {}
 
   bool computeValidity(const Query&, Solver::Validity &result);
   bool computeTruth(const Query&, bool &isValid);
@@ -255,6 +256,8 @@ void CachingSolver::setCoreSolverTimeout(time::Span timeout) {
 
 ///
 
-Solver *klee::createCachingSolver(Solver *_solver) {
-  return new Solver(new CachingSolver(_solver));
+std::unique_ptr<Solver>
+klee::createCachingSolver(std::unique_ptr<Solver> solver) {
+  return std::make_unique<Solver>(
+      std::make_unique<CachingSolver>(std::move(solver)));
 }
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 28996a6a..dbbd3516 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -24,6 +24,7 @@
 #include "llvm/Support/CommandLine.h"
 
 #include <memory>
+#include <utility>
 
 using namespace klee;
 using namespace llvm;
@@ -87,7 +88,8 @@ class CexCachingSolver : public SolverImpl {
   bool getAssignment(const Query& query, Assignment *&result);
   
 public:
-  CexCachingSolver(Solver *_solver) : solver(_solver) {}
+  CexCachingSolver(std::unique_ptr<Solver> solver)
+      : solver(std::move(solver)) {}
   ~CexCachingSolver();
   
   bool computeTruth(const Query&, bool &isValid);
@@ -384,6 +386,8 @@ void CexCachingSolver::setCoreSolverTimeout(time::Span timeout) {
 
 ///
 
-Solver *klee::createCexCachingSolver(Solver *_solver) {
-  return new Solver(new CexCachingSolver(_solver));
+std::unique_ptr<Solver>
+klee::createCexCachingSolver(std::unique_ptr<Solver> solver) {
+  return std::make_unique<Solver>(
+      std::make_unique<CexCachingSolver>(std::move(solver)));
 }
diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp
index 999edda4..9109fe1d 100644
--- a/lib/Solver/ConstructSolverChain.cpp
+++ b/lib/Solver/ConstructSolverChain.cpp
@@ -18,62 +18,72 @@
 
 #include "llvm/Support/raw_ostream.h"
 
+#include <memory>
+#include <utility>
 
 namespace klee {
-Solver *constructSolverChain(Solver *coreSolver,
-                             std::string querySMT2LogPath,
-                             std::string baseSolverQuerySMT2LogPath,
-                             std::string queryKQueryLogPath,
-                             std::string baseSolverQueryKQueryLogPath) {
-  Solver *solver = coreSolver;
+std::unique_ptr<Solver> constructSolverChain(
+    std::unique_ptr<Solver> coreSolver, std::string querySMT2LogPath,
+    std::string baseSolverQuerySMT2LogPath, std::string queryKQueryLogPath,
+    std::string baseSolverQueryKQueryLogPath) {
+  Solver *rawCoreSolver = coreSolver.get();
+  std::unique_ptr<Solver> solver = std::move(coreSolver);
   const time::Span minQueryTimeToLog(MinQueryTimeToLog);
 
   if (QueryLoggingOptions.isSet(SOLVER_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries);
+    solver = createKQueryLoggingSolver(std::move(solver),
+                                       baseSolverQueryKQueryLogPath,
+                                       minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging queries that reach solver in .kquery format to %s\n",
                  baseSolverQueryKQueryLogPath.c_str());
   }
 
   if (QueryLoggingOptions.isSet(SOLVER_SMTLIB)) {
-    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
+    solver =
+        createSMTLIBLoggingSolver(std::move(solver), baseSolverQuerySMT2LogPath,
+                                  minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging queries that reach solver in .smt2 format to %s\n",
                  baseSolverQuerySMT2LogPath.c_str());
   }
 
   if (UseAssignmentValidatingSolver)
-    solver = createAssignmentValidatingSolver(solver);
+    solver = createAssignmentValidatingSolver(std::move(solver));
 
   if (UseFastCexSolver)
-    solver = createFastCexSolver(solver);
+    solver = createFastCexSolver(std::move(solver));
 
   if (UseCexCache)
-    solver = createCexCachingSolver(solver);
+    solver = createCexCachingSolver(std::move(solver));
 
   if (UseBranchCache)
-    solver = createCachingSolver(solver);
+    solver = createCachingSolver(std::move(solver));
 
   if (UseIndependentSolver)
-    solver = createIndependentSolver(solver);
+    solver = createIndependentSolver(std::move(solver));
 
   if (DebugValidateSolver)
-    solver = createValidatingSolver(solver, coreSolver);
+    solver = createValidatingSolver(std::move(solver), rawCoreSolver, false);
 
   if (QueryLoggingOptions.isSet(ALL_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries);
+    solver = createKQueryLoggingSolver(std::move(solver), queryKQueryLogPath,
+                                       minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging all queries in .kquery format to %s\n",
                  queryKQueryLogPath.c_str());
   }
 
   if (QueryLoggingOptions.isSet(ALL_SMTLIB)) {
-    solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
+    solver = createSMTLIBLoggingSolver(std::move(solver), querySMT2LogPath,
+                                       minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging all queries in .smt2 format to %s\n",
                  querySMT2LogPath.c_str());
   }
   if (DebugCrossCheckCoreSolverWith != NO_SOLVER) {
-    Solver *oracleSolver = createCoreSolver(DebugCrossCheckCoreSolverWith);
-    solver = createValidatingSolver(solver, oracleSolver, true);
+    std::unique_ptr<Solver> oracleSolver =
+        createCoreSolver(DebugCrossCheckCoreSolverWith);
+    solver =
+        createValidatingSolver(std::move(solver), oracleSolver.release(), true);
   }
 
   return solver;
 }
-}
+} // namespace klee
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index fbf29747..abbccf5b 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -19,15 +19,16 @@
 #include "llvm/Support/raw_ostream.h"
 
 #include <string>
+#include <memory>
 
 namespace klee {
 
-Solver *createCoreSolver(CoreSolverType cst) {
+std::unique_ptr<Solver> createCoreSolver(CoreSolverType cst) {
   switch (cst) {
   case STP_SOLVER:
 #ifdef ENABLE_STP
     klee_message("Using STP solver backend");
-    return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    return std::make_unique<STPSolver>(UseForkedCoreSolver, CoreSolverOptimizeDivides);
 #else
     klee_message("Not compiled with STP support");
     return NULL;
@@ -45,7 +46,7 @@ Solver *createCoreSolver(CoreSolverType cst) {
   case Z3_SOLVER:
 #ifdef ENABLE_Z3
     klee_message("Using Z3 solver backend");
-    return new Z3Solver();
+    return std::make_unique<Z3Solver>();
 #else
     klee_message("Not compiled with Z3 support");
     return NULL;
diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp
index a845f901..1cf88d64 100644
--- a/lib/Solver/DummySolver.cpp
+++ b/lib/Solver/DummySolver.cpp
@@ -11,6 +11,8 @@
 #include "klee/Solver/SolverImpl.h"
 #include "klee/Solver/SolverStats.h"
 
+#include <memory>
+
 namespace klee {
 
 class DummySolverImpl : public SolverImpl {
@@ -59,5 +61,7 @@ SolverImpl::SolverRunStatus DummySolverImpl::getOperationStatusCode() {
   return SOLVER_RUN_STATUS_FAILURE;
 }
 
-Solver *createDummySolver() { return new Solver(new DummySolverImpl()); }
+std::unique_ptr<Solver> createDummySolver() {
+  return std::make_unique<Solver>(std::make_unique<DummySolverImpl>());
+}
 }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 34a44c3e..81fd6707 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -24,6 +24,7 @@
 #include <cassert>
 #include <map>
 #include <sstream>
+#include <utility>
 #include <vector>
 
 using namespace klee;
@@ -1141,7 +1142,7 @@ FastCexSolver::computeInitialValues(const Query& query,
   return true;
 }
 
-
-Solver *klee::createFastCexSolver(Solver *s) {
-  return new Solver(new StagedSolverImpl(new FastCexSolver(), s));
+std::unique_ptr<Solver> klee::createFastCexSolver(std::unique_ptr<Solver> s) {
+  return std::make_unique<Solver>(std::make_unique<StagedSolverImpl>(
+      std::make_unique<FastCexSolver>(), std::move(s)));
 }
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index a9035eda..7aef05c9 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -11,6 +11,8 @@
 
 #include "klee/Expr/Constraints.h"
 
+#include <utility>
+
 using namespace klee;
 using namespace llvm;
 
@@ -58,11 +60,9 @@ IncompleteSolver::computeValidity(const Query& query) {
 
 /***/
 
-StagedSolverImpl::StagedSolverImpl(IncompleteSolver *_primary, 
-                                   Solver *_secondary) 
-  : primary(_primary),
-    secondary(_secondary) {
-}
+StagedSolverImpl::StagedSolverImpl(std::unique_ptr<IncompleteSolver> primary,
+                                   std::unique_ptr<Solver> secondary)
+    : primary(std::move(primary)), secondary(std::move(secondary)) {}
 
 bool StagedSolverImpl::computeTruth(const Query& query, bool &isValid) {
   IncompleteSolver::PartialValidity trueResult = primary->computeTruth(query); 
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 007bfdcb..c05fa6bb 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -393,7 +393,8 @@ private:
   std::unique_ptr<Solver> solver;
 
 public:
-  IndependentSolver(Solver *_solver) : solver(_solver) {}
+  IndependentSolver(std::unique_ptr<Solver> solver)
+      : solver(std::move(solver)) {}
 
   bool computeTruth(const Query&, bool &isValid);
   bool computeValidity(const Query&, Solver::Validity &result);
@@ -557,6 +558,8 @@ void IndependentSolver::setCoreSolverTimeout(time::Span timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
 
-Solver *klee::createIndependentSolver(Solver *s) {
-  return new Solver(new IndependentSolver(s));
+std::unique_ptr<Solver>
+klee::createIndependentSolver(std::unique_ptr<Solver> s) {
+  return std::make_unique<Solver>(
+      std::make_unique<IndependentSolver>(std::move(s)));
 }
diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp
index fccdd615..4be24e9c 100644
--- a/lib/Solver/KQueryLoggingSolver.cpp
+++ b/lib/Solver/KQueryLoggingSolver.cpp
@@ -13,6 +13,8 @@
 #include "klee/Expr/ExprPPrinter.h"
 #include "klee/System/Time.h"
 
+#include <utility>
+
 using namespace klee;
 
 class KQueryLoggingSolver : public QueryLoggingSolver {
@@ -48,10 +50,11 @@ private :
     }
 
 public:
-    KQueryLoggingSolver(Solver *_solver, std::string path, time::Span queryTimeToLog, bool logTimedOut)
-    : QueryLoggingSolver(_solver, path, "#", queryTimeToLog, logTimedOut),
-    printer(ExprPPrinter::create(logBuffer)) {
-    }
+  KQueryLoggingSolver(std::unique_ptr<Solver> solver, std::string path,
+                      time::Span queryTimeToLog, bool logTimedOut)
+      : QueryLoggingSolver(std::move(solver), std::move(path), "#",
+                           queryTimeToLog, logTimedOut),
+        printer(ExprPPrinter::create(logBuffer)) {}
 
     virtual ~KQueryLoggingSolver() {
         delete printer;
@@ -60,8 +63,10 @@ public:
 
 ///
 
-Solver *klee::createKQueryLoggingSolver(Solver *_solver, std::string path,
-                                    time::Span minQueryTimeToLog, bool logTimedOut) {
-  return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut));
+std::unique_ptr<Solver>
+klee::createKQueryLoggingSolver(std::unique_ptr<Solver> solver,
+                                std::string path, time::Span minQueryTimeToLog,
+                                bool logTimedOut) {
+  return std::make_unique<Solver>(std::make_unique<KQueryLoggingSolver>(
+      std::move(solver), std::move(path), minQueryTimeToLog, logTimedOut));
 }
-
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 37c22f0e..c3c6dfaa 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -51,6 +51,8 @@
 #undef type_t
 #endif
 
+#include <memory>
+
 #include <errno.h>
 #include <signal.h>
 #include <sys/ipc.h>
@@ -85,7 +87,6 @@ private:
 public:
   MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked,
                     bool optimizeDivides);
-  virtual ~MetaSMTSolverImpl();
 
   char *getConstraintLog(const Query &);
   void setCoreSolverTimeout(time::Span timeout) { _timeout = timeout; }
@@ -134,9 +135,6 @@ MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(
 }
 
 template <typename SolverContext>
-MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {}
-
-template <typename SolverContext>
 char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query &) {
   const char *msg = "Not supported";
   char *buf = new char[strlen(msg) + 1];
@@ -404,8 +402,8 @@ MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() {
 template <typename SolverContext>
 MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked,
                                             bool optimizeDivides)
-    : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked,
-                                                  optimizeDivides)) {}
+    : Solver(std::make_unique<MetaSMTSolverImpl<SolverContext>>(
+          this, useForked, optimizeDivides)) {}
 
 template <typename SolverContext>
 MetaSMTSolver<SolverContext>::~MetaSMTSolver() {}
@@ -420,45 +418,50 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(time::Span timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 
-Solver *createMetaSMTSolver() {
+std::unique_ptr<Solver> createMetaSMTSolver() {
   using namespace metaSMT;
 
-  Solver *coreSolver = NULL;
+  std::unique_ptr<Solver> coreSolver;
   std::string backend;
   switch (MetaSMTBackend) {
 #ifdef METASMT_HAVE_STP
   case METASMT_BACKEND_STP:
     backend = "STP";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::STP_Backend> >(
+    coreSolver = std::make_unique<
+        MetaSMTSolver<DirectSolver_Context<solver::STP_Backend>>>(
         UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
 #endif
 #ifdef METASMT_HAVE_Z3
   case METASMT_BACKEND_Z3:
     backend = "Z3";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend> >(
+    coreSolver = std::make_unique<
+        MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend>>>(
         UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
 #endif
 #ifdef METASMT_HAVE_BTOR
   case METASMT_BACKEND_BOOLECTOR:
     backend = "Boolector";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Boolector> >(
+    coreSolver = std::make_unique<
+        MetaSMTSolver<DirectSolver_Context<solver::Boolector>>>(
         UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
 #endif
 #ifdef METASMT_HAVE_CVC4
   case METASMT_BACKEND_CVC4:
     backend = "CVC4";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::CVC4> >(
-        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    coreSolver =
+        std::make_unique<MetaSMTSolver<DirectSolver_Context<solver::CVC4>>>(
+            UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
 #endif
 #ifdef METASMT_HAVE_YICES2
   case METASMT_BACKEND_YICES2:
     backend = "Yices2";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Yices2> >(
-        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    coreSolver =
+        std::make_unique<MetaSMTSolver<DirectSolver_Context<solver::Yices2>>>(
+            UseForkedCoreSolver, CoreSolverOptimizeDivides);
     break;
 #endif
   default:
@@ -468,6 +471,5 @@ Solver *createMetaSMTSolver() {
   klee_message("Starting MetaSMTSolver(%s)", backend.c_str());
   return coreSolver;
 }
-
 }
 #endif // ENABLE_METASMT
diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h
index 89cb7143..64c56c57 100644
--- a/lib/Solver/MetaSMTSolver.h
+++ b/lib/Solver/MetaSMTSolver.h
@@ -13,6 +13,8 @@
 
 #include "klee/Solver/Solver.h"
 
+#include <memory>
+
 namespace klee {
 
 template <typename SolverContext> class MetaSMTSolver : public Solver {
@@ -26,7 +28,7 @@ public:
 
 /// createMetaSMTSolver - Create a solver using the metaSMT backend set by
 /// the option MetaSMTBackend.
-Solver *createMetaSMTSolver();
+std::unique_ptr<Solver> createMetaSMTSolver();
 }
 
 #endif /* KLEE_METASMTSOLVER_H */
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index c057751c..911fa067 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -15,6 +15,8 @@
 #include "klee/Support/FileHandling.h"
 #include "klee/System/Time.h"
 
+#include <utility>
+
 namespace {
 llvm::cl::opt<bool> DumpPartialQueryiesEarly(
     "log-partial-queries-early", llvm::cl::init(false),
@@ -29,13 +31,14 @@ llvm::cl::opt<bool> CreateCompressedQueryLog(
 #endif
 } // namespace
 
-QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
+QueryLoggingSolver::QueryLoggingSolver(std::unique_ptr<Solver> solver,
+                                       std::string path,
                                        const std::string &commentSign,
                                        time::Span queryTimeToLog,
                                        bool logTimedOut)
-    : solver(_solver), BufferString(""), logBuffer(BufferString), queryCount(0),
-      minQueryTimeToLog(queryTimeToLog), logTimedOutQueries(logTimedOut),
-      queryCommentSign(commentSign) {
+    : solver(std::move(solver)), BufferString(""), logBuffer(BufferString),
+      queryCount(0), minQueryTimeToLog(queryTimeToLog),
+      logTimedOutQueries(logTimedOut), queryCommentSign(commentSign) {
   std::string error;
 #ifdef HAVE_ZLIB_H
   if (!CreateCompressedQueryLog) {
@@ -50,7 +53,7 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
   if (!os) {
     klee_error("Could not open file %s : %s", path.c_str(), error.c_str());
   }
-  assert(0 != solver);
+  assert(this->solver);
 }
 
 void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) {
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 76bba429..8149342f 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -58,8 +58,9 @@ protected:
   void flushBufferConditionally(bool writeToFile);
 
 public:
-  QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign,
-                     time::Span queryTimeToLog, bool logTimedOut);
+  QueryLoggingSolver(std::unique_ptr<Solver> solver, std::string path,
+                     const std::string &commentSign, time::Span queryTimeToLog,
+                     bool logTimedOut);
 
   /// implementation of the SolverImpl interface
   bool computeTruth(const Query &query, bool &isValid);
diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp
index bfea5c1b..c0713b45 100644
--- a/lib/Solver/SMTLIBLoggingSolver.cpp
+++ b/lib/Solver/SMTLIBLoggingSolver.cpp
@@ -11,6 +11,9 @@
 
 #include "klee/Expr/ExprSMTLIBPrinter.h"
 
+#include <memory>
+#include <utility>
+
 using namespace klee;
 
 /// This QueryLoggingSolver will log queries to a file in the SMTLIBv2 format
@@ -18,7 +21,6 @@ using namespace klee;
 class SMTLIBLoggingSolver : public QueryLoggingSolver
 {
         private:
-    
                 ExprSMTLIBPrinter printer;
 
                 virtual void printQuery(const Query& query,
@@ -41,22 +43,21 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver
 
                         printer.generateOutput();
                 }    
-        
-	public:
-		SMTLIBLoggingSolver(Solver *_solver,
-                        std::string path,
-                        time::Span queryTimeToLog,
-                        bool logTimedOut)
-		: QueryLoggingSolver(_solver, path, ";", queryTimeToLog, logTimedOut)
-		{
-		  //Setup the printer
-		  printer.setOutput(logBuffer);
-		}
-};
 
+public:
+  SMTLIBLoggingSolver(std::unique_ptr<Solver> solver, std::string path,
+                      time::Span queryTimeToLog, bool logTimedOut)
+      : QueryLoggingSolver(std::move(solver), std::move(path), ";",
+                           queryTimeToLog, logTimedOut) {
+    // Setup the printer
+    printer.setOutput(logBuffer);
+  }
+};
 
-Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path,
-                                        time::Span minQueryTimeToLog, bool logTimedOut)
-{
-  return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut));
+std::unique_ptr<Solver>
+klee::createSMTLIBLoggingSolver(std::unique_ptr<Solver> solver,
+                                std::string path, time::Span minQueryTimeToLog,
+                                bool logTimedOut) {
+  return std::make_unique<Solver>(std::make_unique<SMTLIBLoggingSolver>(
+      std::move(solver), std::move(path), minQueryTimeToLog, logTimedOut));
 }
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index 140ca6f4..8858e83e 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -430,7 +430,7 @@ SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() {
 }
 
 STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
-    : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides)) {}
+    : Solver(std::make_unique<STPSolverImpl>(useForkedSTP, optimizeDivides)) {}
 
 char *STPSolver::getConstraintLog(const Query &query) {
   return impl->getConstraintLog(query);
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index e123a667..bb6ed105 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -12,6 +12,8 @@
 #include "klee/Expr/Constraints.h"
 #include "klee/Solver/SolverImpl.h"
 
+#include <utility>
+
 using namespace klee;
 
 const char *Solver::validity_to_str(Validity v) {
@@ -22,7 +24,7 @@ const char *Solver::validity_to_str(Validity v) {
   }
 }
 
-Solver::Solver(SolverImpl *impl) : impl(impl) {}
+Solver::Solver(std::unique_ptr<SolverImpl> impl) : impl(std::move(impl)) {}
 Solver::~Solver() = default;
 
 char *Solver::getConstraintLog(const Query& query) {
diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp
index 72bdc830..8e9886d1 100644
--- a/lib/Solver/ValidatingSolver.cpp
+++ b/lib/Solver/ValidatingSolver.cpp
@@ -12,6 +12,7 @@
 #include "klee/Solver/SolverImpl.h"
 
 #include <memory>
+#include <utility>
 #include <vector>
 
 namespace klee {
@@ -22,8 +23,9 @@ private:
   std::unique_ptr<Solver, void(*)(Solver*)> oracle;
 
 public:
-  ValidatingSolver(Solver *solver, Solver *oracle, bool ownsOracle = false)
-      : solver(solver),
+  ValidatingSolver(std::unique_ptr<Solver> solver, Solver *oracle,
+                   bool ownsOracle)
+      : solver(std::move(solver)),
         oracle(
             oracle, ownsOracle ? [](Solver *solver) { delete solver; }
                                : [](Solver *) {}) {}
@@ -140,7 +142,10 @@ void ValidatingSolver::setCoreSolverTimeout(time::Span timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
 
-Solver *createValidatingSolver(Solver *s, Solver *oracle, bool ownsOracle) {
-  return new Solver(new ValidatingSolver(s, oracle, ownsOracle));
+std::unique_ptr<Solver> createValidatingSolver(std::unique_ptr<Solver> s,
+                                               Solver *oracle,
+                                               bool ownsOracle) {
+  return std::make_unique<Solver>(
+      std::make_unique<ValidatingSolver>(std::move(s), oracle, ownsOracle));
 }
 }
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index f3e8f92b..180b32f6 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -139,7 +139,7 @@ Z3SolverImpl::~Z3SolverImpl() {
   Z3_params_dec_ref(builder->ctx, solverParameters);
 }
 
-Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {}
+Z3Solver::Z3Solver() : Solver(std::make_unique<Z3SolverImpl>()) {}
 
 char *Z3Solver::getConstraintLog(const Query &query) {
   return impl->getConstraintLog(query);
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index eed4e4c9..51298dfb 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -29,12 +29,11 @@
 #include "llvm/Support/ManagedStatic.h"
 #include "llvm/Support/MemoryBuffer.h"
 #include "llvm/Support/raw_ostream.h"
+#include "llvm/Support/Signals.h"
 
 #include <sys/stat.h>
 #include <unistd.h>
-
-
-#include "llvm/Support/Signals.h"
+#include <utility>
 
 using namespace llvm;
 using namespace klee;
@@ -200,7 +199,7 @@ static bool EvaluateInputAST(const char *Filename,
   if (!success)
     return false;
 
-  Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
+  std::unique_ptr<Solver> coreSolver = klee::createCoreSolver(CoreSolverToUse);
 
   if (CoreSolverToUse != DUMMY_SOLVER) {
     const time::Span maxCoreSolverTime(MaxCoreSolverTime);
@@ -209,11 +208,11 @@ static bool EvaluateInputAST(const char *Filename,
     }
   }
 
-  Solver *S = constructSolverChain(coreSolver,
-                                   getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
-                                   getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
-                                   getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME),
-                                   getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME));
+  std::unique_ptr<Solver> S = constructSolverChain(
+      std::move(coreSolver), getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME),
+      getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME),
+      getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME),
+      getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME));
 
   unsigned Index = 0;
   for (std::vector<Decl*>::iterator it = Decls.begin(),
@@ -294,8 +293,6 @@ static bool EvaluateInputAST(const char *Filename,
     delete *it;
   delete P;
 
-  delete S;
-
   if (uint64_t queries = *theStatisticManager->getStatisticByName("SolverQueries")) {
     llvm::outs()
       << "--\n"
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index d5d207a0..2137602f 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -131,11 +131,11 @@ void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true,
 }
 
 TEST(SolverTest, Evaluation) {
-  Solver *solver = klee::createCoreSolver(CoreSolverToUse);
+  auto solver = klee::createCoreSolver(CoreSolverToUse);
 
-  solver = createCexCachingSolver(solver);
-  solver = createCachingSolver(solver);
-  solver = createIndependentSolver(solver);
+  solver = createCexCachingSolver(std::move(solver));
+  solver = createCachingSolver(std::move(solver));
+  solver = createIndependentSolver(std::move(solver));
 
   testOpcode<SelectExpr>(*solver);
   testOpcode<ZExtExpr>(*solver);
@@ -165,8 +165,6 @@ TEST(SolverTest, Evaluation) {
   testOpcode<SleExpr>(*solver);
   testOpcode<SgtExpr>(*solver);
   testOpcode<SgeExpr>(*solver);
-
-  delete solver;
 }
 
 }
diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp
index eab43d79..e81ff19e 100644
--- a/unittests/Solver/Z3SolverTest.cpp
+++ b/unittests/Solver/Z3SolverTest.cpp
@@ -19,6 +19,8 @@
 #include "klee/Expr/Expr.h"
 #include "klee/Solver/Solver.h"
 
+#include <memory>
+
 using namespace klee;
 
 namespace {
@@ -26,13 +28,11 @@ ArrayCache AC;
 }
 class Z3SolverTest : public ::testing::Test {
 protected:
+  std::unique_ptr<Solver> Z3Solver_;
+
   Z3SolverTest() : Z3Solver_(createCoreSolver(CoreSolverType::Z3_SOLVER)) {
     Z3Solver_->setCoreSolverTimeout(time::Span("10s"));
   }
-
-  virtual ~Z3SolverTest() { delete Z3Solver_; }
-
-  Solver *Z3Solver_;
 };
 
 TEST_F(Z3SolverTest, GetConstraintLog) {