Base time API upon std::chrono

This should not change the behaviour of KLEE and mimics the old API.

- functions moved from util into time namespace
- uses time points and time spans instead of double
- CLI arguments now have the form "3h5min8us"

Changed command line parameters:
- batch-time (double to string)
- istats-write-interval (double to string)
- max-instruction-time (double to string)
- max-solver-time (double to string)
- max-time (double to string)
- min-query-time-to-log (double to string)
- seed-time (double to string)
- stats-write-interval (double to string)
- uncovered-update-interval (double to string)
- added: log-timed-out-queries (replaces negative max-solver-time)

17 files changed, 68 insertions, 78 deletions

diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
index a4d97f54..82702dbf 100644
--- a/lib/Solver/AssignmentValidatingSolver.cpp
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -32,7 +32,7 @@ public:
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query &);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
 
 // TODO: use computeInitialValues for all queries for more stress testing
@@ -148,7 +148,7 @@ char *AssignmentValidatingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void AssignmentValidatingSolver::setCoreSolverTimeout(double timeout) {
+void AssignmentValidatingSolver::setCoreSolverTimeout(time::Span timeout) {
   return solver->impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 1a6dce52..be46621b 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -93,7 +93,7 @@ public:
   }
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query&);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
 
 /** @returns the canonical version of the given query.  The reference
@@ -257,7 +257,7 @@ char *CachingSolver::getConstraintLog(const Query& query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void CachingSolver::setCoreSolverTimeout(double timeout) {
+void CachingSolver::setCoreSolverTimeout(time::Span timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index 8627b2ac..f4ee009c 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -91,7 +91,7 @@ public:
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query& query);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
 
 ///
@@ -371,7 +371,7 @@ char *CexCachingSolver::getConstraintLog(const Query& query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void CexCachingSolver::setCoreSolverTimeout(double timeout) {
+void CexCachingSolver::setCoreSolverTimeout(time::Span timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp
index dc2c9fd4..72fe2a95 100644
--- a/lib/Solver/IncompleteSolver.cpp
+++ b/lib/Solver/IncompleteSolver.cpp
@@ -143,7 +143,7 @@ char *StagedSolverImpl::getConstraintLog(const Query& query) {
   return secondary->impl->getConstraintLog(query);
 }
 
-void StagedSolverImpl::setCoreSolverTimeout(double timeout) {
+void StagedSolverImpl::setCoreSolverTimeout(time::Span timeout) {
   secondary->impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 3594fecf..19a0d745 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -408,7 +408,7 @@ public:
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query&);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
   
 bool IndependentSolver::computeValidity(const Query& query,
@@ -555,7 +555,7 @@ char *IndependentSolver::getConstraintLog(const Query& query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void IndependentSolver::setCoreSolverTimeout(double timeout) {
+void IndependentSolver::setCoreSolverTimeout(time::Span timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp
index 8dc98ac5..0c2ac6dd 100644
--- a/lib/Solver/KQueryLoggingSolver.cpp
+++ b/lib/Solver/KQueryLoggingSolver.cpp
@@ -11,6 +11,7 @@
 
 #include "klee/Expr.h"
 #include "klee/util/ExprPPrinter.h"
+#include "klee/Internal/System/Time.h"
 
 using namespace klee;
 
@@ -49,8 +50,8 @@ private :
     }
 
 public:
-    KQueryLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog)
-    : QueryLoggingSolver(_solver, path, "#", queryTimeToLog),
+    KQueryLoggingSolver(Solver *_solver, std::string path, time::Span queryTimeToLog, bool logTimedOut)
+    : QueryLoggingSolver(_solver, path, "#", queryTimeToLog, logTimedOut),
     printer(ExprPPrinter::create(logBuffer)) {
     }
 
@@ -62,7 +63,7 @@ public:
 ///
 
 Solver *klee::createKQueryLoggingSolver(Solver *_solver, std::string path,
-                                    int minQueryTimeToLog) {
-  return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog));
+                                    time::Span minQueryTimeToLog, bool logTimedOut) {
+  return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut));
 }
 
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index 695c408b..b58319c2 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -77,7 +77,7 @@ private:
   SolverContext _meta_solver;
   MetaSMTSolver<SolverContext> *_solver;
   MetaSMTBuilder<SolverContext> *_builder;
-  double _timeout;
+  time::Span _timeout;
   bool _useForked;
   SolverRunStatus _runStatusCode;
 
@@ -87,7 +87,7 @@ public:
   virtual ~MetaSMTSolverImpl();
 
   char *getConstraintLog(const Query &);
-  void setCoreSolverTimeout(double timeout) { _timeout = timeout; }
+  void setCoreSolverTimeout(time::Span timeout) { _timeout = timeout; }
 
   bool computeTruth(const Query &, bool &isValid);
   bool computeValue(const Query &, ref<Expr> &result);
@@ -106,7 +106,7 @@ public:
   runAndGetCexForked(const Query &query,
                      const std::vector<const Array *> &objects,
                      std::vector<std::vector<unsigned char> > &values,
-                     bool &hasSolution, double timeout);
+                     bool &hasSolution, time::Span timeout);
 
   SolverRunStatus getOperationStatusCode();
 
@@ -118,7 +118,7 @@ MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(
     MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides)
     : _solver(solver), _builder(new MetaSMTBuilder<SolverContext>(
                            _meta_solver, optimizeDivides)),
-      _timeout(0.0), _useForked(useForked) {
+      _useForked(useForked) {
   assert(_solver && "unable to create MetaSMTSolver");
   assert(_builder && "unable to create MetaSMTBuilder");
 
@@ -273,7 +273,7 @@ SolverImpl::SolverRunStatus
 MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
     const Query &query, const std::vector<const Array *> &objects,
     std::vector<std::vector<unsigned char> > &values, bool &hasSolution,
-    double timeout) {
+    time::Span timeout) {
   unsigned char *pos = shared_memory_ptr;
   unsigned sum = 0;
   for (std::vector<const Array *>::const_iterator it = objects.begin(),
@@ -298,7 +298,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
     if (timeout) {
       ::alarm(0); /* Turn off alarm so we can safely set signal handler */
       ::signal(SIGALRM, metaSMTTimeoutHandler);
-      ::alarm(std::max(1, (int)timeout));
+      ::alarm(std::max(1u, static_cast<unsigned>(timeout.toSeconds())));
     }
 
     // assert constraints as we are in a child process
@@ -419,7 +419,7 @@ char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query &query) {
 }
 
 template <typename SolverContext>
-void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
+void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(time::Span timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h
index 60d72383..9fa93719 100644
--- a/lib/Solver/MetaSMTSolver.h
+++ b/lib/Solver/MetaSMTSolver.h
@@ -21,7 +21,7 @@ public:
   virtual ~MetaSMTSolver();
 
   virtual char *getConstraintLog(const Query &);
-  virtual void setCoreSolverTimeout(double timeout);
+  virtual void setCoreSolverTimeout(time::Span timeout);
 };
 
 /// createMetaSMTSolver - Create a solver using the metaSMT backend set by
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp
index 0fb145d7..9001b5c1 100644
--- a/lib/Solver/QueryLoggingSolver.cpp
+++ b/lib/Solver/QueryLoggingSolver.cpp
@@ -13,8 +13,6 @@
 #include "klee/Internal/Support/FileHandling.h"
 #include "klee/Internal/System/Time.h"
 
-using namespace klee::util;
-
 namespace {
 llvm::cl::opt<bool> DumpPartialQueryiesEarly(
     "log-partial-queries-early", llvm::cl::init(false),
@@ -29,9 +27,10 @@ llvm::cl::opt<bool> CreateCompressedQueryLog(
 
 QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path,
                                        const std::string &commentSign,
-                                       int queryTimeToLog)
+                                       time::Span queryTimeToLog,
+                                       bool logTimedOut)
     : solver(_solver), BufferString(""), logBuffer(BufferString), queryCount(0),
-      minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f),
+      minQueryTimeToLog(queryTimeToLog), logTimedOutQueries(logTimedOut),
       queryCommentSign(commentSign) {
   std::string error;
 #ifdef HAVE_ZLIB_H
@@ -79,13 +78,13 @@ void QueryLoggingSolver::startQuery(const Query &query, const char *typeName,
   if (DumpPartialQueryiesEarly) {
     flushBufferConditionally(true);
   }
-  startTime = getWallTime();
+  startTime = time::getWallTime();
 }
 
 void QueryLoggingSolver::finishQuery(bool success) {
-  lastQueryTime = getWallTime() - startTime;
+  lastQueryDuration = time::getWallTime() - startTime;
   logBuffer << queryCommentSign << "   " << (success ? "OK" : "FAIL") << " -- "
-            << "Elapsed: " << lastQueryTime << "\n";
+            << "Elapsed: " << lastQueryDuration << "\n";
 
   if (false == success) {
     logBuffer << queryCommentSign << "   Failure reason: "
@@ -95,21 +94,13 @@ void QueryLoggingSolver::finishQuery(bool success) {
 }
 
 void QueryLoggingSolver::flushBuffer() {
-  bool writeToFile = false;
-
-  if ((0 == minQueryTimeToLog) ||
-      (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) {
-    // we either do not limit logging queries or the query time
-    // is larger than threshold (in ms)
-
-    if ((minQueryTimeToLog >= 0) ||
-        (SOLVER_RUN_STATUS_TIMEOUT ==
-         (solver->impl->getOperationStatusCode()))) {
-      // we do additional check here to log only timeouts in case
-      // user specified negative value for minQueryTimeToLog param
-      writeToFile = true;
-    }
-  }
+  // we either do not limit logging queries
+  // or the query time is larger than threshold
+  // or we log a timed out query
+  bool writeToFile = (!minQueryTimeToLog)
+      || (lastQueryDuration > minQueryTimeToLog)
+      || (logTimedOutQueries &&
+         (SOLVER_RUN_STATUS_TIMEOUT == solver->impl->getOperationStatusCode()));
 
   flushBufferConditionally(writeToFile);
 }
@@ -218,6 +209,6 @@ char *QueryLoggingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void QueryLoggingSolver::setCoreSolverTimeout(double timeout) {
+void QueryLoggingSolver::setCoreSolverTimeout(time::Span timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 4da3c129..75faf3a3 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -13,6 +13,8 @@
 
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
+#include "klee/Internal/System/Time.h"
+
 #include "llvm/Support/raw_ostream.h"
 
 using namespace klee;
@@ -31,13 +33,10 @@ protected:
   // @brief buffer to store logs before flushing to file
   llvm::raw_string_ostream logBuffer;
   unsigned queryCount;
-  int minQueryTimeToLog; // we log to file only those queries
-                         // which take longer than the specified time (ms);
-                         // if this param is negative, log only those queries
-                         // on which the solver has timed out
-
-  double startTime;
-  double lastQueryTime;
+  time::Span minQueryTimeToLog; // we log to file only those queries which take longer than the specified time
+  bool logTimedOutQueries = false;
+  time::Point startTime;
+  time::Span lastQueryDuration;
   const std::string queryCommentSign; // sign representing commented lines
                                       // in given a query format
 
@@ -57,8 +56,8 @@ protected:
   void flushBufferConditionally(bool writeToFile);
 
 public:
-  QueryLoggingSolver(Solver *_solver, std::string path,
-                     const std::string &commentSign, int queryTimeToLog);
+  QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign,
+                     time::Span queryTimeToLog, bool logTimedOut);
 
   virtual ~QueryLoggingSolver();
 
@@ -72,7 +71,7 @@ public:
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query &);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
 
 #endif /* KLEE_QUERYLOGGINGSOLVER_H */
diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp
index 2f3e97da..f734ac38 100644
--- a/lib/Solver/SMTLIBLoggingSolver.cpp
+++ b/lib/Solver/SMTLIBLoggingSolver.cpp
@@ -43,9 +43,10 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver
         
 	public:
 		SMTLIBLoggingSolver(Solver *_solver,
-                                    std::string path,
-                                    int queryTimeToLog)                
-		: QueryLoggingSolver(_solver, path, ";", queryTimeToLog)
+                        std::string path,
+                        time::Span queryTimeToLog,
+                        bool logTimedOut)
+		: QueryLoggingSolver(_solver, path, ";", queryTimeToLog, logTimedOut)
 		{
 		  //Setup the printer
 		  printer.setOutput(logBuffer);
@@ -54,7 +55,7 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver
 
 
 Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path,
-                                        int minQueryTimeToLog)
+                                        time::Span minQueryTimeToLog, bool logTimedOut)
 {
-  return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog));
+  return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut));
 }
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index d1b8cbdc..6081ff95 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -65,7 +65,7 @@ class STPSolverImpl : public SolverImpl {
 private:
   VC vc;
   STPBuilder *builder;
-  double timeout;
+  time::Span timeout;
   bool useForkedSTP;
   SolverRunStatus runStatusCode;
 
@@ -74,7 +74,7 @@ public:
   ~STPSolverImpl();
 
   char *getConstraintLog(const Query &);
-  void setCoreSolverTimeout(double _timeout) { timeout = _timeout; }
+  void setCoreSolverTimeout(time::Span timeout) { this->timeout = timeout; }
 
   bool computeTruth(const Query &, bool &isValid);
   bool computeValue(const Query &, ref<Expr> &result);
@@ -87,7 +87,7 @@ public:
 
 STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
     : vc(vc_createValidityChecker()),
-      builder(new STPBuilder(vc, _optimizeDivides)), timeout(0.0),
+      builder(new STPBuilder(vc, _optimizeDivides)),
       useForkedSTP(_useForkedSTP), runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
   assert(vc && "unable to create validity checker");
   assert(builder && "unable to create STPBuilder");
@@ -219,7 +219,7 @@ static SolverImpl::SolverRunStatus
 runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
                    const std::vector<const Array *> &objects,
                    std::vector<std::vector<unsigned char> > &values,
-                   bool &hasSolution, double timeout) {
+                   bool &hasSolution, time::Span timeout) {
   unsigned char *pos = shared_memory_ptr;
   unsigned sum = 0;
   for (std::vector<const Array *>::const_iterator it = objects.begin(),
@@ -243,7 +243,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
     if (timeout) {
       ::alarm(0); /* Turn off alarm so we can safely set signal handler */
       ::signal(SIGALRM, stpTimeoutHandler);
-      ::alarm(std::max(1, (int)timeout));
+      ::alarm(std::max(1u, static_cast<unsigned>(timeout.toSeconds())));
     }
     unsigned res = vc_query(vc, q);
     if (!res) {
@@ -326,7 +326,6 @@ bool STPSolverImpl::computeInitialValues(
     const Query &query, const std::vector<const Array *> &objects,
     std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
   runStatusCode = SOLVER_RUN_STATUS_FAILURE;
-
   TimerStatIncrementer t(stats::queryTime);
 
   vc_push(vc);
@@ -383,7 +382,7 @@ char *STPSolver::getConstraintLog(const Query &query) {
   return impl->getConstraintLog(query);
 }
 
-void STPSolver::setCoreSolverTimeout(double timeout) {
+void STPSolver::setCoreSolverTimeout(time::Span timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 }
diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h
index cb68ed91..70b9aa12 100644
--- a/lib/Solver/STPSolver.h
+++ b/lib/Solver/STPSolver.h
@@ -32,7 +32,7 @@ public:
   /// setCoreSolverTimeout - Set constraint solver timeout delay to the given
   /// value; 0
   /// is off.
-  virtual void setCoreSolverTimeout(double timeout);
+  virtual void setCoreSolverTimeout(time::Span timeout);
 };
 }
 
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 3434d2ae..4f7458c5 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -29,7 +29,7 @@ char *Solver::getConstraintLog(const Query& query) {
     return impl->getConstraintLog(query);
 }
 
-void Solver::setCoreSolverTimeout(double timeout) {
+void Solver::setCoreSolverTimeout(time::Span timeout) {
     impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp
index ef79b563..40a7c9e0 100644
--- a/lib/Solver/ValidatingSolver.cpp
+++ b/lib/Solver/ValidatingSolver.cpp
@@ -31,7 +31,7 @@ public:
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query &);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
 
 bool ValidatingSolver::computeTruth(const Query &query, bool &isValid) {
@@ -132,7 +132,7 @@ char *ValidatingSolver::getConstraintLog(const Query &query) {
   return solver->impl->getConstraintLog(query);
 }
 
-void ValidatingSolver::setCoreSolverTimeout(double timeout) {
+void ValidatingSolver::setCoreSolverTimeout(time::Span timeout) {
   solver->impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index f127de9b..5efda6b6 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -47,7 +47,7 @@ namespace klee {
 class Z3SolverImpl : public SolverImpl {
 private:
   Z3Builder *builder;
-  double timeout;
+  time::Span timeout;
   SolverRunStatus runStatusCode;
   std::unique_ptr<llvm::raw_fd_ostream> dumpedQueriesFile;
   ::Z3_params solverParameters;
@@ -65,12 +65,11 @@ public:
   ~Z3SolverImpl();
 
   char *getConstraintLog(const Query &);
-  void setCoreSolverTimeout(double _timeout) {
-    assert(_timeout >= 0.0 && "timeout must be >= 0");
+  void setCoreSolverTimeout(time::Span _timeout) {
     timeout = _timeout;
 
-    unsigned int timeoutInMilliSeconds = (unsigned int)((timeout * 1000) + 0.5);
-    if (timeoutInMilliSeconds == 0)
+    auto timeoutInMilliSeconds = static_cast<unsigned>((timeout.toMicroseconds() / 1000));
+    if (!timeoutInMilliSeconds)
       timeoutInMilliSeconds = UINT_MAX;
     Z3_params_set_uint(builder->ctx, solverParameters, timeoutParamStrSymbol,
                        timeoutInMilliSeconds);
@@ -96,7 +95,7 @@ Z3SolverImpl::Z3SolverImpl()
           /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0
               ? Z3LogInteractionFile.c_str()
               : NULL)),
-      timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
+      runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
   assert(builder && "unable to create Z3Builder");
   solverParameters = Z3_mk_params(builder->ctx);
   Z3_params_inc_ref(builder->ctx, solverParameters);
@@ -134,7 +133,7 @@ char *Z3Solver::getConstraintLog(const Query &query) {
   return impl->getConstraintLog(query);
 }
 
-void Z3Solver::setCoreSolverTimeout(double timeout) {
+void Z3Solver::setCoreSolverTimeout(time::Span timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
 
diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h
index 105c7c75..bed74b88 100644
--- a/lib/Solver/Z3Solver.h
+++ b/lib/Solver/Z3Solver.h
@@ -27,7 +27,7 @@ public:
   /// setCoreSolverTimeout - Set constraint solver timeout delay to the given
   /// value; 0
   /// is off.
-  virtual void setCoreSolverTimeout(double timeout);
+  virtual void setCoreSolverTimeout(time::Span timeout);
 };
 }