summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/expr/node.cpp13
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 */
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback