1 files changed, 29 insertions, 19 deletions

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