diff options
Diffstat (limited to 'src/base/cvc4_assert.cpp')
| -rw-r--r-- | src/base/cvc4_assert.cpp | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp index 6e51845dd..efc71c986 100644 --- a/src/base/cvc4_assert.cpp +++ b/src/base/cvc4_assert.cpp @@ -26,9 +26,10 @@ using namespace std; namespace CVC4 { #ifdef CVC4_DEBUG -CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; +//CVC4_THREADLOCAL(const char*) s_debugLastException = NULL; #endif /* CVC4_DEBUG */ + void AssertionException::construct(const char* header, const char* extra, const char* function, const char* file, unsigned line, const char* fmt, @@ -71,13 +72,14 @@ void AssertionException::construct(const char* header, const char* extra, setMessage(string(buf)); #ifdef CVC4_DEBUG - if(s_debugLastException == NULL) { - // we leak buf[] but only in debug mode with assertions failing - s_debugLastException = buf; + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if(buffer != NULL){ + if(buffer->getContents() == NULL) { + buffer->setContents(buf); + } } -#else /* CVC4_DEBUG */ - delete [] buf; #endif /* CVC4_DEBUG */ + delete [] buf; } void AssertionException::construct(const char* header, const char* extra, @@ -111,14 +113,16 @@ void AssertionException::construct(const char* header, const char* extra, setMessage(string(buf)); + #ifdef CVC4_DEBUG - // we leak buf[] but only in debug mode with assertions failing - if(s_debugLastException == NULL) { - s_debugLastException = buf; + LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); + if(buffer != NULL){ + if(buffer->getContents() == NULL) { + buffer->setContents(buf); + } } -#else /* CVC4_DEBUG */ - delete [] buf; #endif /* CVC4_DEBUG */ + delete [] buf; } #ifdef CVC4_DEBUG |