Fix DAGification for printer. (#3233)

diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index a024c97a70b24ecd759ad0b7925081c4c90eb5db..67c5aa7e5f4b88f93ace0d24c772e680d8c95fc9 100644 (file)
--- a/src/printer/dagification_visitor.cpp
+++ b/src/printer/dagification_visitor.cpp
@@ -106,7 +106,12 @@ void DagificationVisitor::visit(TNode current, TNode parent) {
 
     TNode& uniqueParent = d_uniqueParent[current];
 
-    if(!uniqueParent.isNull() && uniqueParent != parent) {
+    // We restrict this optimization to nodes with arity 1 since otherwise we
+    // may run into issues with tree traverals. Without this restriction
+    // dumping regress3/pp-regfile increases the file size by a factor of 5000.
+    if (!uniqueParent.isNull()
+        && (uniqueParent != parent || parent.getNumChildren() > 1))
+    {
       // there is not a unique parent for this expr, mark it
       uniqueParent = TNode::null();
     }