summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
authorPaulMeng <baolmeng@gmail.com>2016-08-24 11:24:57 -0400
committerPaulMeng <baolmeng@gmail.com>2016-08-24 11:24:57 -0400
commitdc3f45d6e41bdd4e52e39b0c6fecae3148a2944c (patch)
tree7516d3d5d43f0dadb943bb186615e0903cbd9f7f /src/expr
parent74bf9ff63f5566fbe1b5db9124f9dc1fde65cb82 (diff)
parent6b355496aaf27d46d6a33402814753589b755842 (diff)
Merge remote-tracking branch 'origin/master'
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/expr_manager_template.cpp6
-rw-r--r--src/expr/expr_manager_template.h2
2 files changed, 4 insertions, 4 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 53e16751e..2dc3aebe5 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -75,7 +75,7 @@ ExprManager::ExprManager() :
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
d_exprStatistics[i] = NULL;
}
- for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+ for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
d_exprStatisticsVars[i] = NULL;
}
#endif
@@ -84,7 +84,7 @@ ExprManager::ExprManager() :
ExprManager::ExprManager(const Options& options) :
d_nodeManager(new NodeManager(this, options)) {
#ifdef CVC4_STATISTICS_ON
- for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+ for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
d_exprStatisticsVars[i] = NULL;
}
for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
@@ -106,7 +106,7 @@ ExprManager::~ExprManager() throw() {
d_exprStatistics[i] = NULL;
}
}
- for (unsigned i = 0; i < LAST_TYPE; ++ i) {
+ for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
if (d_exprStatisticsVars[i] != NULL) {
d_nodeManager->getStatisticsRegistry()->unregisterStat(d_exprStatisticsVars[i]);
delete d_exprStatisticsVars[i];
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 31c911736..f30b720de 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -57,7 +57,7 @@ private:
NodeManager* d_nodeManager;
/** Counts of expressions and variables created of a given kind */
- IntStat* d_exprStatisticsVars[LAST_TYPE];
+ IntStat* d_exprStatisticsVars[LAST_TYPE + 1];
IntStat* d_exprStatistics[kind::LAST_KIND];
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback