diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 2402bb8ca92..44947aa21fc 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/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";