diff options
Diffstat (limited to 'src/util/stats.cpp')
| -rw-r--r-- | src/util/stats.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/util/stats.cpp b/src/util/stats.cpp index 709f80b04..b030495c5 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -46,8 +46,7 @@ void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::registerStat() */ -void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) -{ +void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); d_registeredStats.insert(s); |