diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-12-01 13:47:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-12-01 13:47:50 +0000 |
commit | 265765c9f5c35c4b65934e574dbfabab97b15f7a (patch) | |
tree | cfbd7583bc0a17ce66d9e182d370c057ef8d5bf2 /src/expr/node.cpp | |
parent | 557d4c2d3dd0f9f0210b9438c952903635248357 (diff) |
fix memory corruption issue in debug builds that led to unhelpful output
Diffstat (limited to 'src/expr/node.cpp')
-rw-r--r-- | src/expr/node.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/expr/node.cpp b/src/expr/node.cpp index e580b6348..845ebe8a5 100644 --- 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 */ } |