From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 4 Sep 2019 18:13:18 +0000 (-0700)
Subject: Fix DAGification for printer. (#3233)
X-Git-Tag: cvc5-1.0.0~3981
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=599e788f249e478b5817b6cf45584d8e43458df4;p=cvc5.git

Fix DAGification for printer. (#3233)
---

diff --git a/src/printer/dagification_visitor.cpp b/src/printer/dagification_visitor.cpp
index a024c97a7..67c5aa7e5 100644
--- 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();
     }