diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 21b36dc2d13..b2386f73f96 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -164,7 +164,8 @@ void rw_range_sett::get_objects_byte_extract(
       be.id()==ID_byte_extract_little_endian,
       ns);
     assert(index<std::numeric_limits<size_t>::max());
-    range_spect offset=range_start + map.map_bit(integer2size_t(index));
+    range_spect offset =
+      range_start + map.map_bit(numeric_cast_v<std::size_t>(index));
     get_objects_rec(mode, be.op(), offset, size);
   }
 }
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index cf20ab85dd8..3a92a58bdcb 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -107,7 +107,7 @@ exprt c_typecheck_baset::do_initializer_rec(
       if(mp_integer(tmp.operands().size())>array_size)
       {
         // cut off long strings. gcc does a warning for this
-        tmp.operands().resize(integer2size_t(array_size));
+        tmp.operands().resize(numeric_cast_v<std::size_t>(array_size));
         tmp.type()=type;
       }
       else if(mp_integer(tmp.operands().size())<array_size)
@@ -123,7 +123,7 @@ exprt c_typecheck_baset::do_initializer_rec(
                   << to_string(full_type.subtype()) << "'" << eom;
           throw 0;
         }
-        tmp.operands().resize(integer2size_t(array_size), *zero);
+        tmp.operands().resize(numeric_cast_v<std::size_t>(array_size), *zero);
       }
     }
 
@@ -167,7 +167,7 @@ exprt c_typecheck_baset::do_initializer_rec(
       if(mp_integer(tmp2.operands().size())>array_size)
       {
         // cut off long strings. gcc does a warning for this
-        tmp2.operands().resize(integer2size_t(array_size));
+        tmp2.operands().resize(numeric_cast_v<std::size_t>(array_size));
         tmp2.type()=type;
       }
       else if(mp_integer(tmp2.operands().size())<array_size)
@@ -183,7 +183,7 @@ exprt c_typecheck_baset::do_initializer_rec(
                   << to_string(full_type.subtype()) << "'" << eom;
           throw 0;
         }
-        tmp2.operands().resize(integer2size_t(array_size), *zero);
+        tmp2.operands().resize(numeric_cast_v<std::size_t>(array_size), *zero);
       }
     }
 
@@ -323,7 +323,7 @@ void c_typecheck_baset::designator_enter(
         throw 0;
       }
 
-      entry.size=integer2size_t(array_size);
+      entry.size = numeric_cast_v<std::size_t>(array_size);
       entry.subtype=array_type.subtype();
     }
   }
@@ -341,7 +341,7 @@ void c_typecheck_baset::designator_enter(
       throw 0;
     }
 
-    entry.size=integer2size_t(vector_size);
+    entry.size = numeric_cast_v<std::size_t>(vector_size);
     entry.subtype=vector_type.subtype();
   }
   else
@@ -410,7 +410,8 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
                     << to_string(full_type.subtype()) << "'" << eom;
             throw 0;
           }
-          dest->operands().resize(integer2size_t(index) + 1, *zero);
+          dest->operands().resize(
+            numeric_cast_v<std::size_t>(index) + 1, *zero);
 
           // todo: adjust type!
         }
@@ -424,7 +425,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         }
       }
 
-      dest=&(dest->operands()[integer2size_t(index)]);
+      dest = &(dest->operands()[numeric_cast_v<std::size_t>(index)]);
     }
     else if(full_type.id()==ID_struct)
     {
@@ -730,8 +731,8 @@ designatort c_typecheck_baset::make_designator(
         throw 0;
       }
 
-      entry.index=integer2size_t(index);
-      entry.size=integer2size_t(size);
+      entry.index = numeric_cast_v<std::size_t>(index);
+      entry.size = numeric_cast_v<std::size_t>(size);
       entry.subtype=full_type.subtype();
     }
     else if(full_type.id()==ID_struct ||
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index b337d7da65f..2a84f09788e 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -1378,7 +1378,7 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
       throw 0;
     }
 
-    type.set_width(integer2size_t(i));
+    type.set_width(numeric_cast_v<std::size_t>(i));
     type.remove(ID_size);
   }
 
diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index 1df5ac652fa..6d4d850406f 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -214,7 +214,7 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
           {
             const mp_integer pad_bytes = a - displacement;
             std::size_t pad_bits =
-              integer2size_t(pad_bytes * config.ansi_c.char_width);
+              numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
             it = pad(components, it, pad_bits);
             offset += pad_bytes;
           }
@@ -262,7 +262,7 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
   {
     const mp_integer pad_bytes = a - displacement;
     const std::size_t pad_bits =
-      integer2size_t(pad_bytes * config.ansi_c.char_width);
+      numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
     pad(components, components.end(), pad_bits);
     offset += pad_bytes;
   }
@@ -392,7 +392,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
       {
         const mp_integer pad_bytes = a - displacement;
         const std::size_t pad_bits =
-          integer2size_t(pad_bytes * config.ansi_c.char_width);
+          numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
         it = pad(components, it, pad_bits);
         offset += pad_bytes;
       }
@@ -433,7 +433,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
     {
       mp_integer pad_bytes = max_alignment - displacement;
       std::size_t pad_bits =
-        integer2size_t(pad_bytes * config.ansi_c.char_width);
+        numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
       pad(components, components.end(), pad_bits);
     }
   }
@@ -491,7 +491,7 @@ void add_padding(union_typet &type, const namespacet &ns)
       max_alignment_bits-(size_bits%max_alignment_bits);
 
     unsignedbv_typet padding_type(
-      integer2size_t(size_bits+padding_bits));
+      numeric_cast_v<std::size_t>(size_bits + padding_bits));
 
     struct_typet::componentt component;
     component.type()=padding_type;
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index f00d989b2b7..df1c9fdafbe 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -501,7 +501,7 @@ exprt interpretert::get_value(
     }
 
     // Retrieve the value for each member in the array
