From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 28 Sep 2012 18:22:29 +0000 (+0000)
Subject: fix production-build linking error
X-Git-Tag: cvc5-1.0.0~7771
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a3a0b0a60fd29d67f013b2150ba47d401a3e39c;p=cvc5.git

fix production-build linking error
---

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 */