1 files changed, 2 insertions, 2 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index b14f6a9c8..35a85e681 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -991,13 +991,13 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
           }
           firstSelector = false;
           const DatatypeConstructorArg& selector = *k;
-          out << selector.getName() << ": " << selector.getType();
+          out << selector.getName() << ": " << SelectorType(selector.getType()).getRangeType();
         }
         out << ')';
       }
     }
   }
-  out << endl << "END;" << endl;
+  out << endl << "END;";
 }
 
 static void toStream(std::ostream& out, const CommentCommand* c) throw() {