fix memory corruption issue in debug builds that led to unhelpful output

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index e580b6348aa13b41e0206fc481eb1bbfcb818a23..845ebe8a576babaa343bc0e39cc4d04ca1e228c9 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -18,6 +18,7 @@
 #include "util/output.h"
 
 #include <iostream>
+#include <cstring>
 
 using namespace std;
 
@@ -28,7 +29,8 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
   Exception(message),
   d_node(new Node(node)) {
 #ifdef CVC4_DEBUG
-  s_debugLastException = toString().c_str();
+  // yes, this leaks memory, but only in debug modes with exceptions occurring
+  s_debugLastException = strdup(toString().c_str());
 #endif /* CVC4_DEBUG */
 }