summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r--src/printer/smt2/smt2_printer.cpp5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 04d8c34c4..ba03a4fe8 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -686,6 +686,11 @@ void Smt2Printer::toStream(std::ostream& out,
out << ' ';
stillNeedToPrintParams = false;
break;
+ case kind::BITVECTOR_BITOF:
+ out << "(_ bitOf " << n.getOperator().getConst<BitVectorBitOf>().d_bitIndex
+ << ") ";
+ stillNeedToPrintParams = false;
+ break;
// sets
case kind::SINGLETON:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback