summaryrefslogtreecommitdiff
path: root/src/printer/cvc/cvc_printer.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-04-29 20:27:20 -0500
committerGitHub <noreply@github.com>2019-04-29 20:27:20 -0500
commit19a93d5e0f924c70e7f77719e0310c730c8fbc61 (patch)
tree2ce2d68279ebb4b031ab314f7e206862abbc12f8 /src/printer/cvc/cvc_printer.cpp
parentb351cce04bc13e00b4b63f1bba403b5d549d56bf (diff)
Eliminate APPLY kind (#2976)
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
-rw-r--r--src/printer/cvc/cvc_printer.cpp3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index c95ff5781..630d8bdd7 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -280,9 +280,6 @@ void CvcPrinter::toStream(
out << ")";
return;
break;
- case kind::APPLY:
- toStream(op, n.getOperator(), depth, types, true);
- break;
case kind::CHAIN:
case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter
toStream(out, theory::Rewriter::rewrite(n), depth, types, true);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback