From 3caf3e985e4f35ac6ac04f61b92f11d2569550c6 Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Fri, 24 Nov 2017 16:58:27 +0000
Subject: 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)
---
 include/klee/ExecutionState.h             |   3 +-
 include/klee/IncompleteSolver.h           |   2 +-
 include/klee/Internal/Support/Timer.h     |  16 +--
 include/klee/Internal/System/Time.h       | 117 ++++++++++++++---
 include/klee/Solver.h                     |   9 +-
 include/klee/SolverCmdLine.h              |   6 +-
 include/klee/SolverImpl.h                 |   3 +-
 include/klee/TimerStatIncrementer.h       |   5 +-
 lib/Basic/CmdLineOptions.cpp              |  29 +++--
 lib/Basic/ConstructSolverChain.cpp        |  15 ++-
 lib/Core/AddressSpace.cpp                 |   7 +-
 lib/Core/AddressSpace.h                   |   5 +-
 lib/Core/ExecutionState.cpp               |   3 +-
 lib/Core/Executor.cpp                     |  52 ++++----
 lib/Core/Executor.h                       |  11 +-
 lib/Core/ExecutorTimerInfo.h              |   8 +-
 lib/Core/ExecutorTimers.cpp               |  38 +++---
 lib/Core/Searcher.cpp                     |  28 +++--
 lib/Core/Searcher.h                       |  16 ++-
 lib/Core/StatsTracker.cpp                 | 101 ++++++---------
 lib/Core/StatsTracker.h                   |   7 +-
 lib/Core/TimingSolver.cpp                 |   8 +-
 lib/Core/TimingSolver.h                   |   3 +-
 lib/Core/UserSearcher.cpp                 |   8 +-
 lib/Solver/AssignmentValidatingSolver.cpp |   4 +-
 lib/Solver/CachingSolver.cpp              |   4 +-
 lib/Solver/CexCachingSolver.cpp           |   4 +-
 lib/Solver/IncompleteSolver.cpp           |   2 +-
 lib/Solver/IndependentSolver.cpp          |   4 +-
 lib/Solver/KQueryLoggingSolver.cpp        |   9 +-
 lib/Solver/MetaSMTSolver.cpp              |  14 +--
 lib/Solver/MetaSMTSolver.h                |   2 +-
 lib/Solver/QueryLoggingSolver.cpp         |  37 +++---
 lib/Solver/QueryLoggingSolver.h           |  19 ++-
 lib/Solver/SMTLIBLoggingSolver.cpp        |  11 +-
 lib/Solver/STPSolver.cpp                  |  13 +-
 lib/Solver/STPSolver.h                    |   2 +-
 lib/Solver/Solver.cpp                     |   2 +-
 lib/Solver/ValidatingSolver.cpp           |   4 +-
 lib/Solver/Z3Solver.cpp                   |  13 +-
 lib/Solver/Z3Solver.h                     |   2 +-
 lib/Support/Time.cpp                      | 201 +++++++++++++++++++++++++-----
 lib/Support/Timer.cpp                     |  24 +---
 tools/kleaver/main.cpp                    |   5 +-
 tools/klee/main.cpp                       |  75 +++++------
 unittests/CMakeLists.txt                  |   1 +
 unittests/Time/CMakeLists.txt             |   3 +
 unittests/Time/TimeTest.cpp               | 165 ++++++++++++++++++++++++
 48 files changed, 735 insertions(+), 385 deletions(-)
 create mode 100644 unittests/Time/CMakeLists.txt
 create mode 100644 unittests/Time/TimeTest.cpp

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index ceb07864..69b29865 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -13,6 +13,7 @@
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
 #include "klee/Internal/ADT/TreeStream.h"
+#include "klee/Internal/System/Time.h"
 #include "klee/MergeHandler.h"
 
 // FIXME: We do not want to be exposing these? :(
@@ -101,7 +102,7 @@ public:
   /// Statistics and information
 
   /// @brief Costs for all queries issued for this state, in seconds
-  mutable double queryCost;
+  mutable time::Span queryCost;
 
   /// @brief Weight assigned for importance of this state.  Can be
   /// used for searchers to decide what paths to explore
diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h
index f589e3b3..25b6cc68 100644
--- a/include/klee/IncompleteSolver.h
+++ b/include/klee/IncompleteSolver.h
@@ -103,7 +103,7 @@ public:
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query&);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
 
 }
diff --git a/include/klee/Internal/Support/Timer.h b/include/klee/Internal/Support/Timer.h
index d80ccb31..4cbd3f68 100644
--- a/include/klee/Internal/Support/Timer.h
+++ b/include/klee/Internal/Support/Timer.h
@@ -10,25 +10,17 @@
 #ifndef KLEE_TIMER_H
 #define KLEE_TIMER_H
 
-#include <stdint.h>
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-#include <llvm/Support/Chrono.h>
-#endif
+#include "klee/Internal/System/Time.h"
 
 namespace klee {
   class WallTimer {
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-    llvm::sys::TimePoint<> start;
-#else
-    uint64_t startMicroseconds;
-#endif
+    time::Point start;
     
   public:
     WallTimer();
 
-    /// check - Return the delta since the timer was created, in microseconds.
-    uint64_t check();
+    /// check - Return the delta since the timer was created
+    time::Span check();
   };
 }
 
diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
index 12522c86..9c021ddc 100644
--- a/include/klee/Internal/System/Time.h
+++ b/include/klee/Internal/System/Time.h
@@ -10,31 +10,108 @@
 #ifndef KLEE_UTIL_TIME_H
 #define KLEE_UTIL_TIME_H
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-#include <chrono>
+#include "llvm/Support/raw_ostream.h"
 
-#include "llvm/Support/Chrono.h"
-#else
-#include "llvm/Support/TimeValue.h"
-#endif
+#include <chrono>
+#include <string>
+#include <sys/time.h>
 
 namespace klee {
-  namespace util {
+  namespace time {
 
-    /// Seconds spent by this process in user mode.
-    double getUserTime();
+    /// The klee::time namespace offers various functions to measure the time (`getWallTime`)
+    /// and to get timing information for the current KLEE process (`getUserTime`).
+    /// This implementation is based on `std::chrono` and uses time points and time spans.
+    /// For KLEE statistics, spans are converted to µs and stored in `uint64_t`.
 
-    /// Wall time in seconds.
-    double getWallTime();
+    struct Point;
+    struct Span;
 
-    /// Wall time as TimeValue object.
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-    double durationToDouble(std::chrono::nanoseconds dur);
-    llvm::sys::TimePoint<> getWallTimeVal();
-#else
-    llvm::sys::TimeValue getWallTimeVal();
-#endif
-  }
-}
+    /// Returns information about clock
+    std::string getClockInfo();
+
+    /// Returns time spent by this process in user mode
+    Span getUserTime();
+
+    /// Returns point in time using a monotonic steady clock
+    Point getWallTime();
+
+    struct Point {
+      using SteadyTimePoint = std::chrono::steady_clock::time_point;
+
+      SteadyTimePoint point;
+
+      // ctors
+      Point() = default;
+      explicit Point(SteadyTimePoint p): point(p) {};
+
+      // operators
+      Point& operator+=(const Span&);
+      Point& operator-=(const Span&);
+    };
+
+    // operators
+    Point operator+(const Point&, const Span&);
+    Point operator+(const Span&, const Point&);
+    Point operator-(const Point&, const Span&);
+    Span operator-(const Point&, const Point&);
+    bool operator==(const Point&, const Point&);
+    bool operator!=(const Point&, const Point&);
+    bool operator<(const Point&, const Point&);
+    bool operator<=(const Point&, const Point&);
+    bool operator>(const Point&, const Point&);
+    bool operator>=(const Point&, const Point&);
+
+    namespace { using Duration = std::chrono::steady_clock::duration; }
+
+    struct Span {
+      Duration duration = Duration::zero();
+
+      // ctors
+      Span() = default;
+      explicit Span(const Duration &d): duration(d) {}
+      explicit Span(const std::string &s);
+
+      // operators
+      Span& operator=(const Duration&);
+      Span& operator+=(const Span&);
+      Span& operator-=(const Span&);
+      Span& operator*=(const Duration::rep&);
+
+      // conversions
+      explicit operator Duration() const;
+      explicit operator bool() const;
+      explicit operator timeval() const;
+
+      std::uint64_t toMicroseconds() const;
+      double toSeconds() const;
+      std::tuple<std::uint32_t, std::uint8_t, std::uint8_t> toHMS() const; // hours, minutes, seconds
+    };
+
+    Span operator+(const Span&, const Span&);
+    Span operator-(const Span&, const Span&);
+    Span operator*(const Span&, const Duration::rep&);
+    Span operator/(const Span&, const Duration::rep&);
+    Span operator*(const Duration::rep&, const Span&);
+    bool operator==(const Span&, const Span&);
+    bool operator<=(const Span&, const Span&);
+    bool operator>=(const Span&, const Span&);
+    bool operator<(const Span&, const Span&);
+    bool operator>(const Span&, const Span&);
+
+    /// Span -> "X.Ys"
+    std::ostream& operator<<(std::ostream&, Span);
+    llvm::raw_ostream& operator<<(llvm::raw_ostream&, Span);
+
+    /// time spans
+    Span hours(std::uint16_t);
+    Span minutes(std::uint16_t);
+    Span seconds(std::uint64_t);
+    Span milliseconds(std::uint64_t);
+    Span microseconds(std::uint64_t);
+    Span nanoseconds(std::uint64_t);
+
+  } // time
+} // klee
 
 #endif
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index c2a8ef1e..1aaf555d 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -12,6 +12,7 @@
 
 #include "klee/Expr.h"
 #include "klee/SolverCmdLine.h"
+#include "klee/Internal/System/Time.h"
 
 #include <vector>
 
@@ -200,7 +201,7 @@ namespace klee {
     virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
     
     virtual char *getConstraintLog(const Query& query);
-    virtual void setCoreSolverTimeout(double timeout);
+    virtual void setCoreSolverTimeout(time::Span timeout);
   };
 
   /* *** */
@@ -251,12 +252,14 @@ namespace klee {
   /// createKQueryLoggingSolver - Create a solver which will forward all queries
   /// after writing them to the given path in .kquery format.
   Solver *createKQueryLoggingSolver(Solver *s, std::string path,
-                                int minQueryTimeToLog);
+                                    time::Span minQueryTimeToLog,
+                                    bool logTimedOut);
 
   /// createSMTLIBLoggingSolver - Create a solver which will forward all queries
   /// after writing them to the given path in .smt2 format.
   Solver *createSMTLIBLoggingSolver(Solver *s, std::string path,
-                                    int minQueryTimeToLog);
+                                    time::Span minQueryTimeToLog,
+                                    bool logTimedOut);
 
 
   /// createDummySolver - Create a dummy solver implementation which always
diff --git a/include/klee/SolverCmdLine.h b/include/klee/SolverCmdLine.h
index 19e5fae6..82302208 100644
--- a/include/klee/SolverCmdLine.h
+++ b/include/klee/SolverCmdLine.h
@@ -32,9 +32,11 @@ extern llvm::cl::opt<bool> UseIndependentSolver;
 
 extern llvm::cl::opt<bool> DebugValidateSolver;
 
-extern llvm::cl::opt<int> MinQueryTimeToLog;
+extern llvm::cl::opt<std::string> MinQueryTimeToLog;
 
-extern llvm::cl::opt<double> MaxCoreSolverTime;
+extern llvm::cl::opt<bool> LogTimedOutQueries;
+
+extern llvm::cl::opt<std::string> MaxCoreSolverTime;
 
 extern llvm::cl::opt<bool> UseForkedCoreSolver;
 
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h
index 615f20c5..6ea06e2a 100644
--- a/include/klee/SolverImpl.h
+++ b/include/klee/SolverImpl.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_SOLVERIMPL_H
 #define KLEE_SOLVERIMPL_H
 
+#include "klee/Internal/System/Time.h"
 #include "Solver.h"
 
 #include <vector>
@@ -105,7 +106,7 @@ namespace klee {
         return(NULL);
     }
 
-    virtual void setCoreSolverTimeout(double timeout) {};
+    virtual void setCoreSolverTimeout(time::Span timeout) {};
 };
 
 }
diff --git a/include/klee/TimerStatIncrementer.h b/include/klee/TimerStatIncrementer.h
index a351f96b..483d161a 100644
--- a/include/klee/TimerStatIncrementer.h
+++ b/include/klee/TimerStatIncrementer.h
@@ -22,10 +22,11 @@ namespace klee {
   public:
     TimerStatIncrementer(Statistic &_statistic) : statistic(_statistic) {}
     ~TimerStatIncrementer() {
-      statistic += timer.check(); 
+      // record microseconds
+      statistic += timer.check().toMicroseconds();
     }
 
-    uint64_t check() { return timer.check(); }
+    time::Span check() { return timer.check(); }
   };
 }
 
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index b4517d47..b071eab6 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -23,6 +23,15 @@ using namespace llvm;
 
 namespace klee {
 
+cl::extrahelp TimeFormatInfo(
+  "\nTime format used by KLEE's options\n"
+  "\n"
+  "  Time spans can be specified in two ways:\n"
+  "    1. As positive real numbers representing seconds, e.g. '10', '3.5' but not 'INF', 'NaN', '1e3', '-4.5s'\n"
+  "    2. As a sequence of natural numbers with specified units, e.g. '1h10min' (= '70min'), '5min10s' but not '3.5min', '8S'\n"
+  "       The following units are supported: h, min, s, ms, us, ns.\n"
+);
+
 cl::opt<bool>
 UseFastCexSolver("use-fast-cex-solver",
 		 cl::init(false),
@@ -47,19 +56,19 @@ cl::opt<bool>
 DebugValidateSolver("debug-validate-solver",
                     cl::init(false));
   
-cl::opt<int>
+cl::opt<std::string>
 MinQueryTimeToLog("min-query-time-to-log",
-                  cl::init(0),
-                  cl::value_desc("milliseconds"),
-                  cl::desc("Set time threshold (in ms) for queries logged in files. "
-                           "Only queries longer than threshold will be logged. (default=0). "
-                           "Set this param to a negative value to log timeouts only."));
+                  cl::desc("Set time threshold for queries logged in files. "
+                           "Only queries longer than threshold will be logged. (default=0s)"));
+
+cl::opt<bool>
+LogTimedOutQueries("log-timed-out-queries",
+                   cl::init(true),
+                   cl::desc("Log queries that timed out. (default=true)."));
 
-cl::opt<double>
+cl::opt<std::string>
 MaxCoreSolverTime("max-solver-time",
-                  cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"),
-                  cl::init(0.0),
-                  cl::value_desc("seconds"));
+                  cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"));
 
 cl::opt<bool>
 UseForkedCoreSolver("use-forked-solver",
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 5880ad59..8341f62d 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -13,8 +13,10 @@
 #include "klee/Common.h"
 #include "klee/SolverCmdLine.h"
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/Internal/System/Time.h"
 #include "llvm/Support/raw_ostream.h"
 
+
 namespace klee {
 Solver *constructSolverChain(Solver *coreSolver,
                              std::string querySMT2LogPath,
@@ -22,17 +24,16 @@ Solver *constructSolverChain(Solver *coreSolver,
                              std::string queryKQueryLogPath,
                              std::string baseSolverQueryKQueryLogPath) {
   Solver *solver = coreSolver;
+  const time::Span minQueryTimeToLog(MinQueryTimeToLog);
 
   if (queryLoggingOptions.isSet(SOLVER_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath,
-                                   MinQueryTimeToLog);
+    solver = createKQueryLoggingSolver(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);
+    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging queries that reach solver in .smt2 format to %s\n",
                  baseSolverQuerySMT2LogPath.c_str());
   }
@@ -56,15 +57,13 @@ Solver *constructSolverChain(Solver *coreSolver,
     solver = createValidatingSolver(solver, coreSolver);
 
   if (queryLoggingOptions.isSet(ALL_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath,
-                                       MinQueryTimeToLog);
+    solver = createKQueryLoggingSolver(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);
+    solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging all queries in .smt2 format to %s\n",
                  querySMT2LogPath.c_str());
   }
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 0f5a2bb7..fdf9c905 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -196,7 +196,7 @@ int AddressSpace::checkPointerInObject(ExecutionState &state,
 
 bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
                            ref<Expr> p, ResolutionList &rl,
-                           unsigned maxResolutions, double timeout) const {
+                           unsigned maxResolutions, time::Span timeout) const {
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) {
     ObjectPair res;
     if (resolveOne(CE, res))
@@ -204,7 +204,6 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
     return false;
   } else {
     TimerStatIncrementer timer(stats::resolveTime);
-    uint64_t timeout_us = (uint64_t) (timeout * 1000000.);
 
     // XXX in general this isn't exactly what we want... for
     // a multiple resolution case (or for example, a \in {b,c,0})
@@ -238,7 +237,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
     while (oi != begin) {
       --oi;
       const MemoryObject *mo = oi->first;
-      if (timeout_us && timeout_us < timer.check())
+      if (timeout && timeout < timer.check())
         return true;
 
       int incomplete =
@@ -257,7 +256,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
     // search forwards
     for (oi = start; oi != end; ++oi) {
       const MemoryObject *mo = oi->first;
-      if (timeout_us && timeout_us < timer.check())
+      if (timeout && timeout < timer.check())
         return true;
 
       bool mustBeTrue;
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 57c0e472..2554a5b1 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -14,6 +14,7 @@
 
 #include "klee/Expr.h"
 #include "klee/Internal/ADT/ImmutableMap.h"
+#include "klee/Internal/System/Time.h"
 
 namespace klee {
   class ExecutionState;
@@ -61,7 +62,7 @@ namespace klee {
     ///
     /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey
     MemoryMap objects;
-    
+
     AddressSpace() : cowKey(1) {}
     AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) { }
     ~AddressSpace() {}
@@ -97,7 +98,7 @@ namespace klee {
                  ref<Expr> p,
                  ResolutionList &rl, 
                  unsigned maxResolutions=0,
-                 double timeout=0.) const;
+                 time::Span timeout=time::Span()) const;
 
     /***/
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 00e372e4..9ba163da 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -66,7 +66,6 @@ ExecutionState::ExecutionState(KFunction *kf) :
     pc(kf->instructions),
     prevPC(pc),
 
-    queryCost(0.), 
     weight(1),
     depth(0),
 
@@ -79,7 +78,7 @@ ExecutionState::ExecutionState(KFunction *kf) :
 }
 
 ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
-    : constraints(assumptions), queryCost(0.), ptreeNode(0) {}
+    : constraints(assumptions), ptreeNode(0) {}
 
 ExecutionState::~ExecutionState() {
   for (unsigned int i=0; i<symbolics.size(); i++)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 2e5b864c..ddf11929 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -244,15 +244,13 @@ namespace {
 		      cl::init(1.),
 		      cl::desc("(default=1.0)"));
 
-  cl::opt<double>
+  cl::opt<std::string>
   MaxInstructionTime("max-instruction-time",
-                     cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-solver"),
-                     cl::init(0));
+                     cl::desc("Allow a single instruction to take only this much time (default=0s (off)). Enables --use-forked-solver"));
   
-  cl::opt<double>
+  cl::opt<std::string>
   SeedTime("seed-time",
-           cl::desc("Amount of time to dedicate to seeds, before normal search (default=0 (off))"),
-           cl::init(0));
+           cl::desc("Amount of time to dedicate to seeds, before normal search (default=0s (off))"));
   
   cl::list<Executor::TerminateReason>
   ExitOnErrorType("exit-on-error-type",
@@ -328,11 +326,14 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
       processTree(0), replayKTest(0), replayPath(0), usingSeeds(0),
       atMemoryLimit(false), inhibitForking(false), haltExecution(false),
-      ivcEnabled(false),
-      coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0
-                            ? std::min(MaxCoreSolverTime, MaxInstructionTime)
-                            : std::max(MaxCoreSolverTime, MaxInstructionTime)),
-      debugLogBuffer(debugBufferString) {
+      ivcEnabled(false), debugLogBuffer(debugBufferString) {
+
+
+  const time::Span maxCoreSolverTime(MaxCoreSolverTime);
+  maxInstructionTime = time::Span(MaxInstructionTime);
+  coreSolverTimeout = maxCoreSolverTime && maxInstructionTime ?
+                      std::min(maxCoreSolverTime, maxInstructionTime)
+                    : std::max(maxCoreSolverTime, maxInstructionTime);
 
   if (coreSolverTimeout) UseForkedCoreSolver = true;
   Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
@@ -779,7 +780,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
   if (!isSeeding && !isa<ConstantExpr>(condition) && 
       (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. ||
        MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) &&
-      statsTracker->elapsed() > 60.) {
+      statsTracker->elapsed() > time::seconds(60)) {
     StatisticManager &sm = *theStatisticManager;
     CallPathNode *cpn = current.stack.back().callPathNode;
     if ((MaxStaticForkPct<1. &&
@@ -803,12 +804,12 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     }
   }
 
-  double timeout = coreSolverTimeout;
+  time::Span timeout = coreSolverTimeout;
   if (isSeeding)
     timeout *= it->second.size();
   solver->setTimeout(timeout);
   bool success = solver->evaluate(current, condition, res);
-  solver->setTimeout(0);
+  solver->setTimeout(time::Span());
   if (!success) {
     current.pc = current.prevPC;
     terminateStateEarly(current, "Query timed out (fork).");
@@ -1076,7 +1077,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
       if (solver->mustBeTrue(state, cond, isTrue) && isTrue)
         result = value;
     }
-    solver->setTimeout(0);
+    solver->setTimeout(time::Span());
   }
   
   return result;
@@ -2774,7 +2775,7 @@ void Executor::run(ExecutionState &initialState) {
       v.push_back(SeedInfo(*it));
 
     int lastNumSeeds = usingSeeds->size()+10;
-    double lastTime, startTime = lastTime = util::getWallTime();
+    time::Point lastTime, startTime = lastTime = time::getWallTime();
     ExecutionState *lastState = 0;
     while (!seedMap.empty()) {
       if (haltExecution) {
@@ -2793,7 +2794,7 @@ void Executor::run(ExecutionState &initialState) {
       stepInstruction(state);
 
       executeInstruction(state, ki);
-      processTimers(&state, MaxInstructionTime * numSeeds);
+      processTimers(&state, maxInstructionTime * numSeeds);
       updateStates(&state);
 
       if ((stats::instructions % 1000) == 0) {
@@ -2804,13 +2805,14 @@ void Executor::run(ExecutionState &initialState) {
           numSeeds += it->second.size();
           numStates++;
         }
-        double time = util::getWallTime();
-        if (SeedTime>0. && time > startTime + SeedTime) {
+        const auto time = time::getWallTime();
+        const time::Span seedTime(SeedTime);
+        if (seedTime && time > startTime + seedTime) {
           klee_warning("seed time expired, %d seeds remain over %d states",
                        numSeeds, numStates);
           break;
         } else if (numSeeds<=lastNumSeeds-10 ||
-                   time >= lastTime+10) {
+                   time - lastTime >= time::seconds(10)) {
           lastTime = time;
           lastNumSeeds = numSeeds;          
           klee_message("%d seeds remaining over: %d states", 
@@ -2846,7 +2848,7 @@ void Executor::run(ExecutionState &initialState) {
     stepInstruction(state);
 
     executeInstruction(state, ki);
-    processTimers(&state, MaxInstructionTime);
+    processTimers(&state, maxInstructionTime);
 
     checkMemoryUsage();
 
@@ -3457,7 +3459,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     address = toConstant(state, address, "resolveOne failure");
     success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
   }
-  solver->setTimeout(0);
+  solver->setTimeout(time::Span());
 
   if (success) {
     const MemoryObject *mo = op.first;
@@ -3473,7 +3475,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     bool inBounds;
     solver->setTimeout(coreSolverTimeout);
     bool success = solver->mustBeTrue(state, check, inBounds);
-    solver->setTimeout(0);
+    solver->setTimeout(time::Span());
     if (!success) {
       state.pc = state.prevPC;
       terminateStateEarly(state, "Query timed out (bounds check).");
@@ -3511,7 +3513,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   solver->setTimeout(coreSolverTimeout);
   bool incomplete = state.addressSpace.resolve(state, solver, address, rl,
                                                0, coreSolverTimeout);
-  solver->setTimeout(0);
+  solver->setTimeout(time::Span());
   
   // XXX there is some query wasteage here. who cares?
   ExecutionState *unbound = &state;
@@ -3827,7 +3829,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   for (unsigned i = 0; i != state.symbolics.size(); ++i)
     objects.push_back(state.symbolics[i].second);
   bool success = solver->getInitialValues(tmp, objects, values);
-  solver->setTimeout(0);
+  solver->setTimeout(time::Span());
   if (!success) {
     klee_warning("unable to compute initial values (invalid constraints?)!");
     ExprPPrinter::printQuery(llvm::errs(), state.constraints,
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 3643c3f4..180c9140 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -20,6 +20,7 @@
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Module/KModule.h"
+#include "klee/Internal/System/Time.h"
 #include "klee/util/ArrayCache.h"
 #include "llvm/Support/raw_ostream.h"
 
@@ -216,7 +217,10 @@ private:
 
   /// The maximum time to allow for a single core solver query.
   /// (e.g. for a single STP query)
-  double coreSolverTimeout;
+  time::Span coreSolverTimeout;
+
+  /// Maximum time to allow for a single instruction.
+  time::Span maxInstructionTime;
 
   /// Assumes ownership of the created array objects
   ArrayCache arrayCache;
@@ -461,11 +465,10 @@ private:
   ///
   /// \param timer The timer object to run on firings.
   /// \param rate The approximate delay (in seconds) between firings.
-  void addTimer(Timer *timer, double rate);
+  void addTimer(Timer *timer, time::Span rate);
 
   void initTimers();
-  void processTimers(ExecutionState *current,
-                     double maxInstTime);
+  void processTimers(ExecutionState *current, time::Span maxInstTime);
   void checkMemoryUsage();
   void printDebugInstructions(ExecutionState &state);
   void doDumpStates();
diff --git a/lib/Core/ExecutorTimerInfo.h b/lib/Core/ExecutorTimerInfo.h
index 60977b74..9127fb68 100644
--- a/lib/Core/ExecutorTimerInfo.h
+++ b/lib/Core/ExecutorTimerInfo.h
@@ -23,15 +23,15 @@ public:
   Timer *timer;
 
   /// Approximate delay per timer firing.
-  double rate;
+  time::Span rate;
   /// Wall time for next firing.
-  double nextFireTime;
+  time::Point nextFireTime;
 
 public:
-  TimerInfo(Timer *_timer, double _rate)
+  TimerInfo(Timer *_timer, time::Span _rate)
     : timer(_timer),
       rate(_rate),
-      nextFireTime(util::getWallTime() + rate) {}
+      nextFireTime(time::getWallTime() + rate) {}
   ~TimerInfo() { delete timer; }
 };
 
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index a3c13530..de24d75d 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -23,6 +23,7 @@
 #include "llvm/IR/Function.h"
 #include "llvm/Support/CommandLine.h"
 
+#include <string>
 #include <unistd.h>
 #include <signal.h>
 #include <sys/time.h>
@@ -32,10 +33,9 @@
 using namespace llvm;
 using namespace klee;
 
-cl::opt<double>
+cl::opt<std::string>
 MaxTime("max-time",
-        cl::desc("Halt execution after the specified number of seconds (default=0 (off))"),
-        cl::init(0));
+        cl::desc("Halt execution after the specified number of seconds (default=0s (off))"));
 
 ///
 
@@ -54,7 +54,7 @@ public:
 
 ///
 
-static const double kSecondsPerTick = .1;
+static const time::Span kMilliSecondsPerTick(time::milliseconds(100));
 static volatile unsigned timerTicks = 0;
 
 // XXX hack
@@ -67,15 +67,11 @@ static void onAlarm(int) {
 
 // oooogalay
 static void setupHandler() {
-  struct itimerval t;
-  struct timeval tv;
-  
-  tv.tv_sec = (long) kSecondsPerTick;
-  tv.tv_usec = (long) (fmod(kSecondsPerTick, 1.)*1000000);
-  
+  itimerval t{};
+  timeval tv = static_cast<timeval>(kMilliSecondsPerTick);
   t.it_interval = t.it_value = tv;
-  
-  ::setitimer(ITIMER_REAL, &t, 0);
+
+  ::setitimer(ITIMER_REAL, &t, nullptr);
   ::signal(SIGALRM, onAlarm);
 }
 
@@ -87,8 +83,9 @@ void Executor::initTimers() {
     setupHandler();
   }
 
-  if (MaxTime) {
-    addTimer(new HaltTimer(this), MaxTime.getValue());
+  const time::Span maxTime(MaxTime);
+  if (maxTime) {
+    addTimer(new HaltTimer(this), maxTime);
   }
 }
 
@@ -98,12 +95,12 @@ Executor::Timer::Timer() {}
 
 Executor::Timer::~Timer() {}
 
-void Executor::addTimer(Timer *timer, double rate) {
+void Executor::addTimer(Timer *timer, time::Span rate) {
   timers.push_back(new TimerInfo(timer, rate));
 }
 
 void Executor::processTimers(ExecutionState *current,
-                             double maxInstTime) {
+                             time::Span maxInstTime) {
   static unsigned callsWithoutCheck = 0;
   unsigned ticks = timerTicks;
 
@@ -169,18 +166,17 @@ void Executor::processTimers(ExecutionState *current,
       dumpStates = 0;
     }
 
-    if (maxInstTime > 0 && current &&
+    if (maxInstTime && current &&
         std::find(removedStates.begin(), removedStates.end(), current) ==
             removedStates.end()) {
-      if (timerTicks*kSecondsPerTick > maxInstTime) {
-        klee_warning("max-instruction-time exceeded: %.2fs",
-                     timerTicks*kSecondsPerTick);
+      if (timerTicks*kMilliSecondsPerTick > maxInstTime) {
+        klee_warning("max-instruction-time exceeded: %.2fs", (timerTicks * kMilliSecondsPerTick).toSeconds());
         terminateStateEarly(*current, "max-instruction-time exceeded");
       }
     }
 
     if (!timers.empty()) {
-      double time = util::getWallTime();
+      auto time = time::getWallTime();
 
       for (std::vector<TimerInfo*>::iterator it = timers.begin(), 
              ie = timers.end(); it != ie; ++it) {
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 0c1f4316..cce83d23 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -214,7 +214,7 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
     return inv;
   }
   case QueryCost:
-    return (es->queryCost < .1) ? 1. : 1./es->queryCost;
+    return (es->queryCost.toSeconds() < .1) ? 1. : 1./ es->queryCost.toSeconds();
   case CoveringNew:
   case MinDistToUncovered: {
     uint64_t md2u = computeMinDistToUncovered(es->pc,
@@ -337,7 +337,7 @@ ExecutionState& MergingSearcher::selectState() {
 ///
 
 BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher,
-                                   double _timeBudget,
+                                   time::Span _timeBudget,
                                    unsigned _instructionBudget) 
   : baseSearcher(_baseSearcher),
     timeBudget(_timeBudget),
@@ -352,18 +352,19 @@ BatchingSearcher::~BatchingSearcher() {
 
 ExecutionState &BatchingSearcher::selectState() {
   if (!lastState || 
-      (util::getWallTime()-lastStartTime)>timeBudget ||
-      (stats::instructions-lastStartInstructions)>instructionBudget) {
+      (time::getWallTime() - lastStartTime) > timeBudget ||
+      (stats::instructions - lastStartInstructions) > instructionBudget) {
     if (lastState) {
-      double delta = util::getWallTime()-lastStartTime;
-      if (delta>timeBudget*1.1) {
-        klee_message("increased time budget from %f to %f\n", timeBudget,
-                     delta);
+      time::Span delta = time::getWallTime() - lastStartTime;
+      auto t = timeBudget;
+      t *= 1.1;
+      if (delta > t) {
+        klee_message("increased time budget from %f to %f\n", timeBudget.toSeconds(), delta.toSeconds());
         timeBudget = delta;
       }
     }
     lastState = &baseSearcher->selectState();
-    lastStartTime = util::getWallTime();
+    lastStartTime = time::getWallTime();
     lastStartInstructions = stats::instructions;
     return *lastState;
   } else {
@@ -385,7 +386,7 @@ BatchingSearcher::update(ExecutionState *current,
 
 IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(Searcher *_baseSearcher)
   : baseSearcher(_baseSearcher),
-    time(1.) {
+    time(time::seconds(1)) {
 }
 
 IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher() {
@@ -394,14 +395,15 @@ IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher() {
 
 ExecutionState &IterativeDeepeningTimeSearcher::selectState() {
   ExecutionState &res = baseSearcher->selectState();
-  startTime = util::getWallTime();
+  startTime = time::getWallTime();
   return res;
 }
 
 void IterativeDeepeningTimeSearcher::update(
     ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
     const std::vector<ExecutionState *> &removedStates) {
-  double elapsed = util::getWallTime() - startTime;
+
+  const auto elapsed = time::getWallTime() - startTime;
 
   if (!removedStates.empty()) {
     std::vector<ExecutionState *> alt = removedStates;
@@ -431,7 +433,7 @@ void IterativeDeepeningTimeSearcher::update(
 
   if (baseSearcher->empty()) {
     time *= 2;
-    klee_message("increased time budget to %f\n", time);
+    klee_message("increased time budget to %f\n", time.toSeconds());
     std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
     baseSearcher->update(0, ps, std::vector<ExecutionState *>());
     pausedStates.clear();
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 47026410..dc0e12a4 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -10,11 +10,14 @@
 #ifndef KLEE_SEARCHER_H
 #define KLEE_SEARCHER_H
 
+#include "klee/Internal/System/Time.h"
+
 #include "llvm/Support/raw_ostream.h"
-#include <vector>
-#include <set>
+
 #include <map>
 #include <queue>
+#include <set>
+#include <vector>
 
 namespace llvm {
   class BasicBlock;
@@ -208,16 +211,16 @@ namespace klee {
 
   class BatchingSearcher : public Searcher {
     Searcher *baseSearcher;
-    double timeBudget;
+    time::Span timeBudget;
     unsigned instructionBudget;
 
     ExecutionState *lastState;
-    double lastStartTime;
+    time::Point lastStartTime;
     unsigned lastStartInstructions;
 
   public:
     BatchingSearcher(Searcher *baseSearcher, 
-                     double _timeBudget,
+                     time::Span _timeBudget,
                      unsigned _instructionBudget);
     ~BatchingSearcher();
 
@@ -237,7 +240,8 @@ namespace klee {
 
   class IterativeDeepeningTimeSearcher : public Searcher {
     Searcher *baseSearcher;
-    double time, startTime;
+    time::Point startTime;
+    time::Span time;
     std::set<ExecutionState*> pausedStates;
 
   public:
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index dee14e61..5ad0f174 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -17,7 +17,6 @@
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/MemoryUsage.h"
-#include "klee/Internal/System/Time.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/SolverStats.h"
 
@@ -71,20 +70,20 @@ namespace {
 	       cl::init(true),
                cl::desc("Write instruction level statistics in callgrind format (default=on)"));
 
-  cl::opt<double>
+  cl::opt<std::string>
   StatsWriteInterval("stats-write-interval",
-                     cl::init(1.),
-		     cl::desc("Approximate number of seconds between stats writes (default=1.0s)"));
+                     cl::init("1s"),
+                     cl::desc("Approximate time between stats writes (default=1s)"));
 
   cl::opt<unsigned> StatsWriteAfterInstructions(
       "stats-write-after-instructions", cl::init(0),
       cl::desc("Write statistics after each n instructions, 0 to disable "
                "(default=0)"));
 
-  cl::opt<double>
+  cl::opt<std::string>
   IStatsWriteInterval("istats-write-interval",
-		      cl::init(10.),
-                      cl::desc("Approximate number of seconds between istats writes (default: 10.0s)"));
+                      cl::init("10s"),
+                      cl::desc("Approximate number of seconds between istats writes (default=10s)"));
 
   cl::opt<unsigned> IStatsWriteAfterInstructions(
       "istats-write-after-instructions", cl::init(0),
@@ -92,10 +91,10 @@ namespace {
                "(default=0)"));
 
   // XXX I really would like to have dynamic rate control for something like this.
-  cl::opt<double>
+  cl::opt<std::string>
   UncoveredUpdateInterval("uncovered-update-interval",
-                          cl::init(30.),
-			  cl::desc("(default=30.0s)"));
+                          cl::init("30s"),
+                          cl::desc("(default=30s)"));
   
   cl::opt<bool>
   UseCallPaths("use-call-paths",
@@ -176,18 +175,20 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
                            bool _updateMinDistToUncovered)
   : executor(_executor),
     objectFilename(_objectFilename),
-    startWallTime(util::getWallTime()),
+    startWallTime(time::getWallTime()),
     numBranches(0),
     fullBranches(0),
     partialBranches(0),
     updateMinDistToUncovered(_updateMinDistToUncovered) {
 
-  if (StatsWriteAfterInstructions > 0 && StatsWriteInterval > 0)
+  const time::Span statsWriteInterval(StatsWriteInterval);
+  if (StatsWriteAfterInstructions > 0 && statsWriteInterval)
     klee_error("Both options --stats-write-interval and "
                "--stats-write-after-instructions cannot be enabled at the same "
                "time.");
 
-  if (IStatsWriteAfterInstructions > 0 && IStatsWriteInterval > 0)
+  const time::Span iStatsWriteInterval(IStatsWriteInterval);
+  if (IStatsWriteAfterInstructions > 0 && iStatsWriteInterval)
     klee_error(
         "Both options --istats-write-interval and "
         "--istats-write-after-instructions cannot be enabled at the same "
@@ -245,8 +246,8 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
       writeStatsHeader();
       writeStatsLine();
 
-      if (StatsWriteInterval > 0)
-        executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval);
+      if (statsWriteInterval)
+        executor.addTimer(new WriteStatsTimer(this), statsWriteInterval);
     } else {
       klee_error("Unable to open statistics trace file (run.stats).");
     }
@@ -255,14 +256,14 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
   // Add timer to calculate uncovered instructions if needed by the solver
   if (updateMinDistToUncovered) {
     computeReachableUncovered();
-    executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval);
+    executor.addTimer(new UpdateReachableTimer(this), time::Span(UncoveredUpdateInterval));
   }
 
   if (OutputIStats) {
     istatsFile = executor.interpreterHandler->openOutputFile("run.istats");
     if (istatsFile) {
-      if (IStatsWriteInterval > 0)
-        executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval);
+      if (iStatsWriteInterval)
+        executor.addTimer(new WriteIStatsTimer(this), iStatsWriteInterval);
     } else {
       klee_error("Unable to open instruction level stats file (run.istats).");
     }
@@ -284,45 +285,21 @@ void StatsTracker::done() {
 void StatsTracker::stepInstruction(ExecutionState &es) {
   if (OutputIStats) {
     if (TrackInstructionTime) {
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-      static sys::TimePoint<> lastNowTime;
-      static std::chrono::nanoseconds lastUserTime(0);
+      static time::Point lastNowTime(time::getWallTime());
+      static time::Span lastUserTime;
 
-      if (lastUserTime.count() == 0) {
-        std::chrono::nanoseconds sys;
-        sys::Process::GetTimeUsage(lastNowTime, lastUserTime, sys);
+      if (!lastUserTime) {
+        lastUserTime = time::getUserTime();
       } else {
-        sys::TimePoint<> now;
-        std::chrono::nanoseconds user, sys;
-
-        sys::Process::GetTimeUsage(now, user, sys);
-
-        auto delta =
-          std::chrono::duration_cast<std::chrono::microseconds>(user - lastUserTime);
-        auto deltaNow =
-          std::chrono::duration_cast<std::chrono::microseconds>(now - lastNowTime);
-        stats::instructionTime += delta.count();
-        stats::instructionRealTime += deltaNow.count();
+        const auto now = time::getWallTime();
+        const auto user = time::getUserTime();
+        const auto delta = user - lastUserTime;
+        const auto deltaNow = now - lastNowTime;
+        stats::instructionTime += delta.toMicroseconds();
+        stats::instructionRealTime += deltaNow.toMicroseconds();
         lastUserTime = user;
         lastNowTime = now;
       }
-#else
-      static sys::TimeValue lastNowTime(0,0),lastUserTime(0,0);
-    
-      if (lastUserTime.seconds()==0 && lastUserTime.nanoseconds()==0) {
-        sys::TimeValue sys(0,0);
-        sys::Process::GetTimeUsage(lastNowTime,lastUserTime,sys);
-      } else {
-        sys::TimeValue now(0,0),user(0,0),sys(0,0);
-        sys::Process::GetTimeUsage(now,user,sys);
-        sys::TimeValue delta = user - lastUserTime;
-        sys::TimeValue deltaNow = now - lastNowTime;
-        stats::instructionTime += delta.usec();
-        stats::instructionRealTime += deltaNow.usec();
-        lastUserTime = user;
-        lastNowTime = now;
-      }
-#endif
     }
 
     Instruction *inst = es.pc->inst;
@@ -447,8 +424,8 @@ void StatsTracker::writeStatsHeader() {
   statsFile->flush();
 }
 
-double StatsTracker::elapsed() {
-  return util::getWallTime() - startWallTime;
+time::Span StatsTracker::elapsed() {
+  return time::getWallTime() - startWallTime;
 }
 
 void StatsTracker::writeStatsLine() {
@@ -456,24 +433,24 @@ void StatsTracker::writeStatsLine() {
              << "," << fullBranches
              << "," << partialBranches
              << "," << numBranches
-             << "," << util::getUserTime()
+             << "," << time::getUserTime().toSeconds()
              << "," << executor.states.size()
              << "," << util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize()
              << "," << stats::queries
              << "," << stats::queryConstructs
              << "," << 0 // was numObjects
-             << "," << elapsed()
+             << "," << elapsed().toSeconds()
              << "," << stats::coveredInstructions
              << "," << stats::uncoveredInstructions
-             << "," << stats::queryTime / 1000000.
-             << "," << stats::solverTime / 1000000.
-             << "," << stats::cexCacheTime / 1000000.
-             << "," << stats::forkTime / 1000000.
-             << "," << stats::resolveTime / 1000000.
+             << "," << time::microseconds(stats::queryTime).toSeconds()
+             << "," << time::microseconds(stats::solverTime).toSeconds()
+             << "," << time::microseconds(stats::cexCacheTime).toSeconds()
+             << "," << time::microseconds(stats::forkTime).toSeconds()
+             << "," << time::microseconds(stats::resolveTime).toSeconds()
              << "," << stats::queryCexCacheMisses
              << "," << stats::queryCexCacheHits
 #ifdef KLEE_ARRAY_DEBUG
-             << "," << stats::arrayHashTime / 1000000.
+             << "," << time::microseconds(stats::arrayHashTime).toSeconds()
 #endif
              << ")\n";
   statsFile->flush();
diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h
index e352bb91..88e4cf30 100644
--- a/lib/Core/StatsTracker.h
+++ b/lib/Core/StatsTracker.h
@@ -11,6 +11,7 @@
 #define KLEE_STATSTRACKER_H
 
 #include "CallPathManager.h"
+#include "klee/Internal/System/Time.h"
 
 #include <memory>
 #include <set>
@@ -38,7 +39,7 @@ namespace klee {
     std::string objectFilename;
 
     std::unique_ptr<llvm::raw_fd_ostream> statsFile, istatsFile;
-    double startWallTime;
+    time::Point startWallTime;
 
     unsigned numBranches;
     unsigned fullBranches, partialBranches;
@@ -81,8 +82,8 @@ namespace klee {
     // about to be stepped
     void stepInstruction(ExecutionState &es);
 
-    /// Return time in seconds since execution start.
-    double elapsed();
+    /// Return duration since execution start.
+    time::Span elapsed();
 
     void computeReachableUncovered();
   };
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 3b66f641..0f69509a 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -37,7 +37,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
 
   bool success = solver->evaluate(Query(state.constraints, expr), result);
 
-  state.queryCost += timer.check() / 1e6;
+  state.queryCost += timer.check();
 
   return success;
 }
@@ -57,7 +57,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
 
   bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
 
-  state.queryCost += timer.check() / 1e6;
+  state.queryCost += timer.check();
 
   return success;
 }
@@ -100,7 +100,7 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
 
   bool success = solver->getValue(Query(state.constraints, expr), result);
 
-  state.queryCost += timer.check() / 1e6;
+  state.queryCost += timer.check();
 
   return success;
 }
@@ -120,7 +120,7 @@ TimingSolver::getInitialValues(const ExecutionState& state,
                                                 ConstantExpr::alloc(0, Expr::Bool)), 
                                           objects, result);
   
-  state.queryCost += timer.check() / 1e6;
+  state.queryCost += timer.check();
   
   return success;
 }
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index c98dd881..08ed0de2 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -12,6 +12,7 @@
 
 #include "klee/Expr.h"
 #include "klee/Solver.h"
+#include "klee/Internal/System/Time.h"
 
 #include <vector>
 
@@ -38,7 +39,7 @@ namespace klee {
       delete solver;
     }
 
-    void setTimeout(double t) {
+    void setTimeout(time::Span t) {
       solver->setCoreSolverTimeout(t);
     }
     
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index aa90c401..934cef54 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -51,10 +51,10 @@ namespace {
                     cl::desc("Number of instructions to batch when using --use-batching-search"),
                     cl::init(10000));
   
-  cl::opt<double>
+  cl::opt<std::string>
   BatchTime("batch-time",
-            cl::desc("Amount of time to batch when using --use-batching-search"),
-            cl::init(5.0));
+            cl::desc("Amount of time to batch when using --use-batching-search (default=5s)"),
+            cl::init("5s"));
 
 }
 
@@ -120,7 +120,7 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
   }
 
   if (UseBatchingSearch) {
-    searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions);
+    searcher = new BatchingSearcher(searcher, time::Span(BatchTime), BatchInstructions);
   }
 
   if (UseMerge && UseIncompleteMerge) {
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);
 };
 }
 
diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp
index f508e6fa..7cd9659b 100644
--- a/lib/Support/Time.cpp
+++ b/lib/Support/Time.cpp
@@ -7,58 +7,193 @@
 //
 //===----------------------------------------------------------------------===//
 
-#include "klee/Config/Version.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/Internal/System/Time.h"
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-#include <chrono>
 
-#include <llvm/Support/Chrono.h>
-#else
-#include "llvm/Support/TimeValue.h"
-#endif
+#include <cstdint>
+#include <regex>
+#include <sstream>
+#include <tuple>
+#include <sys/resource.h>
 
-#include "llvm/Support/Process.h"
 
-using namespace llvm;
 using namespace klee;
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-double util::durationToDouble(std::chrono::nanoseconds dur)
-{
-  return dur.count() / 1e9;
+
+/* Why std::chrono:
+ * - C++11
+ * - separation between time points and durations
+ * - good performance on Linux and macOS (similar to gettimeofday)
+ * and not:
+ * - clock_gettime(CLOCK_MONOTONIC_COARSE): software clock, Linux-specific
+ * - clock_gettime(CLOCK_MONOTONIC): slowest on macOS, C-like API
+ * - gettimeofday: C-like API, non-monotonic
+ *
+ * TODO: add time literals with C++14
+ */
+
+// === Point ===
+
+// operators
+time::Point& time::Point::operator+=(const time::Span &span) { point += span.duration; return *this; }
+time::Point& time::Point::operator-=(const time::Span &span) { point -= span.duration; return *this; }
+
+time::Point time::operator+(const time::Point &point, const time::Span &span) { return time::Point(point.point + span.duration); }
+time::Point time::operator+(const time::Span &span, const time::Point &point) { return time::Point(point.point + span.duration); }
+time::Point time::operator-(const time::Point &point, const time::Span &span) { return time::Point(point.point - span.duration); }
+time::Span time::operator-(const time::Point &lhs, const time::Point &rhs) { return time::Span(lhs.point - rhs.point); }
+bool time::operator==(const time::Point &lhs, const time::Point &rhs) { return lhs.point == rhs.point; }
+bool time::operator!=(const time::Point &lhs, const time::Point &rhs) { return lhs.point != rhs.point; }
+bool time::operator<(const time::Point &lhs, const time::Point &rhs) { return lhs.point < rhs.point; }
+bool time::operator<=(const time::Point &lhs, const time::Point &rhs) { return lhs.point <= rhs.point; }
+bool time::operator>(const time::Point &lhs, const time::Point &rhs) { return lhs.point > rhs.point; }
+bool time::operator>=(const time::Point &lhs, const time::Point &rhs) { return lhs.point >= rhs.point; }
+
+
+// === Span ===
+
+// ctors
+/// returns span from string in old (X.Y) and new (3h4min) format
+time::Span::Span(const std::string &s) {
+  if (s.empty()) return;
+
+  std::regex re("^([0-9]*\\.?[0-9]+)|((([0-9]+)(h|min|s|ms|us|ns))+)$", std::regex::extended);
+  std::regex nre("([0-9]+)(h|min|s|ms|us|ns)", std::regex::extended);
+  std::smatch match;
+  std::string submatch;
+
+  // error
+  if (!std::regex_match(s, match, re)) goto error;
+
+  // old (double) format
+  submatch = match[1].str();
+  if (match[1].matched) {
+    errno = 0;
+    auto value = std::stod(submatch);
+    if (errno) goto error;
+
+    std::chrono::duration<double> d(value);
+    duration = std::chrono::duration_cast<std::chrono::microseconds>(d);
+  }
+
+  // new (string) format
+  submatch = match[2].str();
+  for (std::smatch m; std::regex_search(submatch, m, nre); submatch = m.suffix()) {
+    errno = 0;
+    const auto value = std::stoull(m[1]);
+    if (errno) goto error;
+
+    Duration d;
+    if (m[2] == "h") d = std::chrono::hours(value);
+    else if (m[2] == "min") d = std::chrono::minutes(value);
+    else if (m[2] ==   "s") d = std::chrono::seconds(value);
+    else if (m[2] ==  "ms") d = std::chrono::milliseconds(value);
+    else if (m[2] ==  "us") d = std::chrono::microseconds(value);
+    else if (m[2] ==  "ns") d = std::chrono::nanoseconds(value);
+    else goto error;
+
+    duration += d;
+  }
+
+  return;
+
+error:
+  klee_error("Illegal number format: %s", s.c_str());
 }
 
-double util::getUserTime() {
-  sys::TimePoint<> now;
-  std::chrono::nanoseconds user, sys;
+// operators
+time::Span& time::Span::operator=(const time::Duration &d) { duration = d; return *this; };
+time::Span& time::Span::operator+=(const time::Span &other) { duration += other.duration; return *this; }
+time::Span& time::Span::operator-=(const time::Span &other) { duration -= other.duration; return *this; }
+time::Span& time::Span::operator*=(const time::Duration::rep &rep) { duration *= rep; return *this; }
+
+time::Span time::operator+(const time::Span &lhs, const time::Span &rhs) { return time::Span(lhs.duration + rhs.duration); }
+time::Span time::operator-(const time::Span &lhs, const time::Span &rhs) { return time::Span(lhs.duration - rhs.duration); }
+time::Span time::operator*(const time::Span &span, const time::Duration::rep &rep) { return time::Span(span.duration * rep); }
+time::Span time::operator*(const time::Duration::rep &rep, const time::Span &span) { return time::Span(span.duration * rep); }
+time::Span time::operator/(const time::Span &span, const time::Duration::rep &rep) { return time::Span(span.duration / rep); }
+bool time::operator==(const time::Span &lhs, const time::Span &rhs) { return lhs.duration == rhs.duration; }
+bool time::operator<=(const time::Span &lhs, const time::Span &rhs) { return lhs.duration <= rhs.duration; }
+bool time::operator>=(const time::Span &lhs, const time::Span &rhs) { return lhs.duration >= rhs.duration; }
+bool time::operator<(const time::Span &lhs, const time::Span &rhs) { return lhs.duration < rhs.duration; }
+bool time::operator>(const time::Span &lhs, const time::Span &rhs) { return lhs.duration > rhs.duration; }
+
+std::ostream& time::operator<<(std::ostream &stream, time::Span span) { return stream << span.toSeconds() << 's'; }
+llvm::raw_ostream& time::operator<<(llvm::raw_ostream &stream, time::Span span) { return stream << span.toSeconds() << 's'; }
+
 
-  sys::Process::GetTimeUsage(now, user, sys);
+// units
+time::Span time::hours(std::uint16_t ticks) { return time::Span(std::chrono::hours(ticks)); }
+time::Span time::minutes(std::uint16_t ticks) { return time::Span(std::chrono::minutes(ticks)); }
+time::Span time::seconds(std::uint64_t ticks) { return time::Span(std::chrono::seconds(ticks)); }
+time::Span time::milliseconds(std::uint64_t ticks) { return time::Span(std::chrono::milliseconds(ticks)); }
+time::Span time::microseconds(std::uint64_t ticks) { return time::Span(std::chrono::microseconds(ticks)); }
+time::Span time::nanoseconds(std::uint64_t ticks) { return time::Span(std::chrono::nanoseconds(ticks)); }
 
-  return durationToDouble(user);
+
+// conversions
+time::Span::operator time::Duration() const { return duration; }
+
+time::Span::operator bool() const { return duration.count() != 0; }
+
+time::Span::operator timeval() const {
+  timeval tv{};
+  const auto secs = std::chrono::duration_cast<std::chrono::seconds>(duration);
+  const auto usecs = std::chrono::duration_cast<std::chrono::microseconds>(duration - secs);
+  tv.tv_sec = secs.count();
+  tv.tv_usec = usecs.count();
+  return tv;
 }
 
-double util::getWallTime() {
-  return durationToDouble(getWallTimeVal().time_since_epoch());
+std::uint64_t time::Span::toMicroseconds() const {
+  return (std::uint64_t)std::chrono::duration_cast<std::chrono::microseconds>(duration).count();
 }
 
-sys::TimePoint<> util::getWallTimeVal() {
-  return std::chrono::system_clock::now();
+double time::Span::toSeconds() const {
+  return std::chrono::duration_cast<std::chrono::nanoseconds>(duration).count() / (double)1000000000;
 }
 
-#else
-double util::getUserTime() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  return (user.seconds() + (double) user.nanoseconds() * 1e-9);
+std::tuple<std::uint32_t, std::uint8_t, std::uint8_t> time::Span::toHMS() const {
+  auto d = duration;
+  const auto h = std::chrono::duration_cast<std::chrono::hours>(d);
+  const auto m = std::chrono::duration_cast<std::chrono::minutes>(d -= h);
+  const auto s = std::chrono::duration_cast<std::chrono::seconds>(d -= m);
+
+  return std::make_tuple((std::uint32_t) h.count(), (std::uint8_t) m.count(), (std::uint8_t) s.count());
 }
 
-double util::getWallTime() {
-  sys::TimeValue now = getWallTimeVal();
-  return (now.seconds() + ((double) now.nanoseconds() * 1e-9));
+
+// methods
+/// Returns information about clock
+std::string time::getClockInfo() {
+  std::stringstream buffer;
+  buffer << "Using monotonic steady clock with "
+         << std::chrono::steady_clock::period::num
+         << '/'
+         << std::chrono::steady_clock::period::den
+         << "s resolution\n";
+  return buffer.str();
 }
 
-sys::TimeValue util::getWallTimeVal() {
-  return sys::TimeValue::now();
+
+/// Returns time spent by this process in user mode
+time::Span time::getUserTime() {
+  rusage usage{};
+  auto ret = ::getrusage(RUSAGE_SELF, &usage);
+
+  if (ret) {
+    klee_warning("getrusage returned with error, return (0,0)");
+    return {};
+  } else {
+    return time::seconds(static_cast<std::uint64_t>(usage.ru_utime.tv_sec)) +
+           time::microseconds(static_cast<std::uint64_t>(usage.ru_utime.tv_usec));
+  }
 }
-#endif
+
+
+/// Returns point in time using a monotonic steady clock
+time::Point time::getWallTime() {
+  return time::Point(std::chrono::steady_clock::now());
+}
+
diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp
index 0e727bb4..4e52feb5 100644
--- a/lib/Support/Timer.cpp
+++ b/lib/Support/Timer.cpp
@@ -9,32 +9,14 @@
 
 #include "klee/Config/Version.h"
 #include "klee/Internal/Support/Timer.h"
-
 #include "klee/Internal/System/Time.h"
 
 using namespace klee;
-using namespace llvm;
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
 
 WallTimer::WallTimer() {
-  start = util::getWallTimeVal();
+  start = time::getWallTime();
 }
 
-uint64_t WallTimer::check() {
-  auto now = util::getWallTimeVal();
-  return std::chrono::duration_cast<std::chrono::microseconds>(now -
-    start).count();
+time::Span WallTimer::check() {
+  return time::Span(time::getWallTime() - start);
 }
-
-#else
-
-WallTimer::WallTimer() {
-  startMicroseconds = util::getWallTimeVal().usec();
-}
-
-uint64_t WallTimer::check() {
-  return util::getWallTimeVal().usec() - startMicroseconds;
-}
-
-#endif
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 3ce414a2..3ac13adb 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -216,8 +216,9 @@ static bool EvaluateInputAST(const char *Filename,
   Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
 
   if (CoreSolverToUse != DUMMY_SOLVER) {
-    if (0 != MaxCoreSolverTime) {
-      coreSolver->setCoreSolverTimeout(MaxCoreSolverTime);
+    const time::Span maxCoreSolverTime(MaxCoreSolverTime);
+    if (maxCoreSolverTime) {
+      coreSolver->setCoreSolverTimeout(maxCoreSolverTime);
     }
   }
 
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 0cbeaa96..50848bad 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -58,6 +58,7 @@
 #include <sys/wait.h>
 
 #include <cerrno>
+#include <ctime>
 #include <fstream>
 #include <iomanip>
 #include <iterator>
@@ -213,7 +214,7 @@ namespace {
            cl::init(0));
 }
 
-extern cl::opt<double> MaxTime;
+extern cl::opt<std::string> MaxTime;
 
 /***/
 
@@ -409,7 +410,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
     if (!success)
       klee_warning("unable to get symbolic solution, losing test case");
 
-    double start_time = util::getWallTime();
+    const auto start_time = time::getWallTime();
 
     unsigned id = ++m_numTotalTests;
 
@@ -515,10 +516,10 @@ void KleeHandler::processTestCase(const ExecutionState &state,
       m_interpreter->setHaltExecution(true);
 
     if (WriteTestInfo) {
-      double elapsed_time = util::getWallTime() - start_time;
+      time::Span elapsed_time(time::getWallTime() - start_time);
       auto f = openTestFile("info", id);
       if (f)
-        *f << "Time to generate test case: " << elapsed_time << "s\n";
+        *f << "Time to generate test case: " << elapsed_time << '\n';
     }
   }
 
@@ -940,21 +941,6 @@ static void halt_via_gdb(int pid) {
     perror("system");
 }
 
-// returns the end of the string put in buf
-static char *format_tdiff(char *buf, long seconds)
-{
-  assert(seconds >= 0);
-
-  long minutes = seconds / 60;  seconds %= 60;
-  long hours   = minutes / 60;  minutes %= 60;
-  long days    = hours   / 24;  hours   %= 24;
-
-  buf = strrchr(buf, '\0');
-  if (days > 0) buf += sprintf(buf, "%ld days, ", days);
-  buf += sprintf(buf, "%02ld:%02ld:%02ld", hours, minutes, seconds);
-  return buf;
-}
-
 #ifndef SUPPORT_KLEE_UCLIBC
 static void
 linkWithUclibc(StringRef libDir,
@@ -1080,7 +1066,7 @@ int main(int argc, char **argv, char **envp) {
 #endif
 
   if (Watchdog) {
-    if (MaxTime==0) {
+    if (MaxTime.empty()) {
       klee_error("--watchdog used without --max-time");
     }
 
@@ -1092,7 +1078,8 @@ int main(int argc, char **argv, char **envp) {
       fflush(stderr);
       sys::SetInterruptFunction(interrupt_handle_watchdog);
 
-      double nextStep = util::getWallTime() + MaxTime*1.1;
+      const time::Span maxTime(MaxTime);
+      auto nextStep = time::getWallTime() + maxTime + (maxTime / 10);
       int level = 0;
 
       // Simple stupid code...
@@ -1114,7 +1101,7 @@ int main(int argc, char **argv, char **envp) {
         } else if (res==pid && WIFEXITED(status)) {
           return WEXITSTATUS(status);
         } else {
-          double time = util::getWallTime();
+          auto time = time::getWallTime();
 
           if (time > nextStep) {
             ++level;
@@ -1136,7 +1123,8 @@ int main(int argc, char **argv, char **envp) {
 
             // Ideally this triggers a dump, which may take a while,
             // so try and give the process extra time to clean up.
-            nextStep = util::getWallTime() + std::max(15., MaxTime*.1);
+            auto max = std::max(time::seconds(15), maxTime / 10);
+            nextStep = time::getWallTime() + max;
           }
         }
       }
@@ -1293,12 +1281,16 @@ int main(int argc, char **argv, char **envp) {
     interpreter->setReplayPath(&replayPath);
   }
 
-  char buf[256];
-  time_t t[2];
-  t[0] = time(NULL);
-  strftime(buf, sizeof(buf), "Started: %Y-%m-%d %H:%M:%S\n", localtime(&t[0]));
-  handler->getInfoStream() << buf;
-  handler->getInfoStream().flush();
+
+  auto startTime = std::time(nullptr);
+  { // output clock info and start time
+    std::stringstream startInfo;
+    startInfo << time::getClockInfo()
+              << "Started: "
+              << std::put_time(std::localtime(&startTime), "%Y-%m-%d %H:%M:%S") << '\n';
+    handler->getInfoStream() << startInfo.str();
+    handler->getInfoStream().flush();
+  }
 
   if (!ReplayKTestDir.empty() || !ReplayKTestFile.empty()) {
     assert(SeedOutFile.empty());
@@ -1396,13 +1388,24 @@ int main(int argc, char **argv, char **envp) {
     }
   }
 
-  t[1] = time(NULL);
-  strftime(buf, sizeof(buf), "Finished: %Y-%m-%d %H:%M:%S\n", localtime(&t[1]));
-  handler->getInfoStream() << buf;
-
-  strcpy(buf, "Elapsed: ");
-  strcpy(format_tdiff(buf, t[1] - t[0]), "\n");
-  handler->getInfoStream() << buf;
+  auto endTime = std::time(nullptr);
+  { // output end and elapsed time
+    std::uint32_t h;
+    std::uint8_t m, s;
+    std::tie(h,m,s) = time::seconds(endTime - startTime).toHMS();
+    std::stringstream endInfo;
+    endInfo << "Finished: "
+            << std::put_time(std::localtime(&endTime), "%Y-%m-%d %H:%M:%S") << '\n'
+            << "Elapsed: "
+            << std::setfill('0') << std::setw(2) << h
+            << ':'
+            << std::setfill('0') << std::setw(2) << +m
+            << ':'
+            << std::setfill('0') << std::setw(2) << +s
+            << '\n';
+            handler->getInfoStream() << endInfo.str();
+    handler->getInfoStream().flush();
+  }
 
   // Free all the args.
   for (unsigned i=0; i<InputArgv.size()+1; i++)
diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt
index 00d4cbfa..d6e58183 100644
--- a/unittests/CMakeLists.txt
+++ b/unittests/CMakeLists.txt
@@ -86,6 +86,7 @@ add_subdirectory(Ref)
 add_subdirectory(Solver)
 add_subdirectory(TreeStream)
 add_subdirectory(DiscretePDF)
+add_subdirectory(Time)
 
 # Set up lit configuration
 set (UNIT_TEST_EXE_SUFFIX "Test")
diff --git a/unittests/Time/CMakeLists.txt b/unittests/Time/CMakeLists.txt
new file mode 100644
index 00000000..6a860582
--- /dev/null
+++ b/unittests/Time/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_klee_unit_test(TimeTest
+  TimeTest.cpp)
+target_link_libraries(TimeTest PRIVATE kleeSupport)
diff --git a/unittests/Time/TimeTest.cpp b/unittests/Time/TimeTest.cpp
new file mode 100644
index 00000000..9caa14fd
--- /dev/null
+++ b/unittests/Time/TimeTest.cpp
@@ -0,0 +1,165 @@
+#include "klee/Internal/System/Time.h"
+#include "gtest/gtest.h"
+#include "gtest/gtest-death-test.h"
+
+#include <cerrno>
+#include <sstream>
+
+
+int finished = 0;
+
+using namespace klee;
+
+
+TEST(TimeTest, TimingFunctions) {
+  auto t = time::getClockInfo();
+  ASSERT_STRNE(t.c_str(), "");
+
+  auto p0 = time::getWallTime();
+  auto p1 = time::getWallTime();
+  ASSERT_GT(p0, time::Point());
+  ASSERT_GT(p1, time::Point());
+  ASSERT_LE(p0, p1);
+
+  time::getUserTime();
+}
+
+
+TEST(TimeTest, TimeParserNewFormat) {
+  // valid
+  errno = 0;
+  auto s0 = time::Span("");
+  ASSERT_EQ(s0, time::Span());
+  ASSERT_EQ(errno, 0);
+
+  s0 = time::Span("3h10min");
+  ASSERT_EQ(s0, time::minutes(190));
+  s0 = time::Span("5min5min");
+  ASSERT_EQ(s0, time::seconds(600));
+  s0 = time::Span("3us");
+  ASSERT_EQ(s0, time::microseconds(3));
+  s0 = time::Span("1h1min1s1ms1us1ns");
+  ASSERT_EQ(s0, time::nanoseconds(3661001001001));
+  s0 = time::Span("1min1min");
+  ASSERT_EQ(s0, time::minutes(2));
+
+  // invalid
+  ASSERT_EXIT(time::Span("h"), ::testing::ExitedWithCode(1), "Illegal number format: h");
+  ASSERT_EXIT(time::Span("-5min"), ::testing::ExitedWithCode(1), "Illegal number format: -5min");
+  ASSERT_EXIT(time::Span("3.5h"), ::testing::ExitedWithCode(1), "Illegal number format: 3.5h");
+  ASSERT_EXIT(time::Span("3mi"), ::testing::ExitedWithCode(1), "Illegal number format: 3mi");
+}
+
+
+TEST(TimeTest, TimeParserOldFormat) {
+  // valid
+  errno = 0;
+
+  auto s0 = time::Span("20");
+  ASSERT_EQ(s0, time::seconds(20));
+  s0 = time::Span("3.5");
+  ASSERT_EQ(s0, time::milliseconds(3500));
+  s0 = time::Span("0.0");
+  ASSERT_EQ(s0, time::Span());
+  s0 = time::Span("0");
+  ASSERT_EQ(s0, time::Span());
+
+  ASSERT_EQ(errno, 0);
+
+  // invalid
+  ASSERT_EXIT(time::Span("-3.5"), ::testing::ExitedWithCode(1), "Illegal number format: -3.5");
+  ASSERT_EXIT(time::Span("NAN"), ::testing::ExitedWithCode(1), "Illegal number format: NAN");
+  ASSERT_EXIT(time::Span("INF"), ::testing::ExitedWithCode(1), "Illegal number format: INF");
+  ASSERT_EXIT(time::Span("foo"), ::testing::ExitedWithCode(1), "Illegal number format: foo");
+}
+
+
+TEST(TimeTest, TimeArithmeticAndComparisons) {
+  auto h   = time::hours(1);
+  auto min = time::minutes(1);
+  auto sec = time::seconds(1);
+  auto ms  = time::milliseconds(1);
+  auto us  = time::microseconds(1);
+  auto ns  = time::nanoseconds(1);
+
+  ASSERT_GT(h, min);
+  ASSERT_GT(min, sec);
+  ASSERT_GT(sec, ms);
+  ASSERT_GT(ms, us);
+  ASSERT_GT(us, ns);
+
+  ASSERT_LT(min, h);
+  ASSERT_LT(sec, min);
+  ASSERT_LT(ms, sec);
+  ASSERT_LT(us, ms);
+  ASSERT_LT(ns, us);
+
+  ASSERT_GE(h, min);
+  ASSERT_LE(min, h);
+
+  auto sec2 = time::seconds(1);
+  ASSERT_EQ(sec, sec2);
+  sec2 += time::nanoseconds(1);
+  ASSERT_LT(sec, sec2);
+
+  auto op0 = time::seconds(1);
+  auto op1 = op0 / 1000;
+  ASSERT_EQ(op1, ms);
+  op0 = time::nanoseconds(3);
+  op1 = op0 * 1000;
+  ASSERT_EQ(op1, 3*us);
+
+  op0 = (time::seconds(10) + time::minutes(1) - time::milliseconds(10000)) * 60;
+  ASSERT_EQ(op0, h);
+
+  auto p1 = time::getWallTime();
+  auto p2 = p1;
+  p1 += time::seconds(10);
+  p2 -= time::seconds(15);
+  ASSERT_EQ(p1 - p2, time::seconds(25));
+
+  auto s = time::minutes(3);
+  p1 = s + p2;
+  ASSERT_NE(p1, p2);
+  ASSERT_LT(p2, p1);
+  p1 = p1 - s;
+  ASSERT_EQ(p1, p2);
+
+  s = time::minutes(5);
+  s -= time::minutes(4);
+  ASSERT_EQ(s, time::seconds(60));
+}
+
+
+TEST(TimeTest, TimeConversions) {
+  auto t = time::Span("3h14min1s");
+  auto d = t.toSeconds();
+  ASSERT_EQ(d, 11641.0);
+
+  std::uint32_t h;
+  std::uint8_t m, s;
+  std::tie(h, m, s) = t.toHMS();
+  ASSERT_EQ(h, 3u);
+  ASSERT_EQ(m, 14u);
+  ASSERT_EQ(s, 1u);
+
+  ASSERT_TRUE((bool)t);
+  ASSERT_FALSE((bool)time::Span());
+
+  auto us = t.toMicroseconds();
+  ASSERT_EQ(us, 11641000000u);
+
+  t += time::microseconds(42);
+  auto v = (timeval)t;
+  ASSERT_EQ(v.tv_sec, 11641);
+  ASSERT_EQ(v.tv_usec, 42);
+
+  t = std::chrono::seconds(1);
+  ASSERT_EQ(t, time::seconds(1));
+  auto u = (std::chrono::steady_clock::duration)t;
+  ASSERT_EQ(u, std::chrono::seconds(1));
+
+  std::ostringstream os;
+  os << time::Span("2.5");
+  ASSERT_EQ(os.str(), "2.5s");
+}
-- 
cgit 1.4.1