1 files changed, 48 insertions, 45 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 11cf7dd11..b7e1520b7 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1248,58 +1248,61 @@ static void toStream(std::ostream& out, const GetOptionCommand* c, bool cvc3Mode
 
 static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, bool cvc3Mode) throw() {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
-  out << "DATATYPE" << endl;
-  bool firstDatatype = true;
-  for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
-        i_end = datatypes.end();
-      i != i_end;
-      ++i) {
-    if(! firstDatatype) {
-      out << ',' << endl;
-    }
-    const Datatype& dt = (*i).getDatatype();
-    out << "  " << dt.getName();
-    if(dt.isParametric()) {
-      out << '[';
-      for(size_t j = 0; j < dt.getNumParameters(); ++j) {
-        if(j > 0) {
-          out << ',';
-        }
-        out << dt.getParameter(j);
+  //do not print tuple/datatype internal declarations
+  if( datatypes.size()!=1 || ( !datatypes[0].getDatatype().isTuple() && !datatypes[0].getDatatype().isRecord() ) ){
+    out << "DATATYPE" << endl;
+    bool firstDatatype = true;
+    for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
+          i_end = datatypes.end();
+        i != i_end;
+        ++i) {
+      if(! firstDatatype) {
+        out << ',' << endl;
       }
-      out << ']';
-    }
-    out << " = ";
-    bool firstConstructor = true;
-    for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
-      if(! firstConstructor) {
-        out << " | ";
-      }
-      firstConstructor = false;
-      const DatatypeConstructor& c = *j;
-      out << c.getName();
-      if(c.getNumArgs() > 0) {
-        out << '(';
-        bool firstSelector = true;
-        for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) {
-          if(! firstSelector) {
-            out << ", ";
+      const Datatype& dt = (*i).getDatatype();
+      out << "  " << dt.getName();
+      if(dt.isParametric()) {
+        out << '[';
+        for(size_t j = 0; j < dt.getNumParameters(); ++j) {
+          if(j > 0) {
+            out << ',';
           }
-          firstSelector = false;
-          const DatatypeConstructorArg& selector = *k;
-          Type t = SelectorType(selector.getType()).getRangeType();
-          if( t.isDatatype() ){
-            const Datatype & sdt = ((DatatypeType)t).getDatatype();
-            out << selector.getName() << ": " << sdt.getName();
-          }else{
-            out << selector.getName() << ": " << t;
+          out << dt.getParameter(j);
+        }
+        out << ']';
+      }
+      out << " = ";
+      bool firstConstructor = true;
+      for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
+        if(! firstConstructor) {
+          out << " | ";
+        }
+        firstConstructor = false;
+        const DatatypeConstructor& c = *j;
+        out << c.getName();
+        if(c.getNumArgs() > 0) {
+          out << '(';
+          bool firstSelector = true;
+          for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) {
+            if(! firstSelector) {
+              out << ", ";
+            }
+            firstSelector = false;
+            const DatatypeConstructorArg& selector = *k;
+            Type t = SelectorType(selector.getType()).getRangeType();
+            if( t.isDatatype() ){
+              const Datatype & sdt = ((DatatypeType)t).getDatatype();
+              out << selector.getName() << ": " << sdt.getName();
+            }else{
+              out << selector.getName() << ": " << t;
+            }
           }
+          out << ')';
         }
-        out << ')';
       }
     }
+    out << endl << "END;";
   }
-  out << endl << "END;";
 }
 
 static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode) throw() {