2 files changed, 5 insertions, 12 deletions
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
index a2256028..2689d19c 100644
--- a/include/klee/Solver/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -14,6 +14,7 @@
 #include "klee/System/Time.h"
 #include "klee/Solver/SolverCmdLine.h"
 
+#include <memory>
 #include <vector>
 
 namespace klee {
@@ -58,10 +59,6 @@ namespace klee {
   };
 
   class Solver {
-    // DO NOT IMPLEMENT.
-    Solver(const Solver&);
-    void operator=(const Solver&);
-
   public:
     enum Validity {
       True = 1,
@@ -69,15 +66,12 @@ namespace klee {
       Unknown = 0
     };
   
-  public:
     /// validity_to_str - Return the name of given Validity enum value.
     static const char *validity_to_str(Validity v);
 
-  public:
-    SolverImpl *impl;
+    std::unique_ptr<SolverImpl> impl;
 
-  public:
-    Solver(SolverImpl *_impl) : impl(_impl) {}
+    Solver(SolverImpl *impl);
     virtual ~Solver();
 
     /// evaluate - Determine for a particular state if the query
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 5fe973fe..e123a667 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -22,9 +22,8 @@ const char *Solver::validity_to_str(Validity v) {
   }
 }
 
-Solver::~Solver() { 
-  delete impl; 
-}
+Solver::Solver(SolverImpl *impl) : impl(impl) {}
+Solver::~Solver() = default;
 
 char *Solver::getConstraintLog(const Query& query) {
     return impl->getConstraintLog(query);