From 542156e0f589dfe89ca7fb5736b44b05cb653ab6 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 22 Jun 2014 00:32:33 -0400
Subject: Minor cleanup stuff.

---
 src/printer/cvc/cvc_printer.cpp | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/printer/cvc')

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 77d8f14de..16f5f5c51 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -661,6 +661,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << n.getOperator().getConst<BitVectorExtract>();
       opType = POSTFIX;
       break;
+    case kind::BITVECTOR_BITOF:
+      op << n.getOperator().getConst<BitVectorBitOf>();
+      opType = POSTFIX;
+      break;
     case kind::BITVECTOR_REPEAT:
       out << "BVREPEAT(";
       toStream(out, n[0], depth, types, false);
-- 
cgit v1.2.3