diff options
Diffstat (limited to 'src/util/statistics_registry.h')
-rw-r--r-- | src/util/statistics_registry.h | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index bd33557d9..8246bfdd2 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -824,6 +824,7 @@ public: */ class CodeTimer { TimerStat& d_timer; + bool d_reentrant; /** Private copy constructor undefined (no copy permitted). */ CodeTimer(const CodeTimer& timer) CVC4_UNDEFINED; @@ -831,11 +832,15 @@ class CodeTimer { CodeTimer& operator=(const CodeTimer& timer) CVC4_UNDEFINED; public: - CodeTimer(TimerStat& timer) : d_timer(timer) { - d_timer.start(); + CodeTimer(TimerStat& timer, bool allow_reentrant = false) : d_timer(timer), d_reentrant(false) { + if(!allow_reentrant || !(d_reentrant = d_timer.running())) { + d_timer.start(); + } } ~CodeTimer() { - d_timer.stop(); + if(!d_reentrant) { + d_timer.stop(); + } } };/* class CodeTimer */ |