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.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 9ccf02301..2a55cb972 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -409,7 +409,7 @@ void CvcPrinter::toStream(
case kind::APPLY_TYPE_ASCRIPTION: {
toStream(out, n[0], depth, types, false);
out << "::";
- TypeNode t = TypeNode::fromType(n.getOperator().getConst<AscriptionType>().getType());
+ TypeNode t = n.getOperator().getConst<AscriptionType>().getType();
out << (t.isFunctionLike() ? t.getRangeType() : t);
}
return;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback