3 files changed, 13 insertions, 26 deletions

diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 7e4d8fe0..0fb145d7 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -7,18 +7,11 @@
 //
 //===----------------------------------------------------------------------===//
 #include "QueryLoggingSolver.h"
-#include "klee/Config/config.h"
-#include "klee/Internal/System/Time.h"
 #include "klee/Statistics.h"
-#ifdef HAVE_ZLIB_H
-#include "klee/Internal/Support/CompressionStream.h"
+#include "klee/Config/config.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Internal/Support/FileHandling.h"
-#endif
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5)
-#include "llvm/Support/FileSystem.h"
-#endif
+#include "klee/Internal/System/Time.h"
 
 using namespace klee::util;
 
@@ -37,9 +30,9 @@ llvm::cl::opt<bool> CreateCompressedQueryLog(
 QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
                                        const std::string &commentSign,
                                        int queryTimeToLog)
-    : solver(_solver), os(0), BufferString(""), logBuffer(BufferString),
-      queryCount(0), minQueryTimeToLog(queryTimeToLog), startTime(0.0f),
-      lastQueryTime(0.0f), queryCommentSign(commentSign) {
+    : solver(_solver), BufferString(""), logBuffer(BufferString), queryCount(0),
+      minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f),
+      queryCommentSign(commentSign) {
   std::string error;
 #ifdef HAVE_ZLIB_H
   if (!CreateCompressedQueryLog) {
@@ -47,18 +40,18 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
     os = klee_open_output_file(path, error);
 #ifdef HAVE_ZLIB_H
   } else {
-    os = new compressed_fd_ostream((path + ".gz").c_str(), error);
+    path.append(".gz");
+    os = klee_open_compressed_output_file(path, error);
   }
-  if (!error.empty()) {
+#endif
+  if (!os) {
     klee_error("Could not open file %s : %s", path.c_str(), error.c_str());
   }
-#endif
   assert(0 != solver);
 }
 
 QueryLoggingSolver::~QueryLoggingSolver() {
   delete solver;
-  delete os;
 }
 
 void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) {
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 68edfe55..4da3c129 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -25,7 +25,7 @@ class QueryLoggingSolver : public SolverImpl {
 
 protected:
   Solver *solver;
-  llvm::raw_ostream *os;
+  std::unique_ptr<llvm::raw_ostream> os;
   // @brief Buffer used by logBuffer
   std::string BufferString;
   // @brief buffer to store logs before flushing to file
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 72a15c50..f127de9b 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -49,7 +49,7 @@ private:
   Z3Builder *builder;
   double timeout;
   SolverRunStatus runStatusCode;
-  llvm::raw_fd_ostream* dumpedQueriesFile;
+  std::unique_ptr<llvm::raw_fd_ostream> dumpedQueriesFile;
   ::Z3_params solverParameters;
   // Parameter symbols
   ::Z3_symbol timeoutParamStrSymbol;
@@ -96,8 +96,7 @@ Z3SolverImpl::Z3SolverImpl()
           /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0
               ? Z3LogInteractionFile.c_str()
               : NULL)),
-      timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE),
-      dumpedQueriesFile(0) {
+      timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
   assert(builder && "unable to create Z3Builder");
   solverParameters = Z3_mk_params(builder->ctx);
   Z3_params_inc_ref(builder->ctx, solverParameters);
@@ -107,7 +106,7 @@ Z3SolverImpl::Z3SolverImpl()
   if (!Z3QueryDumpFile.empty()) {
     std::string error;
     dumpedQueriesFile = klee_open_output_file(Z3QueryDumpFile, error);
-    if (!error.empty()) {
+    if (!dumpedQueriesFile) {
       klee_error("Error creating file for dumping Z3 queries: %s",
                  error.c_str());
     }
@@ -127,11 +126,6 @@ Z3SolverImpl::Z3SolverImpl()
 Z3SolverImpl::~Z3SolverImpl() {
   Z3_params_dec_ref(builder->ctx, solverParameters);
   delete builder;
-
-  if (dumpedQueriesFile) {
-    dumpedQueriesFile->close();
-    delete dumpedQueriesFile;
-  }
 }
 
 Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {}