From ab8e5a034964c45796168e4e140e31d33a51932b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 2 Sep 2010 08:16:28 +0000 Subject: [PATCH] fix an error in TimerStat --- src/util/stats.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/stats.h b/src/util/stats.h index 74afb5792..a005c7689 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -326,6 +326,7 @@ public: if(__CVC4_USE_STATISTICS) { AlwaysAssert(!d_running); clock_gettime(CLOCK_REALTIME, &d_start); + d_running = true; } } @@ -335,6 +336,7 @@ public: ::timespec end; clock_gettime(CLOCK_REALTIME, &end); d_data += end - d_start; + d_running = false; } } };/* class TimerStat */ -- 2.30.2