1 files changed, 18 insertions, 16 deletions
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