Do not call toString() on malformed node when throwing TypeCheckingExceptionPrivate...
authoryoni206 <yoni206@users.noreply.github.com>
Mon, 2 Apr 2018 18:40:48 +0000 (11:40 -0700)
committerAina Niemetz <aina.niemetz@gmail.com>
Mon, 2 Apr 2018 18:40:48 +0000 (11:40 -0700)
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.

src/expr/node.cpp

index 110925f416226e880085a7006b598bc295241b03..b41014f9c50d93a0b15acd687dba2312ca78d449 100644 (file)
@@ -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 */
 }