diff options
Diffstat (limited to 'src/util/configuration.cpp')
| -rw-r--r-- | src/util/configuration.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
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 */ |