diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-17 18:59:39 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-04 07:56:20 -0500 |
commit | ed87e0c1ccb0cb93cdedf5229c6a2b47af77743c (patch) | |
tree | b7c0efe878b82e6aff545b1d2fd52a02120f5813 /src/util/statistics_registry.h | |
parent | 08294c3914e4e87f3c5c1eda60e6ea259b789f55 (diff) |
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).
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 */ |