summaryrefslogtreecommitdiff
path: root/src/printer
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2012-08-06 19:35:39 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2012-08-06 19:35:39 +0000
commitd847992670fb6b868521a80ae83f02e6c0722288 (patch)
tree810df7c414ea6f6bb32b5531640765a729f77811 /src/printer
parent92a39d3b7bbf3f1617ad7e1ec87f4a36070c1968 (diff)
fix constant printing for datatypes
Diffstat (limited to 'src/printer')
-rw-r--r--src/printer/cvc/cvc_printer.cpp2
1 files changed, 1 insertions, 1 deletions
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 << ")";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback