6 files changed, 48 insertions, 15 deletions
diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
index 9c021ddc..f989e929 100644
--- a/include/klee/Internal/System/Time.h
+++ b/include/klee/Internal/System/Time.h
@@ -76,7 +76,8 @@ namespace klee {
       Span& operator=(const Duration&);
       Span& operator+=(const Span&);
       Span& operator-=(const Span&);
-      Span& operator*=(const Duration::rep&);
+      Span& operator*=(unsigned);
+      Span& operator*=(double);
 
       // conversions
       explicit operator Duration() const;
@@ -90,9 +91,11 @@ namespace klee {
 
     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&);
+    Span operator*(const Span&, double);
+    Span operator*(double, const Span&);
+    Span operator*(const Span&, unsigned);
+    Span operator*(unsigned, const Span&);
+    Span operator/(const Span&, unsigned);
     bool operator==(const Span&, const Span&);
     bool operator<=(const Span&, const Span&);
     bool operator>=(const Span&, const Span&);
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 95bddf8c..488ffa34 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -889,7 +889,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
 
   time::Span timeout = coreSolverTimeout;
   if (isSeeding)
-    timeout *= it->second.size();
+    timeout *= static_cast<unsigned>(it->second.size());
   solver->setTimeout(timeout);
   bool success = solver->evaluate(current, condition, res);
   solver->setTimeout(time::Span());
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index de24d75d..9d2e8868 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -169,7 +169,7 @@ void Executor::processTimers(ExecutionState *current,
     if (maxInstTime && current &&
         std::find(removedStates.begin(), removedStates.end(), current) ==
             removedStates.end()) {
-      if (timerTicks*kMilliSecondsPerTick > maxInstTime) {
+      if (timerTicks * kMilliSecondsPerTick > maxInstTime) {
         klee_warning("max-instruction-time exceeded: %.2fs", (timerTicks * kMilliSecondsPerTick).toSeconds());
         terminateStateEarly(*current, "max-instruction-time exceeded");
       }
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index cce83d23..db295468 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -432,7 +432,7 @@ void IterativeDeepeningTimeSearcher::update(
   }
 
   if (baseSearcher->empty()) {
-    time *= 2;
+    time *= 2U;
     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 *>());
diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp
index 7cd9659b..219b07b0 100644
--- a/lib/Support/Time.cpp
+++ b/lib/Support/Time.cpp
@@ -106,13 +106,23 @@ error:
 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::Span::operator*=(unsigned factor) { duration *= factor; return *this; }
+time::Span& time::Span::operator*=(double factor) {
+  duration = std::chrono::microseconds((std::uint64_t)((double)toMicroseconds() * factor));
+  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); }
+time::Span time::operator*(const time::Span &span, double factor) {
+  return time::Span(std::chrono::microseconds((std::uint64_t)((double)span.toMicroseconds() * factor)));
+};
+time::Span time::operator*(double factor, const time::Span &span) {
+  return time::Span(std::chrono::microseconds((std::uint64_t)((double)span.toMicroseconds() * factor)));
+};
+time::Span time::operator*(const time::Span &span, unsigned factor) { return time::Span(span.duration * factor); }
+time::Span time::operator*(unsigned factor, const time::Span &span) { return time::Span(span.duration * factor); }
+time::Span time::operator/(const time::Span &span, unsigned divisor) { return time::Span(span.duration / divisor); }
 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; }
diff --git a/unittests/Time/TimeTest.cpp b/unittests/Time/TimeTest.cpp
index 9caa14fd..a05c41b4 100644
--- a/unittests/Time/TimeTest.cpp
+++ b/unittests/Time/TimeTest.cpp
@@ -103,13 +103,13 @@ TEST(TimeTest, TimeArithmeticAndComparisons) {
   ASSERT_LT(sec, sec2);
 
   auto op0 = time::seconds(1);
-  auto op1 = op0 / 1000;
+  auto op1 = op0 / 1000U;
   ASSERT_EQ(op1, ms);
   op0 = time::nanoseconds(3);
-  op1 = op0 * 1000;
-  ASSERT_EQ(op1, 3*us);
+  op1 = op0 * 1000U;
+  ASSERT_EQ(op1, 3U*us);
 
-  op0 = (time::seconds(10) + time::minutes(1) - time::milliseconds(10000)) * 60;
+  op0 = (time::seconds(10) + time::minutes(1) - time::milliseconds(10000)) * 60U;
   ASSERT_EQ(op0, h);
 
   auto p1 = time::getWallTime();
@@ -163,3 +163,23 @@ TEST(TimeTest, TimeConversions) {
   os << time::Span("2.5");
   ASSERT_EQ(os.str(), "2.5s");
 }
+
+TEST(TimeTest, ImplicitArithmeticConversions) {
+  auto t1 = time::Span("1000s");
+  t1 *= 2U;
+  auto d = t1.toSeconds();
+  ASSERT_EQ(d, 2000.0);
+
+  auto t2 = t1 * 1.5;
+  d = t2.toSeconds();
+  ASSERT_EQ(d, 3000.0);
+
+  t2 = 2.5 * t1;
+  d = t2.toSeconds();
+  ASSERT_EQ(d, 5000.0);
+
+  t1 = time::Span("1000s");
+  t1 *= 2.2;
+  d = t1.toSeconds();
+  ASSERT_EQ(d, 2200.0);
+}
\ No newline at end of file