New, uniform checkTime statistic for all theories (as discussed in meeting).

1 files changed, 6 insertions, 2 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 867dd7c31..2dab434d1 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -197,7 +197,11 @@ private:
    */
   QuantifiersEngine* d_quantEngine;
 
+protected:
+
   // === STATISTICS ===
+  /** time spent in check calls */
+  TimerStat d_checkTime;
   /** time spent in theory combination */
   TimerStat d_computeCareGraphTime;
 
@@ -207,8 +211,6 @@ private:
     return ss.str();
   }
 
-protected:
-
   /**
    * The only method to add suff to the care graph.
    */
@@ -255,12 +257,14 @@ protected:
   , d_sharedTermsIndex(satContext, 0)
   , d_careGraph(NULL)
   , d_quantEngine(NULL)
+  , d_checkTime(statName(id, "checkTime"))
   , d_computeCareGraphTime(statName(id, "computeCareGraphTime"))
   , d_sharedTerms(satContext)
   , d_out(&out)
   , d_valuation(valuation)
   , d_proofEnabled(false)
   {
+    StatisticsRegistry::registerStat(&d_checkTime);
     StatisticsRegistry::registerStat(&d_computeCareGraphTime);
   }