summaryrefslogtreecommitdiff
path: root/src/printer/cvc/cvc_printer.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
-rw-r--r--src/printer/cvc/cvc_printer.cpp6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f0a936c97..ecc224026 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -493,9 +493,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
case kind::BITVECTOR_UDIV:
op << "BVUDIV";
break;
+ case kind::BITVECTOR_UDIV_TOTAL:
+ op << "BVUDIV_TOTAL";
+ break;
case kind::BITVECTOR_UREM:
op << "BVUREM";
break;
+ case kind::BITVECTOR_UREM_TOTAL:
+ op << "BVUREM_TOTAL";
+ break;
case kind::BITVECTOR_SDIV:
op << "BVSDIV";
break;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback