diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
index 2be590c8c1b..f7500891a9f 100644
--- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -86,7 +86,7 @@ static const std::string get_thread_block_identifier(
 {
   PRECONDITION(f_code.arguments().size() == 1);
   const exprt &expr = f_code.arguments()[0];
-  mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false);
+  const mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());
   return integer2string(lbl_id);
 }
 
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index f06058bc621..785d52ad8d6 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1811,9 +1811,10 @@ std::string expr2ct::convert_constant(
     if(c_enum_type.id()!=ID_c_enum)
       return convert_norep(src, precedence);
 
-    bool is_signed=c_enum_type.subtype().id()==ID_signedbv;
+    const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
+    const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
 
-    mp_integer int_value = bv2integer(id2string(value), is_signed);
+    mp_integer int_value = bv2integer(id2string(value), width, is_signed);
     mp_integer i=0;
 
     irep_idt int_value_string=integer2string(int_value);
@@ -1849,8 +1850,10 @@ std::string expr2ct::convert_constant(
           type.id()==ID_c_bit_field ||
           type.id()==ID_c_bool)
   {
+    const auto width = to_bitvector_type(type).get_width();
+
     mp_integer int_value =
-      bv2integer(id2string(value), type.id() == ID_signedbv);
+      bv2integer(id2string(value), width, type.id() == ID_signedbv);
 
     const irep_idt &c_type=
       type.id()==ID_c_bit_field?type.subtype().get(ID_C_c_type):
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index e6fc798e8d5..98278adc640 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -1830,11 +1830,12 @@ bool goto_convertt::get_string_constant(
       forall_operands(it, index_op)
         if(it->is_constant())
         {
-          unsigned long i = integer2ulong(
-            bv2integer(id2string(to_constant_expr(*it).get_value()), true));
+          const auto i = numeric_cast<std::size_t>(*it);
+          if(!i.has_value())
+            return true;
 
-          if(i!=0) // to skip terminating 0
-            result+=static_cast<char>(i);
+          if(i.value() != 0) // to skip terminating 0
+            result += static_cast<char>(i.value());
         }
 
       return value=result, false;
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index 6450163818f..b8b085c9d22 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -129,22 +129,25 @@ void goto_trace_stept::output(
 /// \param expr: expression to get numeric representation from
 /// \param options: configuration options
 /// \return a string with the numeric representation
-static std::string
-numeric_representation(const exprt &expr, const trace_optionst &options)
+static std::string numeric_representation(
+  const constant_exprt &expr,
+  const trace_optionst &options)
 {
   std::string result;
   std::string prefix;
+
+  const irep_idt &value = expr.get_value();
+
   if(options.hex_representation)
   {
-    mp_integer value_int =
-      bv2integer(id2string(to_constant_expr(expr).get_value()), false);
+    mp_integer value_int = bv2integer(id2string(value), value.size(), false);
     result = integer2string(value_int, 16);
     prefix = "0x";
   }
   else
   {
     prefix = "0b";
-    result = expr.get_string(ID_value);
+    result = id2string(value);
   }
 
   std::ostringstream oss;
@@ -181,7 +184,8 @@ std::string trace_numeric_value(
        type.id()==ID_c_enum ||
        type.id()==ID_c_enum_tag)
     {
-      const std::string &str = numeric_representation(expr, options);
+      const std::string &str =
+        numeric_representation(to_constant_expr(expr), options);
       return str;
     }
     else if(type.id()==ID_bool)
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 46c0a1b0cca..b56b4a512fb 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -382,7 +382,8 @@ void interpretert::evaluate(
     else if(expr.type().id()==ID_c_bool)
     {
       const irep_idt &value=to_constant_expr(expr).get_value();
-      dest.push_back(bv2integer(id2string(value), false));
+      const auto width = to_c_bool_type(expr.type()).get_width();
+      dest.push_back(bv2integer(id2string(value), width, false));
       return;
     }
     else if(expr.type().id()==ID_bool)
@@ -983,16 +984,16 @@ void interpretert::evaluate(
       }
       else if(expr.type().id()==ID_signedbv)
       {
-        const std::string s =
-          integer2bv(value, to_signedbv_type(expr.type()).get_width());
-        dest.push_back(bv2integer(s, true));
+        const auto width = to_signedbv_type(expr.type()).get_width();
+        const std::string s = integer2bv(value, width);
+        dest.push_back(bv2integer(s, width, true));
         return;
       }
       else if(expr.type().id()==ID_unsignedbv)
       {
-        const std::string s =
-          integer2bv(value, to_unsignedbv_type(expr.type()).get_width());
-        dest.push_back(bv2integer(s, false));
+        const auto width = to_unsignedbv_type(expr.type()).get_width();
+        const std::string s = integer2bv(value, width);
+        dest.push_back(bv2integer(s, width, false));
         return;
       }
       else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
index cd23e92f7bc..29f9a6078ec 100644
--- a/src/util/arith_tools.cpp
+++ b/src/util/arith_tools.cpp
@@ -43,17 +43,20 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
   }
   else if(type_id==ID_unsignedbv)
   {
-    int_value = bv2integer(id2string(value), false);
+    const auto width = to_unsignedbv_type(type).get_width();
+    int_value = bv2integer(id2string(value), width, false);
     return false;
   }
   else if(type_id==ID_signedbv)
   {
-    int_value = bv2integer(id2string(value), true);
+    const auto width = to_signedbv_type(type).get_width();
+    int_value = bv2integer(id2string(value), width, true);
     return false;
   }
   else if(type_id==ID_c_bool)
   {
-    int_value = bv2integer(id2string(value), false);
+    const auto width = to_c_bool_type(type).get_width();
+    int_value = bv2integer(id2string(value), width, false);
     return false;
   }
   else if(type_id==ID_c_enum)
@@ -61,26 +64,36 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
     const typet &subtype=to_c_enum_type(type).subtype();
     if(subtype.id()==ID_signedbv)
     {
-      int_value = bv2integer(id2string(value), true);
+      const auto width = to_signedbv_type(type).get_width();
+      int_value = bv2integer(id2string(value), width, true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value = bv2integer(id2string(value), false);
+      const auto width = to_unsignedbv_type(type).get_width();
+      int_value = bv2integer(id2string(value), width, false);
       return false;
     }
   }
   else if(type_id==ID_c_bit_field)
   {
-    const typet &subtype = to_c_bit_field_type(type).subtype();
+    const auto &c_bit_field_type = to_c_bit_field_type(type);
+    const auto width = c_bit_field_type.get_width();
+    const typet &subtype = c_bit_field_type.subtype();
+
     if(subtype.id()==ID_signedbv)
     {
-      int_value = bv2integer(id2string(value), true);
+      int_value = bv2integer(id2string(value), width, true);
       return false;
     }
     else if(subtype.id()==ID_unsignedbv)
     {
-      int_value = bv2integer(id2string(value), false);
+      int_value = bv2integer(id2string(value), width, false);
+      return false;
+    }
+    else if(subtype.id() == ID_c_bool)
+    {
+      int_value = bv2integer(id2string(value), width, false);
       return false;
     }
   }
diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
index 38842e33ec3..4d54eedba65 100644
--- a/src/util/bv_arithmetic.cpp
+++ b/src/util/bv_arithmetic.cpp
@@ -184,5 +184,5 @@ void bv_arithmetict::from_expr(const exprt &expr)
 {
   PRECONDITION(expr.is_constant());
   spec=bv_spect(expr.type());
-  value = bv2integer(expr.get_string(ID_value), spec.is_signed);
+  value = bv2integer(expr.get_string(ID_value), spec.width, spec.is_signed);
 }
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index 5bee718c7c5..5730acf9303 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -246,8 +246,9 @@ bool exprt::is_one() const
     }
     else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
     {
+      const auto width = to_bitvector_type(type()).get_width();
       mp_integer int_value =
-        bv2integer(id2string(constant_expr.get_value()), false);
+        bv2integer(id2string(constant_expr.get_value()), width, false);
       if(int_value==1)
         return true;
     }
diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp
index 5c5e48332ff..9f6003b4c22 100644
--- a/src/util/fixedbv.cpp
+++ b/src/util/fixedbv.cpp
@@ -26,7 +26,7 @@ fixedbvt::fixedbvt(const constant_exprt &expr)
 void fixedbvt::from_expr(const constant_exprt &expr)
 {
   spec=fixedbv_spect(to_fixedbv_type(expr.type()));
-  v = bv2integer(id2string(expr.get_value()), true);
+  v = bv2integer(id2string(expr.get_value()), spec.width, true);
 }
 
 void fixedbvt::from_integer(const mp_integer &i)
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index cbc363a33df..dbe21afe331 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -1062,7 +1062,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
 void ieee_floatt::from_expr(const constant_exprt &expr)
 {
   spec=ieee_float_spect(to_floatbv_type(expr.type()));
-  unpack(bv2integer(id2string(expr.get_value()), false));
+  unpack(bv2integer(id2string(expr.get_value()), spec.width(), false));
 }
 
 mp_integer ieee_floatt::to_integer() const
diff --git a/src/util/mp_arith.cpp b/src/util/mp_arith.cpp
index 810884790db..e858078617b 100644
--- a/src/util/mp_arith.cpp
+++ b/src/util/mp_arith.cpp
@@ -192,8 +192,10 @@ const std::string integer2bv(const mp_integer &src, std::size_t width)
 }
 
 /// convert a bit-vector representation (possibly signed) to integer
-const mp_integer bv2integer(const std::string &src, bool is_signed)
+const mp_integer
+bv2integer(const std::string &src, std::size_t width, bool is_signed)
 {
+  PRECONDITION(src.size() == width);
   return binary2integer(src, is_signed);
 }
 
diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h
index aa09701cbcb..9ff40e76947 100644
--- a/src/util/mp_arith.h
+++ b/src/util/mp_arith.h
@@ -55,7 +55,8 @@ const mp_integer binary2integer(const std::string &, bool is_signed);
 const std::string integer2bv(const mp_integer &, std::size_t width);
 
 /// convert a bit-vector representation (possibly signed) to integer
-const mp_integer bv2integer(const std::string &, bool is_signed);
+const mp_integer
+bv2integer(const std::string &, std::size_t width, bool is_signed);
 
 /// \deprecated use numeric_cast_v<unsigned long long> instead
 DEPRECATED("Use numeric_cast_v<unsigned long long> instead")
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 3dc894c3307..440e6562cbe 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -669,7 +669,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
          expr_type_id==ID_signedbv ||
          expr_type_id==ID_floatbv)
       {
-        mp_integer int_value = bv2integer(id2string(value), false);
+        const auto width = to_bv_type(op_type).get_width();
+        mp_integer int_value = bv2integer(id2string(value), width, false);
         expr=from_integer(int_value, expr_type);
         return false;
       }
@@ -811,71 +812,32 @@ bool simplify_exprt::simplify_if_implies(
        expr.op1().is_constant() &&
        cond.op1().type()==expr.op1().type())
     {
-      const irep_idt &type_id=cond.op1().type().id();
-      if(type_id==ID_integer || type_id==ID_natural)
-      {
-        if(string2integer(cond.op1().get_string(ID_value))>=
-           string2integer(expr.op1().get_string(ID_value)))
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-      else if(type_id==ID_unsignedbv)
-      {
-        const mp_integer i1, i2;
-        if(
-          bv2integer(cond.op1().get_string(ID_value), false) >=
-          bv2integer(expr.op1().get_string(ID_value), false))
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-      else if(type_id==ID_signedbv)
+      mp_integer i1, i2;
+
+      if(
+        !to_integer(to_constant_expr(cond.op1()), i1) &&
+        !to_integer(to_constant_expr(expr.op1()), i2))
       {
-        const mp_integer i1, i2;
-        if(
-          bv2integer(cond.op1().get_string(ID_value), true) >=
-          bv2integer(expr.op1().get_string(ID_value), true))
+        if(i1 >= i2)
         {
           new_truth = true;
           return false;
         }
       }
     }
+
     if(cond.op1()==expr.op1() &&
        cond.op0().is_constant() &&
        expr.op0().is_constant() &&
        cond.op0().type()==expr.op0().type())
     {
-      const irep_idt &type_id = cond.op1().type().id();
-      if(type_id==ID_integer || type_id==ID_natural)
-      {
-        if(string2integer(cond.op1().get_string(ID_value))<=
-           string2integer(expr.op1().get_string(ID_value)))
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-      else if(type_id==ID_unsignedbv)
-      {
-        const mp_integer i1, i2;
-        if(
-          bv2integer(cond.op1().get_string(ID_value), false) <=
-          bv2integer(expr.op1().get_string(ID_value), false))
-        {
-          new_truth = true;
-          return false;
-        }
-      }
-      else if(type_id==ID_signedbv)
+      mp_integer i1, i2;
+
+      if(
+        !to_integer(to_constant_expr(cond.op0()), i1) &&
+        !to_integer(to_constant_expr(expr.op0()), i2))
       {
-        const mp_integer i1, i2;
-        if(
-          bv2integer(cond.op1().get_string(ID_value), true) <=
-          bv2integer(expr.op1().get_string(ID_value), true))
+        if(i1 <= i2)
         {
           new_truth = true;
           return false;
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 0e145f310ee..510343eb223 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -387,7 +387,9 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     else
     {
       // this is a pointer, we can't use to_integer
-      mp_integer number = bv2integer(id2string(c_ptr.get_value()), false);
+      const auto width = to_pointer_type(ptr.type()).get_width();
+      mp_integer number =
+        bv2integer(id2string(c_ptr.get_value()), width, false);
       // a null pointer would have been caught above, return value 0
       // will indicate that conversion failed
       if(number==0)