diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-09-02 08:16:28 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-09-02 08:16:28 +0000 |
| commit | ab8e5a034964c45796168e4e140e31d33a51932b (patch) | |
| tree | 899dc042f2b9240c9074c78f1d3a6557a0b95822 | |
| parent | 3e27353891bfd54650a6385e99f1fd496df0b85f (diff) | |
fix an error in TimerStat
| -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 */ |