From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 13:47:50 +0000 (+0000)
Subject: fix memory corruption issue in debug builds that led to unhelpful output
X-Git-Tag: cvc5-1.0.0~7492
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=265765c9f5c35c4b65934e574dbfabab97b15f7a;p=cvc5.git

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 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 */
 }