From: yoni206 <yoni206@users.noreply.github.com>
Date: Mon, 2 Apr 2018 18:40:48 +0000 (-0700)
Subject: Do not call toString() on malformed node when throwing TypeCheckingExceptionPrivate... 
X-Git-Tag: cvc5-1.0.0~5193
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d40d7ade3c66ba10a1f20ae5ab014aed8e2df01;p=cvc5.git

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.
---

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