From 69f9580ef8bb66e786bc9fada2c094c5f6f16f6a Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Tue, 7 Feb 2012 16:14:17 +0000
Subject: [PATCH] fixing some missing stuff

---
 src/printer/cvc/cvc_printer.cpp | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 1bcb4892b..26616259c 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -130,7 +130,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       }
       break;
     default:
-      Unreachable();
+      Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl;
+      out << n.getKind();
       break;
     }
     return;
@@ -177,7 +178,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     case kind::APPLY:
       toStream(op, n.getOperator(), depth, types, true);
       break;
-
+    case kind::SORT_TYPE:
+    {
+      string name;
+      if(n.getAttribute(expr::VarNameAttr(), name)) {
+        out << name;
+        return;
+      }
+    }
+    break;
     // BOOL
     case kind::AND:
       op << "AND";
@@ -470,7 +479,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       return;
       break;
     default:
-      Unreachable();
+      Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl;
       break;
   }
 
-- 
2.30.2