From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 6 Aug 2012 19:35:39 +0000 (+0000)
Subject: fix constant printing for datatypes
X-Git-Tag: cvc5-1.0.0~7887
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d847992670fb6b868521a80ae83f02e6c0722288;p=cvc5.git

fix constant printing for datatypes
---

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 << ")";