From 6a3a0b0a60fd29d67f013b2150ba47d401a3e39c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 28 Sep 2012 18:22:29 +0000 Subject: [PATCH] fix production-build linking error --- src/util/statistics_registry.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 #include @@ -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 */ -- 2.30.2