From 265765c9f5c35c4b65934e574dbfabab97b15f7a Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 13:47:50 +0000
Subject: [PATCH] fix memory corruption issue in debug builds that led to
 unhelpful output

---
 src/expr/node.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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