diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 18:22:29 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 18:22:29 +0000 |
| commit | 6a3a0b0a60fd29d67f013b2150ba47d401a3e39c (patch) | |
| tree | 774ed20cd0c6746763f860648b49e03124c71206 /src/util/statistics_registry.h | |
| parent | 65f720aac2d497c6e829d9c76638073a10060e7d (diff) | |
fix production-build linking error
Diffstat (limited to 'src/util/statistics_registry.h')
| -rw-r--r-- | src/util/statistics_registry.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 99168353f..c51e77ff5 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -24,6 +24,7 @@ #define __CVC4__STATISTICS_REGISTRY_H #include "util/statistics.h" +#include "util/exception.h" #include <sstream> #include <iomanip> @@ -838,7 +839,9 @@ public: RegisterStatistic(Stat* stat) : d_reg(StatisticsRegistry::current()), d_stat(stat) { - Assert(d_reg != NULL, "There is no current statistics registry!"); + if(d_reg != NULL) { + throw CVC4::Exception("There is no current statistics registry!"); + } StatisticsRegistry::registerStat(d_stat); } #endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ |