Fix nullary operator printers, minor.

1 files changed, 9 insertions, 2 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 7b0ccdb8a..6b42d4e74 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -90,8 +90,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     string s;
     if(n.getAttribute(expr::VarNameAttr(), s)) {
       out << s;
-    }else if( n.getKind() == kind::UNIVERSE_SET ){
-      out << "UNIVERSE :: " << n.getType();
     } else {
       if(n.getKind() == kind::VARIABLE) {
         out << "var_";
@@ -107,6 +105,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     }
     return;
   }
+  if(n.isNullaryOp()) {
+    if( n.getKind() == kind::UNIVERSE_SET ){
+      out << "UNIVERSE :: " << n.getType();
+    }else{
+      //unknown printer
+      out << n.getKind();
+    }
+    return;
+  }
 
   // constants
   if(n.getMetaKind() == kind::metakind::CONSTANT) {