From 7de5f26ca35f6b3b11dc8a7465f7a15e5d0d2e50 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 19 Jul 2019 12:39:07 -0400
Subject: Fixes for sygus with datatypes (#3103)

---
 src/printer/smt2/smt2_printer.cpp | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

(limited to 'src/printer')

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9b34b1d7c..163c8acad 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1476,18 +1476,15 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
       return;
     }
   }
+  Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
+  if (!p.isNull())
+  {
+    out << p;
+  }
   else
   {
-    Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
-    if (!p.isNull())
-    {
-      out << p;
-    }
-    else
-    {
-      // cannot convert term to analog, print original
-      out << n;
-    }
+    // cannot convert term to analog, print original
+    out << n;
   }
 }
 
-- 
cgit v1.2.3