4 files changed, 34 insertions, 34 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,