implement flattening for +/- for the range type

The flattening solver backend lowers the integer range type to bitvectors.
This adds support for addition and subtraction for the range type via
lowering to bitvector addition/subtraction.

Author: kroening

src/solvers/flattening/boolbv_add_sub.cpp

@@ -124,6 +124,15 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
         }
       }
     }
+    else if(type.id() == ID_range)
+    {
+      // add: lhs + from + rhs + from - from = lhs + rhs + from
+      // sub: lhs + from - (rhs + from) - from = lhs - rhs - from
+      mp_integer from = to_range_type(type).get_from();
+      bv = bv_utils.add_sub(bv, op, subtract);
+      bv = bv_utils.add_sub(
+        bv, bv_utils.build_constant(from, op.size()), subtract);
+    }
     else if(type.id()==ID_floatbv)
     {
       // needs to change due to rounding mode