-    result.reserve_operands(integer2size_t(count));
+    result.reserve_operands(numeric_cast_v<std::size_t>(count));
     for(mp_integer i=0; i<count; ++i)
     {
       const exprt operand=get_value(
@@ -568,7 +568,7 @@ exprt interpretert::get_value(
     }
 
     // Retrieve the value for each member in the array
-    result.reserve_operands(integer2size_t(count));
+    result.reserve_operands(numeric_cast_v<std::size_t>(count));
     for(mp_integer i=0; i<count; ++i)
     {
       const exprt operand=get_value(type.subtype(), rhs,
@@ -580,35 +580,36 @@ exprt interpretert::get_value(
   else if(real_type.id()==ID_floatbv)
   {
     ieee_floatt f(to_floatbv_type(type));
-    f.unpack(rhs[integer2size_t(offset)]);
+    f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
     return f.to_expr();
   }
   else if(real_type.id()==ID_fixedbv)
   {
     fixedbvt f;
-    f.from_integer(rhs[integer2size_t(offset)]);
+    f.from_integer(rhs[numeric_cast_v<std::size_t>(offset)]);
     return f.to_expr();
   }
   else if(real_type.id()==ID_bool)
   {
-    if(rhs[integer2size_t(offset)]!=0)
+    if(rhs[numeric_cast_v<std::size_t>(offset)] != 0)
       return true_exprt();
     else
       false_exprt();
   }
   else if(real_type.id()==ID_c_bool)
   {
-    return from_integer(rhs[integer2size_t(offset)]!=0?1:0, type);
+    return from_integer(
+      rhs[numeric_cast_v<std::size_t>(offset)] != 0 ? 1 : 0, type);
   }
   else if(real_type.id() == ID_pointer)
   {
-    if(rhs[integer2size_t(offset)]==0)
+    if(rhs[numeric_cast_v<std::size_t>(offset)] == 0)
       return null_pointer_exprt(to_pointer_type(real_type)); // NULL pointer
 
-    if(rhs[integer2size_t(offset)]<memory.size())
+    if(rhs[numeric_cast_v<std::size_t>(offset)] < memory.size())
     {
       // We want the symbol pointed to
-      mp_integer address=rhs[integer2size_t(offset)];
+      mp_integer address = rhs[numeric_cast_v<std::size_t>(offset)];
       irep_idt identifier=address_to_identifier(address);
       mp_integer offset=address_to_offset(address);
       const typet type=get_type(identifier);
@@ -631,8 +632,9 @@ exprt interpretert::get_value(
       return std::move(index_expr);
     }
 
-    error() << "interpreter: invalid pointer " << rhs[integer2size_t(offset)]
-            << " > object count " << memory.size() << eom;
+    error() << "interpreter: invalid pointer "
+            << rhs[numeric_cast_v<std::size_t>(offset)] << " > object count "
+            << memory.size() << eom;
 
     throw "interpreter: reading from invalid pointer";
   }
@@ -640,7 +642,8 @@ exprt interpretert::get_value(
   {
     // Strings are currently encoded by their irep_idt ID.
     return constant_exprt(
-      get_string_container().get_string(rhs[integer2size_t(offset)].to_long()),
+      get_string_container().get_string(
+        numeric_cast_v<std::size_t>(rhs[numeric_cast_v<std::size_t>(offset)])),
       type);
   }
 
@@ -680,8 +683,8 @@ void interpretert::execute_assign()
     side_effect_exprt side_effect=to_side_effect_expr(code_assign.rhs());
     if(side_effect.get_statement()==ID_nondet)
     {
-      mp_integer address=
-        integer2size_t(evaluate_address(code_assign.lhs()));
+      mp_integer address =
+        numeric_cast_v<std::size_t>(evaluate_address(code_assign.lhs()));
 
       mp_integer size=
         get_size(code_assign.lhs().type());
@@ -710,11 +713,11 @@ void interpretert::assign(
       {
         status() << total_steps << " ** assigning "
                  << address_to_identifier(address_val) << "["
-                 << address_to_offset(address_val) << "]:="
-                 << rhs[integer2size_t(i)]
-                 << "\n" << eom;
+                 << address_to_offset(address_val)
+                 << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
+                 << eom;
       }
-      cell.value=rhs[integer2size_t(i)];
+      cell.value = rhs[numeric_cast_v<std::size_t>(i)];
       if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
         cell.initialized=memory_cellt::initializedt::WRITTEN_BEFORE_READ;
     }
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index a133646b1c7..310241fb5ac 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -50,7 +50,7 @@ void interpretert::read_unbounded(
   mp_vectort &dest) const
 {
   // copy memory region
-  std::size_t address_val=integer2size_t(address);
+  std::size_t address_val = numeric_cast_v<std::size_t>(address);
   const mp_integer offset=address_to_offset(address_val);
   const mp_integer alloc_size=
     base_address_to_actual_size(address_val-offset);
@@ -61,7 +61,8 @@ void interpretert::read_unbounded(
 
     if((address+i)<memory.size())
     {
-      const memory_cellt &cell=memory[integer2size_t(address+i)];
+      const memory_cellt &cell =
+        memory[numeric_cast_v<std::size_t>(address + i)];
       value=cell.value;
       if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
         cell.initialized=memory_cellt::initializedt::READ_BEFORE_WRITTEN;
@@ -315,7 +316,7 @@ void interpretert::evaluate(
   {
     if(expr.type().id()==ID_struct)
     {
-      dest.reserve(integer2size_t(get_size(expr.type())));
+      dest.reserve(numeric_cast_v<std::size_t>(get_size(expr.type())));
       bool error=false;
 
       forall_operands(it, expr)
@@ -418,7 +419,7 @@ void interpretert::evaluate(
   else if(expr.id()==ID_struct)
   {
     if(!unbounded_size(expr.type()))
-      dest.reserve(integer2size_t(get_size(expr.type())));
+      dest.reserve(numeric_cast_v<std::size_t>(get_size(expr.type())));
 
     bool error=false;
 
@@ -959,7 +960,7 @@ void interpretert::evaluate(
     {
       if(!unbounded_size(expr.type()))
       {
-        dest.resize(integer2size_t(get_size(expr.type())));
+        dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type())));
         read(address, dest);
       }
       else
@@ -1026,7 +1027,7 @@ void interpretert::evaluate(
 
     if(size.size()==1)
     {
-      std::size_t size_int=integer2size_t(size[0]);
+      std::size_t size_int = numeric_cast_v<std::size_t>(size[0]);
       for(std::size_t i=0; i<size_int; ++i)
         evaluate(expr.op0(), dest);
       return;
@@ -1052,10 +1053,11 @@ void interpretert::evaluate(
       mp_integer need_size=(where_idx+1)*subtype_size;
 
       if(dest.size()<need_size)
-        dest.resize(integer2size_t(need_size), 0);
+        dest.resize(numeric_cast_v<std::size_t>(need_size), 0);
 
       for(std::size_t i=0; i<new_value.size(); ++i)
-        dest[integer2size_t((where_idx*subtype_size)+i)]=new_value[i];
+        dest[numeric_cast_v<std::size_t>((where_idx * subtype_size) + i)] =
+          new_value[i];
 
       return;
     }
diff --git a/src/goto-programs/remove_const_function_pointers.cpp b/src/goto-programs/remove_const_function_pointers.cpp
index acc49169674..d109fcc9254 100644
--- a/src/goto-programs/remove_const_function_pointers.cpp
+++ b/src/goto-programs/remove_const_function_pointers.cpp
@@ -537,8 +537,8 @@ bool remove_const_function_pointerst::try_resolve_index_of(
         if(try_resolve_index_value(index_expr.index(), value))
         {
           expressionst array_out_functions;
-          const exprt &func_expr=
-            potential_array_expr.operands()[integer2size_t(value)];
+          const exprt &func_expr =
+            potential_array_expr.operands()[numeric_cast_v<std::size_t>(value)];
           bool value_const=false;
           bool resolved_value=
             try_resolve_expression(func_expr, array_out_functions, value_const);
diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp
index ee8da285581..6b9326492cf 100644
--- a/src/goto-programs/remove_vector.cpp
+++ b/src/goto-programs/remove_vector.cpp
@@ -98,7 +98,7 @@ static void remove_vector(exprt &expr)
       // do component-wise:
       // x+y -> vector(x[0]+y[0],x[1]+y[1],...)
       array_exprt array_expr(array_type);
-      array_expr.operands().resize(integer2size_t(dimension));
+      array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
 
       for(std::size_t i=0; i<array_expr.operands().size(); i++)
       {
@@ -125,7 +125,7 @@ static void remove_vector(exprt &expr)
       // do component-wise:
       // -x -> vector(-x[0],-x[1],...)
       array_exprt array_expr(array_type);
-      array_expr.operands().resize(integer2size_t(dimension));
+      array_expr.operands().resize(numeric_cast_v<std::size_t>(dimension));
 
       for(std::size_t i=0; i<array_expr.operands().size(); i++)
       {
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
index c8bd3759891..ad89cf30c51 100644
--- a/src/goto-programs/vcd_goto_trace.cpp
+++ b/src/goto-programs/vcd_goto_trace.cpp
@@ -15,6 +15,7 @@ Date: June 2011
 
 #include <ctime>
 
+#include <util/arith_tools.h>
 #include <util/numbering.h>
 #include <util/pointer_offset_size.h>
 
@@ -62,7 +63,7 @@ std::string as_vcd_binary(
   const auto width = pointer_offset_bits(type, ns);
 
   if(width.has_value())
-    return std::string(integer2size_t(*width), 'x');
+    return std::string(numeric_cast_v<std::size_t>(*width), 'x');
   else
     return "";
 }
diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp
index 0ccca1d2a11..258e71040e2 100644
--- a/src/solvers/flattening/boolbv_byte_update.cpp
+++ b/src/solvers/flattening/boolbv_byte_update.cpp
@@ -53,7 +53,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
       if(little_endian)
       {
         for(std::size_t i=0; i<update_width; i++)
-          bv[integer2size_t(offset+i)]=value_bv[i];
+          bv[numeric_cast_v<std::size_t>(offset + i)] = value_bv[i];
       }
       else
       {
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
index 930df8f9b94..9ba71cb9dc5 100644
--- a/src/solvers/flattening/boolbv_get.cpp
+++ b/src/solvers/flattening/boolbv_get.cpp
@@ -390,7 +390,7 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
     result=exprt(ID_array, type);
     result.type().set(ID_size, size);
 
-    std::size_t size_int=integer2size_t(size_mpint);
+    std::size_t size_int = numeric_cast_v<std::size_t>(size_mpint);
 
     // allocate operands
     result.operands().resize(size_int);
@@ -404,7 +404,8 @@ exprt boolbvt::bv_get_unbounded_array(const exprt &expr) const
         it!=values.end();
         it++)
       if(it->first>=0 && it->first<size_mpint)
-        result.operands()[integer2size_t(it->first)].swap(it->second);
+        result.operands()[numeric_cast_v<std::size_t>(it->first)].swap(
+          it->second);
   }
 
   return result;
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index 4c0202c3940..d67e65c1993 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -221,8 +221,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)
         mp_integer offset=i*width;
 
         for(std::size_t j=0; j<width; j++)
-          equal_bv[j]=prop.lequal(bv[j],
-                             array_bv[integer2size_t(offset+j)]);
+          equal_bv[j] = prop.lequal(
+            bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
 
         prop.l_set_to_true(
           prop.limplies(convert(index_equality), prop.land(equal_bv)));
@@ -255,7 +255,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
         for(std::size_t j=0; j<width; j++)
         {
-          literalt l=array_bv[integer2size_t(offset+j)];
+          literalt l = array_bv[numeric_cast_v<std::size_t>(offset + j)];
 
           if(i==0) // this initializes bv
             bv[j]=l;
@@ -313,7 +313,7 @@ bvt boolbvt::convert_index(
     // If not there are large improvements possible as above
 
     for(std::size_t i=0; i<width; i++)
-      bv[i]=tmp[integer2size_t(offset+i)];
+      bv[i] = tmp[numeric_cast_v<std::size_t>(offset + i)];
   }
   else if(
     array.id() == ID_member || array.id() == ID_index ||
diff --git a/src/solvers/flattening/boolbv_shift.cpp b/src/solvers/flattening/boolbv_shift.cpp
index d66c9f41e62..e0559811aba 100644
--- a/src/solvers/flattening/boolbv_shift.cpp
+++ b/src/solvers/flattening/boolbv_shift.cpp
@@ -58,7 +58,7 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
     if(i<0 || i>std::numeric_limits<signed>::max())
       distance=0;
     else
-      distance=integer2size_t(i);
+      distance = numeric_cast_v<std::size_t>(i);
 
     if(type_id==ID_verilog_signedbv ||
        type_id==ID_verilog_unsignedbv)
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
index 093c76ccd5f..6f796c3bed3 100644
--- a/src/solvers/flattening/boolbv_with.cpp
+++ b/src/solvers/flattening/boolbv_with.cpp
@@ -192,7 +192,7 @@ void boolbvt::convert_with_bv(
     next_bv=prev_bv;
 
     if(op1_value<next_bv.size())
-      next_bv[integer2size_t(op1_value)]=l;
+      next_bv[numeric_cast_v<std::size_t>(op1_value)] = l;
 
     return;
   }
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index a6c71a92adf..791c06475b1 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -640,7 +640,8 @@ exprt bv_pointerst::bv_get_rec(
   constant_exprt result(bvrep, type);
 
   pointer_logict::pointert pointer;
-  pointer.object=integer2size_t(binary2integer(value_addr, false));
+  pointer.object =
+    numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
   pointer.offset=binary2integer(value_offset, true);
 
   // we add the elaborated expression as operand
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
index d8fd94ae8f8..0b3573f98de 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/src/solvers/lowering/byte_operators.cpp
@@ -556,7 +556,7 @@ exprt flatten_byte_update(
     // do a shift, mask and OR
     const auto type_width = pointer_offset_bits(t, ns);
     CHECK_RETURN(type_width.has_value() && *type_width > 0);
-    const std::size_t width = integer2size_t(*type_width);
+    const std::size_t width = numeric_cast_v<std::size_t>(*type_width);
 
     INVARIANT(
       element_size * 8 <= width,
diff --git a/src/solvers/lowering/popcount.cpp b/src/solvers/lowering/popcount.cpp
index d31d4a84475..617a2d092db 100644
--- a/src/solvers/lowering/popcount.cpp
+++ b/src/solvers/lowering/popcount.cpp
@@ -29,7 +29,7 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
   const auto x_width = pointer_offset_bits(x.type(), ns);
   CHECK_RETURN(x_width.has_value() && *x_width >= 1);
   const std::size_t bits = address_bits(*x_width);
-  const std::size_t new_width = integer2size_t(power(2, bits));
+  const std::size_t new_width = numeric_cast_v<std::size_t>(power(2, bits));
   const bool need_typecast =
     new_width > *x_width || x.type().id() != ID_unsignedbv;
   if(need_typecast)
diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp
index 35d42f86b85..6f176fba9ab 100644
--- a/src/solvers/qbf/qbf_qube_core.cpp
+++ b/src/solvers/qbf/qbf_qube_core.cpp
@@ -14,7 +14,6 @@ Author: CM Wintersteiger
 
 #include <util/arith_tools.h>
 #include <util/invariant.h>
-#include <util/mp_arith.h>
 
 qbf_qube_coret::qbf_qube_coret() : qdimacs_coret()
 {
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 4f8004e8fba..38c35dec4ef 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -478,7 +478,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
     // split into object and offset
     mp_integer pow=power(2, width-config.bv_encoding.object_bits);
     pointer_logict::pointert ptr;
-    ptr.object=integer2size_t(v/pow);
+    ptr.object = numeric_cast_v<std::size_t>(v / pow);
     ptr.offset=v%pow;
     return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
   }
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
index fbc2ddff67d..6829d1384f6 100644
--- a/src/util/endianness_map.cpp
+++ b/src/util/endianness_map.cpp
@@ -42,7 +42,7 @@ void endianness_mapt::build_little_endian(const typet &src)
   if(!s.has_value())
     return;
 
-  std::size_t new_size = map.size() + integer2size_t(*s);
+  const std::size_t new_size = map.size() + numeric_cast_v<std::size_t>(*s);
   map.reserve(new_size);
 
   for(std::size_t i=map.size(); i<new_size; ++i)
@@ -66,7 +66,8 @@ void endianness_mapt::build_big_endian(const typet &src)
     auto bits = pointer_offset_bits(src, ns); // error is -1
     CHECK_RETURN(bits.has_value());
 
-    size_t bits_int = integer2size_t(*bits), base = map.size();
+    const std::size_t bits_int = numeric_cast_v<std::size_t>(*bits);
+    const std::size_t base = map.size();
 
     for(size_t bit=0; bit<bits_int; bit++)
     {
@@ -123,7 +124,7 @@ void endianness_mapt::build_big_endian(const typet &src)
     if(!s.has_value())
       return;
 
-    std::size_t new_size = map.size() + integer2size_t(*s);
+    const std::size_t new_size = map.size() + numeric_cast_v<std::size_t>(*s);
     map.reserve(new_size);
 
     for(std::size_t i=map.size(); i<new_size; ++i)
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 198e89671a2..cb0b9835e07 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -202,7 +202,8 @@ std::string ieee_floatt::to_string_decimal(std::size_t precision) const
       // pad with zeros from the front, if needed
       while(mp_integer(tmp.size())<=position) tmp="0"+tmp;
 
-      std::size_t dot=tmp.size()-integer2size_t(position);
+      const std::size_t dot =
+        tmp.size() - numeric_cast_v<std::size_t>(position);
       result+=std::string(tmp, 0, dot)+'.';
       result+=std::string(tmp, dot, std::string::npos);
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index bc8b22b61fe..d4d1a2d2b7e 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1505,11 +1505,10 @@ exprt simplify_exprt::bits2expr(
       const auto m_size = pointer_offset_bits(component.type(), ns);
       CHECK_RETURN(m_size.has_value() && *m_size>=0);
 
-      std::string comp_bits=
-        std::string(
-          bits,
-          integer2size_t(m_offset_bits),
-          integer2size_t(*m_size));
+      std::string comp_bits = std::string(
+        bits,
+        numeric_cast_v<std::size_t>(m_offset_bits),
+        numeric_cast_v<std::size_t>(*m_size));
 
       exprt comp=bits2expr(comp_bits, component.type(), little_endian);
       if(comp.is_nil())
@@ -1530,7 +1529,7 @@ exprt simplify_exprt::bits2expr(
     const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns);
     CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
 
-    const std::size_t el_size = integer2size_t(*el_size_opt);
+    const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
 
     array_exprt result(array_type);
     result.reserve_operands(n_el);
@@ -1722,7 +1721,9 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
       const_bits+=const_bits;
 
     std::string el_bits = std::string(
-      const_bits, integer2size_t(*offset * 8), integer2size_t(*el_size));
+      const_bits,
+      numeric_cast_v<std::size_t>(*offset * 8),
+      numeric_cast_v<std::size_t>(*el_size));
 
     exprt tmp=
       bits2expr(
@@ -1759,8 +1760,8 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
   {
     std::string bits_cut = std::string(
       bits.value(),
-      integer2size_t(*offset * 8),
-      integer2size_t(el_size.value()));
+      numeric_cast_v<std::size_t>(*offset * 8),
+      numeric_cast_v<std::size_t>(*el_size));
 
     exprt tmp=
       bits2expr(
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index 2a1226c4a5f..f4a2aea43b6 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -199,7 +199,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
         {
           ieee_floatt result(to_constant_expr(casted_expr));
           result.rounding_mode =
-            (ieee_floatt::rounding_modet)integer2size_t(rounding_mode_index);
+            (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
+              rounding_mode_index);
           result.change_spec(
             ieee_float_spect(to_floatbv_type(dest_type)));
           expr=result.to_expr();
@@ -212,7 +213,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
           {
             ieee_floatt result(to_constant_expr(casted_expr));
             result.rounding_mode =
-              (ieee_floatt::rounding_modet)integer2size_t(rounding_mode_index);
+              (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
+                rounding_mode_index);
             mp_integer value=result.to_integer();
             expr=from_integer(value, dest_type);
             return false;
@@ -229,7 +231,8 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr)
           {
             ieee_floatt result(to_floatbv_type(dest_type));
             result.rounding_mode =
-              (ieee_floatt::rounding_modet)integer2size_t(rounding_mode_index);
+              (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(
+                rounding_mode_index);
             result.from_integer(value);
             expr=result.to_expr();
             return false;
@@ -313,8 +316,8 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
     mp_integer rounding_mode;
     if(!to_integer(op2, rounding_mode))
     {
-      v0.rounding_mode=
-        (ieee_floatt::rounding_modet)integer2size_t(rounding_mode);
+      v0.rounding_mode =
+        (ieee_floatt::rounding_modet)numeric_cast_v<std::size_t>(rounding_mode);
       v1.rounding_mode=v0.rounding_mode;
 
       ieee_floatt result=v0;
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index d85299c6b9e..2945efb4c26 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1144,7 +1144,8 @@ bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr)
     std::string svalue=id2string(value);
 
     std::string extracted_value = svalue.substr(
-      integer2size_t(*width - start - 1), integer2size_t(start - end + 1));
+      numeric_cast_v<std::size_t>(*width - start - 1),
+      numeric_cast_v<std::size_t>(start - end + 1));
 
     constant_exprt result(extracted_value, expr.type());
     expr.swap(result);
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 7c9ae292896..2d11add8273 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -217,7 +217,8 @@ bool simplify_exprt::simplify_member(exprt &expr)
       if(bits.has_value() &&
          mp_integer(bits->size())>=target_bits)
       {
-        std::string bits_cut=std::string(*bits, 0, integer2size_t(target_bits));
+        std::string bits_cut =
+          std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
 
         exprt tmp=bits2expr(bits_cut, expr.type(), true);