SMT2: relations on the range type

The range type is encoded using binary (using an offset for negative
numbers).  This adds support for <, <=, >, >= over the range type to the
SMT2 backend.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -3560,9 +3560,11 @@ void smt2_convt::convert_relation(const binary_relation_exprt &expr)
 {
   const typet &op_type=expr.op0().type();
 
-  if(op_type.id()==ID_unsignedbv ||
-     op_type.id()==ID_bv)
+  if(
+    op_type.id() == ID_unsignedbv || op_type.id() == ID_bv ||
+    op_type.id() == ID_range)
   {
+    // The range type is encoded in binary
     out << "(";
     if(expr.id()==ID_le)
       out << "bvule";