diff options
Diffstat (limited to 'test/unit/util/stats_black.h')
-rw-r--r-- | test/unit/util/stats_black.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index e44a016e6..d32ef828c 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -30,7 +30,7 @@ class StatsBlack : public CxxTest::TestSuite { public: void testStats() { - +#ifdef CVC4_STATISTICS_ON // StatisticsRegistry //static void flushStatistics(std::ostream& out); @@ -99,6 +99,7 @@ public: TS_ASSERT_EQUALS(zero, sTimer.getData()); sTimer.stop(); TS_ASSERT_LESS_THAN(zero, sTimer.getData()); +#endif /* CVC4_STATISTICS_ON */ } }; |