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

1 files changed, 22 insertions, 0 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) {