From 410eb892bd779a7544cace62fa2b447b8188e238 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 4 May 2018 11:46:31 -0500
Subject: [PATCH] Do not print tuples. (#1874)

---
 src/printer/smt2/smt2_printer.cpp | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 5d2b8972d..96bee9724 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1441,10 +1441,7 @@ void Smt2Printer::toStream(std::ostream& out,
   else if (const DatatypeDeclarationCommand* datatype_declaration_command =
                dynamic_cast<const DatatypeDeclarationCommand*>(command))
   {
-    if (!datatype_declaration_command->getDatatypes()[0].isTuple())
-    {
-      out << command << endl;
-    }
+    toStream(out, datatype_declaration_command, -1, false, 1);
   }
   else
   {
@@ -1903,8 +1900,14 @@ static void toStream(std::ostream& out,
                      Variant v)
 {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
-  out << "(declare-";
   Assert(!datatypes.empty());
+  if (datatypes[0].getDatatype().isTuple())
+  {
+    // not necessary to print tuples
+    Assert(datatypes.size() == 1);
+    return;
+  }
+  out << "(declare-";
   if (datatypes[0].getDatatype().isCodatatype())
   {
     out << "co";
-- 
2.30.2