diff options
| -rw-r--r-- | src/util/stats.h | 2 |
1 files changed, 2 insertions, 0 deletions
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 */ |