Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).

1 files changed, 0 insertions, 13 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2ba593377..aa9c17e5a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -281,19 +281,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
-    case kind::SUBRANGE_TYPE: {
-      const SubrangeBounds& bounds = n.getConst<SubrangeBounds>();
-      // No way to represent subranges in SMT-LIBv2; this is inspired
-      // by yices format (but isn't identical to it).
-      out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')';
-      break;
-    }
-    case kind::SUBTYPE_TYPE:
-      // No way to represent predicate subtypes in SMT-LIBv2; this is
-      // inspired by yices format (but isn't identical to it).
-      out << "(subtype " << n.getConst<Predicate>() << ')';
-      break;
-
     case kind::DATATYPE_TYPE:
       {
         const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));