From: François Bobot <francois@bobot.eu>
Date: Fri, 4 May 2012 14:28:00 +0000 (+0000)
Subject: fix: getNumTraceTags, getNumDebugTags
X-Git-Tag: cvc5-1.0.0~8203
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=66c8c03e12d42d4b6095a05229567b83e6f175e1;p=cvc5.git

fix: getNumTraceTags, getNumDebugTags
---

diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 8942c049b..9b4d32e0b 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -131,7 +131,8 @@ bool Configuration::isBuiltWithTlsSupport() {
 
 unsigned Configuration::getNumDebugTags() {
 #if CVC4_DEBUG
-  return sizeof(Debug_tags) / sizeof(Debug_tags[0]);
+  /* -1 because a NULL pointer is inserted as the last value */
+  return sizeof(Debug_tags) / sizeof(Debug_tags[0]) - 1;
 #else /* CVC4_DEBUG */
   return 0;
 #endif /* CVC4_DEBUG */
@@ -148,7 +149,8 @@ char const* const* Configuration::getDebugTags() {
 
 unsigned Configuration::getNumTraceTags() {
 #if CVC4_TRACING
-  return sizeof(Trace_tags) / sizeof(Trace_tags[0]);
+  /* -1 because a NULL pointer is inserted as the last value */
+  return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1;
 #else /* CVC4_TRACING */
   return 0;
 #endif /* CVC4_TRACING */