Fix timer statistics to report correct time even on process abort.

3 files changed, 30 insertions, 10 deletions

diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index f6a27e20d..67cc3a53c 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -119,6 +119,28 @@ void TimerStat::stop() {
   }
 }/* TimerStat::stop() */
 
+timespec TimerStat::getData() const {
+  ::timespec data = d_data;
+  if(__CVC4_USE_STATISTICS && d_running) {
+    ::timespec end;
+    clock_gettime(CLOCK_MONOTONIC, &end);
+    data += end - d_start;
+  }
+  return data;
+}
+
+SExpr TimerStat::getValue() const {
+  ::timespec data = d_data;
+  if(__CVC4_USE_STATISTICS && d_running) {
+    ::timespec end;
+    clock_gettime(CLOCK_MONOTONIC, &end);
+    data += end - d_start;
+  }
+  std::stringstream ss;
+  ss << std::fixed << std::setprecision(8) << data;
+  return SExpr(Rational::fromDecimal(ss.str()));
+}/* TimerStat::getValue() */
+
 RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) :
   d_reg(stats::getStatisticsRegistry(&em)),
   d_stat(stat) {
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index 8ffc60d17..eb5245e25 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -179,7 +179,7 @@ public:
   }
 
   /** Get the value of the statistic. */
-  virtual const T& getData() const = 0;
+  virtual T getData() const = 0;
 
   /** Flush the value of the statistic to the given output stream. */
   void flushInformation(std::ostream& out) const {
@@ -270,7 +270,7 @@ public:
   }
 
   /** Get the value of the referenced data cell. */
-  const T& getData() const {
+  T getData() const {
     return *d_data;
   }
 
@@ -312,7 +312,7 @@ public:
   }
 
   /** Get the underlying data value. */
-  const T& getData() const {
+  T getData() const {
     return d_data;
   }
 
@@ -354,7 +354,7 @@ public:
   }
 
   /** Get the data of the underlying (wrapped) statistic. */
-  const T& getData() const {
+  T getData() const {
     return d_stat.getData();
   }
 
@@ -808,11 +808,9 @@ public:
    */
   void stop();
 
-  SExpr getValue() const {
-    std::stringstream ss;
-    ss << std::fixed << std::setprecision(8) << d_data;
-    return SExpr(Rational::fromDecimal(ss.str()));
-  }
+  timespec getData() const;
+
+  SExpr getValue() const;
 
 };/* class TimerStat */
 
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h
index 3e3f6b942..1367a62c1 100644
--- a/test/unit/util/stats_black.h
+++ b/test/unit/util/stats_black.h
@@ -94,7 +94,7 @@ public:
 
     sTimer.start();
     timespec zero = { 0, 0 };
-    TS_ASSERT_EQUALS(zero, sTimer.getData());
+    //TS_ASSERT_EQUALS(zero, sTimer.getData());
     sTimer.stop();
     TS_ASSERT_LESS_THAN(zero, sTimer.getData());
 #endif /* CVC4_STATISTICS_ON */