From d847992670fb6b868521a80ae83f02e6c0722288 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Mon, 6 Aug 2012 19:35:39 +0000
Subject: [PATCH] fix constant printing for datatypes

---
 src/printer/cvc/cvc_printer.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 564769207..8121085d3 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -102,7 +102,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
   }
 
   // constants
-  if(n.isConst()) {
+  if(n.getMetaKind() == kind::metakind::CONSTANT) {
     switch(n.getKind()) {
     case kind::BITVECTOR_TYPE:
       out << "BITVECTOR(" << n.getConst<BitVectorSize>().size << ")";
-- 
2.30.2