diff options
-rw-r--r-- | src/expr/node.cpp | 13 |
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 */ } |