diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp
index 271d48111b..95b43a3e9e 100644
--- a/jbmc/src/java_bytecode/expr2java.cpp
+++ b/jbmc/src/java_bytecode/expr2java.cpp
@@ -191,21 +191,17 @@ std::string expr2javat::convert_constant(
     std::string dest;
     dest.reserve(char_representation_length);
 
-    mp_integer int_value;
-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const char16_t int_value = numeric_cast_v<char16_t>(src);
 
     // Character literals in Java have type 'char', thus no cast is needed.
     // This is different from C, where charater literals have type 'int'.
-    dest += '\'' + utf16_native_endian_to_java(int_value.to_long()) + '\'';
+    dest += '\'' + utf16_native_endian_to_java(int_value) + '\'';
     return dest;
   }
   else if(src.type()==java_byte_type())
   {
     // No byte-literals in Java, so just cast:
-    mp_integer int_value;
-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const mp_integer int_value = numeric_cast_v<mp_integer>(src);
     std::string dest="(byte)";
     dest+=integer2string(int_value);
     return dest;
@@ -213,9 +209,7 @@ std::string expr2javat::convert_constant(
   else if(src.type()==java_short_type())
   {
     // No short-literals in Java, so just cast:
-    mp_integer int_value;
-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const mp_integer int_value = numeric_cast_v<mp_integer>(src);
     std::string dest="(short)";
     dest+=integer2string(int_value);
     return dest;
@@ -223,9 +217,7 @@ std::string expr2javat::convert_constant(
   else if(src.type()==java_long_type())
   {
     // long integer literals must have 'L' at the end
-    mp_integer int_value;
-    if(to_integer(src, int_value))
-      UNREACHABLE;
+    const mp_integer int_value = numeric_cast_v<mp_integer>(src);
     std::string dest=integer2string(int_value);
     dest+='L';
     return dest;
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index d34cbe72f0..da39212246 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -210,12 +210,8 @@ const exprt java_bytecode_convert_methodt::variable(
   size_t address,
   java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
 {
-  mp_integer number;
-  bool ret=to_integer(to_constant_expr(arg), number);
-  CHECK_RETURN(!ret);
-
-  std::size_t number_int=integer2size_t(number);
   typet t=java_type_from_char(type_char);
+  const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
   variablest &var_list=variables[number_int];
 
   // search variable in list for correct frame / address if necessary
@@ -1332,9 +1328,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="goto" || statement=="goto_w")
     {
       PRECONDITION(op.empty() && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "goto argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
     }
@@ -1342,9 +1336,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     {
       // As 'goto', except we must also push the subroutine return address:
       PRECONDITION(op.empty() && results.size() == 1);
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "jsr argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
       results[0]=
@@ -1386,9 +1378,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("if_?cmp??"))
     {
       PRECONDITION(op.size() == 2 && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "if_?cmp?? argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       c = convert_if_cmp(
         address_map, statement, op, number, i_it->source_location);
     }
@@ -1405,25 +1395,19 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
 
       INVARIANT(!id.empty(), "unexpected bytecode-if");
       PRECONDITION(op.size() == 1 && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "if?? argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       c = convert_if(address_map, op, id, number, i_it->source_location);
     }
     else if(statement==patternt("ifnonnull"))
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "ifnonnull argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       c = convert_ifnonull(address_map, op, number, i_it->source_location);
     }
     else if(statement==patternt("ifnull"))
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg0), number);
-      INVARIANT(!ret, "ifnull argument should be an integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       c = convert_ifnull(address_map, op, number, i_it->source_location);
     }
     else if(statement=="iinc")
@@ -1620,10 +1604,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     {
       // The first argument is the type, the second argument is the number of
       // dimensions.  The size of each dimension is on the stack.
-      mp_integer number;
-      bool ret=to_integer(to_constant_expr(arg1), number);
-      INVARIANT(!ret, "multianewarray argument should be an integer");
-      std::size_t dimension=integer2size_t(number);
+      const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);
 
       op=pop(dimension);
       assert(results.size()==1);
@@ -1954,9 +1935,7 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
       code_switch_caset code_case;
       code_case.add_source_location() = location;
 
-      mp_integer number;
-      bool ret = to_integer(to_constant_expr(*a_it), number);
-      DATA_INVARIANT(!ret, "case label expected to be integer");
+      const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
       // The switch case does not contain any code, it just branches via a GOTO
       // to the jump target of the tableswitch/lookupswitch case at
       // hand. Therefore we consider this code to belong to the source bytecode
@@ -2074,9 +2053,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
     ieee_floatt value(spec);
     if(arg0.type().id() != ID_floatbv)
     {
-      mp_integer number;
-      bool ret = to_integer(to_constant_expr(arg0), number);
-      DATA_INVARIANT(!ret, "failed to convert constant");
+      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
       value.from_integer(number);
     }
     else
@@ -2086,9 +2063,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
   }
   else
   {
-    mp_integer value;
-    bool ret = to_integer(to_constant_expr(arg0), value);
-    DATA_INVARIANT(!ret, "failed to convert constant");
+    const mp_integer value = numeric_cast_v<mp_integer>(arg0);
     const typet type = java_type_from_char(statement[0]);
     results[0] = from_integer(value, type);
   }
diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
index 094d6850c9..96234f7511 100644
--- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -90,9 +90,7 @@ refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
 /// \return the corresponding index set
 std::set<exprt> full_index_set(const array_string_exprt &s)
 {
-  PRECONDITION(s.length().is_constant());
-  mp_integer n;
-  to_integer(s.length(), n);
+  const mp_integer n = numeric_cast_v<mp_integer>(s.length());
   std::set<exprt> ret;
   for(mp_integer i=0; i<n; ++i)
     ret.insert(from_integer(i));
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 94e7facdbd..6ab842f3b0 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1110,13 +1110,9 @@ void goto_checkt::bounds_check(
     }
     else
     {
-      mp_integer i;
+      const auto i = numeric_cast<mp_integer>(index);
 
-      if(!to_integer(index, i) && i>=0)
-      {
-        // ok
-      }
-      else
+      if(!i.has_value() || *i < 0)
       {
         exprt effective_offset=ode.offset();
 
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 6beadef879..21b36dc2d1 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -181,18 +181,15 @@ void rw_range_sett::get_objects_shift(
 
   range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
 
-  mp_integer dist;
-  if(range_start==-1 ||
-     size==-1 ||
-     src_size==-1 ||
-     to_integer(simp_distance, dist))
+  const auto dist = numeric_cast<mp_integer>(simp_distance);
+  if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
   {
     get_objects_rec(mode, shift.op(), -1, -1);
     get_objects_rec(mode, shift.distance(), -1, -1);
   }
   else
   {
-    range_spect dist_r=to_range_spect(dist);
+    const range_spect dist_r = to_range_spect(*dist);
 
     // not sure whether to worry about
     // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
@@ -284,22 +281,17 @@ void rw_range_sett::get_objects_index(
 
   const exprt simp_index=simplify_expr(expr.index(), ns);
 
-  mp_integer index;
-  if(to_integer(simp_index, index))
-  {
+  const auto index = numeric_cast<mp_integer>(simp_index);
+  if(!index.has_value())
     get_objects_rec(get_modet::READ, expr.index());
-    index=-1;
-  }
 
-  if(range_start==-1 ||
-     sub_size==-1 ||
-     index==-1)
+  if(range_start == -1 || sub_size == -1 || !index.has_value())
     get_objects_rec(mode, expr.array(), -1, size);
   else
     get_objects_rec(
       mode,
       expr.array(),
-      range_start+to_range_spect(index*sub_size),
+      range_start + to_range_spect(*index * sub_size),
       size);
 }
 
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index efa128fbbb..088f603370 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -254,8 +254,7 @@ void interval_domaint::assume_rec(
 
     if(is_int(lhs.type()) && is_int(rhs.type()))
     {
-      mp_integer tmp;
-      to_integer(rhs, tmp);
+      mp_integer tmp = numeric_cast_v<mp_integer>(rhs);
       if(id==ID_lt)
         --tmp;
       integer_intervalt &ii=int_map[lhs_identifier];
@@ -280,8 +279,7 @@ void interval_domaint::assume_rec(
 
     if(is_int(lhs.type()) && is_int(rhs.type()))
     {
-      mp_integer tmp;
-      to_integer(lhs, tmp);
+      mp_integer tmp = numeric_cast_v<mp_integer>(lhs);
       if(id==ID_lt)
         ++tmp;
       integer_intervalt &ii=int_map[rhs_identifier];
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index 59bf88ca8e..a25e0c27c7 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -123,10 +123,9 @@ std::string inv_object_storet::build_string(const exprt &expr) const
       if(expr.get(ID_value)==ID_NULL)
         return "0";
 
-    mp_integer i;
-
-    if(!to_integer(expr, i))
-      return integer2string(i);
+    const auto i = numeric_cast<mp_integer>(expr);
+    if(i.has_value())
+      return integer2string(*i);
   }
 
   // we also like "address_of" and "reference_to"
@@ -455,25 +454,24 @@ void invariant_sett::strengthen_rec(const exprt &expr)
        get_object(expr.op1(), p.second))
       return;
 
-    mp_integer i0, i1;
-    bool have_i0=!to_integer(expr.op0(), i0);
-    bool have_i1=!to_integer(expr.op1(), i1);
+    const auto i0 = numeric_cast<mp_integer>(expr.op0());
+    const auto i1 = numeric_cast<mp_integer>(expr.op1());
 
     if(expr.id()==ID_le)
     {
-      if(have_i0)
-        add_bounds(p.second, lower_interval(i0));
-      else if(have_i1)
-        add_bounds(p.first, upper_interval(i1));
+      if(i0.has_value())
+        add_bounds(p.second, lower_interval(*i0));
+      else if(i1.has_value())
+        add_bounds(p.first, upper_interval(*i1));
       else
         add_le(p);
     }
     else if(expr.id()==ID_lt)
     {
-      if(have_i0)
-        add_bounds(p.second, lower_interval(i0+1));
-      else if(have_i1)
-        add_bounds(p.first, upper_interval(i1-1));
+      if(i0.has_value())
+        add_bounds(p.second, lower_interval(*i0 + 1));
+      else if(i1.has_value())
+        add_bounds(p.first, upper_interval(*i1 - 1));
       else
       {
         add_le(p);
@@ -553,12 +551,12 @@ void invariant_sett::strengthen_rec(const exprt &expr)
        get_object(expr.op1(), p.second))
       return;
 
-    mp_integer i;
-
-    if(!to_integer(expr.op0(), i))
-      add_bounds(p.second, boundst(i));
-    else if(!to_integer(expr.op1(), i))
-      add_bounds(p.first, boundst(i));
+    const auto i0 = numeric_cast<mp_integer>(expr.op0());
+    const auto i1 = numeric_cast<mp_integer>(expr.op1());
+    if(i0.has_value())
+      add_bounds(p.second, boundst(*i0));
+    else if(i1.has_value())
+      add_bounds(p.first, boundst(*i1));
 
     s=p;
     std::swap(s.first, s.second);
@@ -685,10 +683,10 @@ void invariant_sett::get_bounds(unsigned a, boundst &bounds) const
 
   {
     const exprt &e_a=object_store->get_expr(a);
-    mp_integer tmp;
-    if(!to_integer(e_a, tmp))
+    const auto tmp = numeric_cast<mp_integer>(e_a);
+    if(tmp.has_value())
     {
-      bounds=boundst(tmp);
+      bounds = boundst(*tmp);
       return;
     }
 
@@ -858,8 +856,7 @@ exprt invariant_sett::get_constant(const exprt &expr) const
 
         if(e.is_constant())
         {
-          mp_integer value;
-          assert(!to_integer(e, value));
+          const mp_integer value = numeric_cast_v<mp_integer>(e);
 
           if(expr.type().id()==ID_pointer)
           {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 59dc8197ce..38ecec5304 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -618,9 +618,7 @@ std::string expr2ct::convert_rec(
   {
     const vector_typet &vector_type=to_vector_type(src);
 
-    mp_integer size_int;
-    to_integer(vector_type.size(), size_int);
-
+    const mp_integer size_int = numeric_cast_v<mp_integer>(vector_type.size());
     std::string dest="__gcc_v"+integer2string(size_int);
 
     std::string tmp=convert(vector_type.subtype());
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index a43d16630d..20dfd6563e 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -225,10 +225,7 @@ void cpp_typecheckt::zero_initializer(
     if(size_expr.id()==ID_infinity)
       return; // don't initialize
 
-    mp_integer size;
-
-    bool to_int=to_integer(size_expr, size);
-    CHECK_RETURN(!to_int);
+    const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
     CHECK_RETURN(size>=0);
 
     exprt::operandst empty_operands;
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index e10b5a1497..a9b797a6e3 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -203,13 +203,13 @@ std::string trace_numeric_value(
     }
     else if(type.id()==ID_integer)
     {
-      mp_integer i;
-      if(!to_integer(expr, i) && i>=0)
+      const auto i = numeric_cast<mp_integer>(expr);
+      if(i.has_value() && *i >= 0)
       {
         if(options.hex_representation)
-          return "0x" + integer2string(i, 16);
+          return "0x" + integer2string(*i, 16);
         else
-          return "0b" + integer2string(i, 2);
+          return "0b" + integer2string(*i, 2);
       }
     }
   }
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 63324cd5d3..b698bbf18a 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -497,7 +497,7 @@ exprt interpretert::get_value(
     }
     else
     {
-      to_integer(size_expr, count);
+      count = numeric_cast_v<mp_integer>(size_expr);
     }
 
     // Retrieve the value for each member in the array
@@ -564,7 +564,7 @@ exprt interpretert::get_value(
     }
     else
     {
-      to_integer(size_expr, count);
+      count = numeric_cast_v<mp_integer>(size_expr);
     }
 
     // Retrieve the value for each member in the array
@@ -1023,9 +1023,7 @@ mp_integer interpretert::get_size(const typet &type)
       // Go via the binary representation to reproduce any
       // overflow behaviour.
       exprt size_const=from_integer(i[0], size_expr.type());
-      mp_integer size_mp;
-      bool ret=to_integer(size_const, size_mp);
-      CHECK_RETURN(!ret);
+      const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
       return subtype_size*size_mp;
     }
     return subtype_size;
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 790a457df0..a133646b1c 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -408,10 +408,9 @@ void interpretert::evaluate(
     }
     else
     {
-      mp_integer i;
-      if(!to_integer(expr, i))
+      if(const auto i = numeric_cast<mp_integer>(expr))
       {
-        dest.push_back(i);
+        dest.push_back(*i);
         return;
       }
     }
diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp
index a0802876c7..ee8da28558 100644
--- a/src/goto-programs/remove_vector.cpp
+++ b/src/goto-programs/remove_vector.cpp
@@ -91,8 +91,8 @@ static void remove_vector(exprt &expr)
       remove_vector(expr.type());
       array_typet array_type=to_array_type(expr.type());
 
-      mp_integer dimension;
-      to_integer(array_type.size(), dimension);
+      const mp_integer dimension =
+        numeric_cast_v<mp_integer>(array_type.size());
 
       const typet subtype=array_type.subtype();
       // do component-wise:
@@ -118,8 +118,8 @@ static void remove_vector(exprt &expr)
       remove_vector(expr.type());
       array_typet array_type=to_array_type(expr.type());
 
-      mp_integer dimension;
-      to_integer(array_type.size(), dimension);
+      const mp_integer dimension =
+        numeric_cast_v<mp_integer>(array_type.size());
 
       const typet subtype=array_type.subtype();
       // do component-wise:
diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp
index 1e3dfd5555..63f0acb884 100644
--- a/src/solvers/flattening/boolbv_quantifier.cpp
+++ b/src/solvers/flattening/boolbv_quantifier.cpp
@@ -96,8 +96,7 @@ exprt get_quantifier_var_max(
       if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
       {
         exprt over_expr=x.op1();
-        mp_integer over_i;
-        to_integer(over_expr, over_i);
+        mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
         /**
          * Due to the ''simplify'',
          * the ''over_i'' value we obtain here is not the exact
@@ -125,8 +124,7 @@ exprt get_quantifier_var_max(
       if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
       {
         exprt over_expr=y.op1();
-        mp_integer over_i;
-        to_integer(over_expr, over_i);
+        mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
         over_i-=1;
         res=from_integer(over_i, y.op1().type());
         return res;
diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp
index bb608721f5..f807affffa 100644
--- a/src/solvers/flattening/boolbv_update.cpp
+++ b/src/solvers/flattening/boolbv_update.cpp
@@ -84,13 +84,11 @@ void boolbvt::convert_update_rec(
     std::size_t element_size=boolbv_width(subtype);
 
     // iterate over array
-    mp_integer size;
-    if(to_integer(array_type.size(), size))
-      throw "update: failed to get array size";
+    const std::size_t size = numeric_cast_v<std::size_t>(array_type.size());
 
     bvt tmp_bv=bv;
 
-    for(std::size_t i=0; i!=integer2size_t(size); ++i)
+    for(std::size_t i = 0; i != size; ++i)
     {
       std::size_t new_offset=offset+i*element_size;
 
diff --git a/src/solvers/qbf/qdimacs_core.cpp b/src/solvers/qbf/qdimacs_core.cpp
index c46d06729f..8c06d048ec 100644
--- a/src/solvers/qbf/qdimacs_core.cpp
+++ b/src/solvers/qbf/qdimacs_core.cpp
@@ -31,6 +31,8 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
       }
     }
 
+    // clang-format off
+    // this is unmaintained code, don't try to reformat it
     for(used_bits_mapt::const_iterator it=used_bits_map.begin();
         it!=used_bits_map.end();
         it++)
@@ -58,9 +60,8 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
             if(oit->op0().get(ID_identifier)==ident)
             {
               const exprt &val_expr=oit->op1();
-              mp_integer value;
-              to_integer(val_expr, value);
-              value_string[value.to_ulong()]='1';
+              const std::size_t value = numeric_cast_v<std::size_t>(val_expr);
+              value_string[value]='1';
 
               #if 0
               std::cout << "[" << value << "]=1\n";
@@ -94,5 +95,6 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
       }
       #endif
     }
+    // clang-format on
   }
 }
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 0dc3673be3..873aeeb22f 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -185,11 +185,11 @@ void bv_refinementt::check_SAT(approximationt &a)
     o1.unpack(a.op1_value);
 
     // get actual rounding mode
-    mp_integer rounding_mode_int;
     exprt rounding_mode_expr = get(a.expr.op2());
-    to_integer(rounding_mode_expr, rounding_mode_int);
+    const std::size_t rounding_mode_int =
+      numeric_cast_v<std::size_t>(rounding_mode_expr);
     ieee_floatt::rounding_modet rounding_mode =
-      (ieee_floatt::rounding_modet)integer2ulong(rounding_mode_int);
+      (ieee_floatt::rounding_modet)rounding_mode_int;
 
     ieee_floatt result=o0;
     o0.rounding_mode=rounding_mode;
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index b2ed428b03..bc8b22b61f 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1525,10 +1525,7 @@ exprt simplify_exprt::bits2expr(
   {
     const array_typet &array_type=to_array_type(type);
 
-    mp_integer size;
-    if(to_integer(array_type.size(), size))
-      UNREACHABLE;
-    std::size_t n_el=integer2size_t(size);
+    const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.size());
 
     const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns);
     CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index df5deccfd4..d85299c6b9 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -31,8 +31,7 @@ bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
   {
     auto bits_per_byte = expr.get_bits_per_byte();
     std::size_t width=to_bitvector_type(expr.type()).get_width();
-    mp_integer value;
-    to_integer(expr.op(), value);
+    const mp_integer value = numeric_cast_v<mp_integer>(expr.op());
     std::vector<mp_integer> bytes;
 
     // take apart
@@ -1788,8 +1787,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
       if(changed)
       {
         // adjust constant
-        mp_integer i;
-        to_integer(expr.op1(), i);
+        mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
         i-=constant;
         expr.op1()=from_integer(i, expr.op1().type());
 
diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp
index 4409934e8b..ce3b2527f5 100644
--- a/src/util/ssa_expr.cpp
+++ b/src/util/ssa_expr.cpp
@@ -35,10 +35,7 @@ static void build_ssa_identifier_rec(
 
     build_ssa_identifier_rec(index.array(), l0, l1, l2, os, l1_object_os);
 
-    mp_integer idx;
-    if(to_integer(to_constant_expr(index.index()), idx))
-      UNREACHABLE;
-
+    const mp_integer idx = numeric_cast_v<mp_integer>(index.index());
     os << '[' << idx << ']';
   }
   else if(expr.id()==ID_symbol)
diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp
index b320f85fc4..28fae345e1 100644
--- a/src/util/xml_expr.cpp
+++ b/src/util/xml_expr.cpp
@@ -247,8 +247,7 @@ xmlt xml(
       result.name="integer";
       result.set_attribute("c_type", "_Bool");
       result.set_attribute("binary", expr.get_string(ID_value));
-      mp_integer b;
-      to_integer(to_constant_expr(expr), b);
+      const mp_integer b = numeric_cast_v<mp_integer>(expr);
       result.data=integer2string(b);
     }
     else
diff --git a/unit/testing-utils/require_expr.cpp b/unit/testing-utils/require_expr.cpp
index 9f242400a9..dafd866c7b 100644
--- a/unit/testing-utils/require_expr.cpp
+++ b/unit/testing-utils/require_expr.cpp
@@ -28,9 +28,8 @@ index_exprt require_expr::require_index(const exprt &expr, int expected_index)
   REQUIRE(expr.id()==ID_index);
   const index_exprt &index_expr=to_index_expr(expr);
   REQUIRE(index_expr.index().id()==ID_constant);
-  const constant_exprt &index_value=to_constant_expr(index_expr.index());
-  mp_integer index_integer_value;
-  to_integer(index_value, index_integer_value);
+  const mp_integer index_integer_value =
+    numeric_cast_v<mp_integer>(index_expr.index());
   REQUIRE(index_integer_value==expected_index);
 
   return index_expr;
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 8f75262f44..aea95b5bc3 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -36,8 +36,7 @@ TEST_CASE("Simplify pointer_offset(address of array index)")
   exprt simp=simplify_expr(p_o, ns);
 
   REQUIRE(simp.id()==ID_constant);
-  mp_integer offset_value;
-  REQUIRE(!to_integer(simp, offset_value));
+  const mp_integer offset_value = numeric_cast_v<mp_integer>(simp);
   REQUIRE(offset_value==1);
 }
 
@@ -57,8 +56,7 @@ TEST_CASE("Simplify const pointer offset")
   exprt simp=simplify_expr(p_o, ns);
 
   REQUIRE(simp.id()==ID_constant);
-  mp_integer offset_value;
-  REQUIRE(!to_integer(simp, offset_value));
+  const mp_integer offset_value = numeric_cast_v<mp_integer>(simp);
   REQUIRE(offset_value==1234);
 }