diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp index 11560c150ad..f2b495521c5 100644 --- a/src/util/format_type.cpp +++ b/src/util/format_type.cpp @@ -98,6 +98,12 @@ std::ostream &format_rec(std::ostream &os, const typet &type) return os << "\xe2\x84\xa4"; // u+2124, 'Z' else if(id == ID_natural) return os << "\xe2\x84\x95"; // u+2115, 'N' + else if(id == ID_range) + { + auto &range_type = to_range_type(type); + return os << "{ " << range_type.get_from() << ", ..., " + << range_type.get_to() << " }"; + } else if(id == ID_rational) return os << "\xe2\x84\x9a"; // u+211A, 'Q' else if(id == ID_mathematical_function) diff --git a/unit/Makefile b/unit/Makefile index 285bd40e043..b42983234a1 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -144,6 +144,7 @@ SRC += analyses/ai/ai.cpp \ util/format.cpp \ util/format_expr.cpp \ util/format_number_range.cpp \ + util/format_type.cpp \ util/get_base_name.cpp \ util/graph.cpp \ util/help_formatter.cpp \