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.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 4d784c383..63529c2a5 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -316,6 +316,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
break;
case kind::APPLY_CONSTRUCTOR:
case kind::APPLY_SELECTOR:
+ case kind::APPLY_SELECTOR_TOTAL:
case kind::APPLY_TESTER:
toStream(op, n.getOperator(), depth, types, false);
break;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback