Do not call toString() on malformed node when throwing TypeCheckingExceptionPrivate. (#1733)

While throwing a TypeCheckingExceptionPrivate, an IllegalArgumentException was thrown when
trying calling toString() on a malformed node. Fixed by printing the kind of the node and its children
rather than calling toString() on the malformed node.

1 files changed, 12 insertions, 1 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 110925f41..b41014f9c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -31,9 +31,20 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
     : Exception(message), d_node(new Node(node))
 {
 #ifdef CVC4_DEBUG
+  std::stringstream ss;
   LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
   if(current != NULL){
-    current->setContents(toString().c_str());
+    // Since this node is malformed, we cannot use toString().
+    // Instead, we print the kind and the children.
+    ss << "node kind: " << node.getKind() << ". children: ";
+    int i = 0;
+    for (const TNode& child : node)
+    {
+      ss << "child[" << i << "]: " << child << ". ";
+      i++;
+    }
+    string ssstring = ss.str();
+    current->setContents(ssstring.c_str());
   }
 #endif /* CVC4_DEBUG */
 }