Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).

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 */