diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
index 76417570344..b8907be9a10 100644
--- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -86,7 +86,8 @@ static const std::string get_thread_block_identifier(
 {
   PRECONDITION(f_code.arguments().size() == 1);
   const exprt &expr = f_code.arguments()[0];
-  const mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());
+  const mp_integer lbl_id =
+    numeric_cast_v<mp_integer>(to_constant_expr(expr.op0()));
   return integer2string(lbl_id);
 }
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 4c375214507..dd1f4d131f2 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -183,7 +183,8 @@ exprt java_bytecode_convert_methodt::variable(
   java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
 {
   typet t=java_type_from_char(type_char);
-  const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
+  const std::size_t number_int =
+    numeric_cast_v<std::size_t>(to_constant_expr(arg));
   variablest &var_list=variables[number_int];
 
   // search variable in list for correct frame / address if necessary
@@ -1309,7 +1310,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="goto" || statement=="goto_w")
     {
       PRECONDITION(op.empty() && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
     }
@@ -1317,7 +1319,8 @@ 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);
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       code_gotot code_goto(label(integer2string(number)));
       c=code_goto;
       results[0]=
@@ -1344,7 +1347,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("?const"))
     {
       assert(results.size()==1);
-      results = convert_const(statement, arg0, results);
+      results = convert_const(statement, to_constant_expr(arg0), results);
     }
     else if(statement==patternt("?ipush"))
     {
@@ -1357,7 +1360,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("if_?cmp??"))
     {
       PRECONDITION(op.size() == 2 && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       c = convert_if_cmp(
         address_map, statement, op, number, i_it->source_location);
     }
@@ -1374,19 +1378,22 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
 
       INVARIANT(!id.empty(), "unexpected bytecode-if");
       PRECONDITION(op.size() == 1 && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       c = convert_if(address_map, op, id, number, i_it->source_location);
     }
     else if(statement==patternt("ifnonnull"))
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       c = convert_ifnonull(address_map, op, number, i_it->source_location);
     }
     else if(statement==patternt("ifnull"))
     {
       PRECONDITION(op.size() == 1 && results.empty());
-      const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(arg0));
       c = convert_ifnull(address_map, op, number, i_it->source_location);
     }
     else if(statement=="iinc")
@@ -1581,7 +1588,8 @@ 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.
-      const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);
+      const std::size_t dimension =
+        numeric_cast_v<std::size_t>(to_constant_expr(arg1));
 
       op=pop(dimension);
       assert(results.size()==1);
@@ -1905,7 +1913,8 @@ code_switcht java_bytecode_convert_methodt::convert_switch(
   {
     if(is_label)
     {
-      const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
+      const mp_integer number =
+        numeric_cast_v<mp_integer>(to_constant_expr(*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
@@ -2014,7 +2023,7 @@ void java_bytecode_convert_methodt::convert_dup2_x2(
 
 exprt::operandst &java_bytecode_convert_methodt::convert_const(
   const irep_idt &statement,
-  const exprt &arg0,
+  const constant_exprt &arg0,
   exprt::operandst &results) const
 {
   const char type_char = statement[0];
@@ -2034,7 +2043,7 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
       value.from_integer(number);
     }
     else
-      value.from_expr(to_constant_expr(arg0));
+      value.from_expr(arg0);
 
     results[0] = value.to_expr();
   }
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
index b8f105fc94c..fab0ff46b42 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -487,7 +487,7 @@ class java_bytecode_convert_methodt:public messaget
 
   exprt::operandst &convert_const(
     const irep_idt &statement,
-    const exprt &arg0,
+    const constant_exprt &arg0,
     exprt::operandst &results) const;
 
   void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results);
diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
index 2bb317164ac..253f23c5133 100644
--- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -99,7 +99,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)
 {
-  const mp_integer n = numeric_cast_v<mp_integer>(s.length());
+  const mp_integer n = numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
   std::set<exprt> ret;
   for(mp_integer i = 0; i < n; ++i)
     ret.insert(from_integer(i));
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index cdcabad3562..cafeb03cf3a 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -254,7 +254,7 @@ void interval_domaint::assume_rec(
 
     if(is_int(lhs.type()) && is_int(rhs.type()))
     {
-      mp_integer tmp = numeric_cast_v<mp_integer>(rhs);
+      mp_integer tmp = numeric_cast_v<mp_integer>(to_constant_expr(rhs));
       if(id==ID_lt)
         --tmp;
       integer_intervalt &ii=int_map[lhs_identifier];
@@ -279,7 +279,7 @@ void interval_domaint::assume_rec(
 
     if(is_int(lhs.type()) && is_int(rhs.type()))
     {
-      mp_integer tmp = numeric_cast_v<mp_integer>(lhs);
+      mp_integer tmp = numeric_cast_v<mp_integer>(to_constant_expr(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 11d76f0e057..9714093f653 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -850,7 +850,8 @@ exprt invariant_sett::get_constant(const exprt &expr) const
 
         if(e.is_constant())
         {
-          const mp_integer value = numeric_cast_v<mp_integer>(e);
+          const mp_integer value =
+            numeric_cast_v<mp_integer>(to_constant_expr(e));
 
           if(expr.type().id()==ID_pointer)
           {
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 1456aa0043e..b1a292d36ff 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -155,7 +155,9 @@ void symbol_factoryt::gen_nondet_array_init(
   const recursion_sett &recursion_set)
 {
   auto const &array_type = to_array_type(expr.type());
-  auto const array_size = numeric_cast_v<size_t>(array_type.size());
+  const auto &size = array_type.size();
+  PRECONDITION(size.id() == ID_constant);
+  auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size));
   DATA_INVARIANT(array_size > 0, "Arrays should have positive size");
   for(size_t index = 0; index < array_size; ++index)
   {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index a20ce849331..a5caa5b4cc9 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -2172,7 +2172,7 @@ std::string expr2ct::convert_array(
       if(it==--src.operands().end())
         break;
 
-      const unsigned int ch = numeric_cast_v<unsigned>(*it);
+      const unsigned int ch = numeric_cast_v<unsigned>(to_constant_expr(*it));
 
       if(last_was_hex)
       {
diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp
index 019478408e4..0d7db92c808 100644
--- a/src/cpp/cpp_typecheck_initializer.cpp
+++ b/src/cpp/cpp_typecheck_initializer.cpp
@@ -231,7 +231,8 @@ void cpp_typecheckt::zero_initializer(
     if(size_expr.id()==ID_infinity)
       return; // don't initialize
 
-    const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
+    const mp_integer size =
+      numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
     CHECK_RETURN(size>=0);
 
     exprt::operandst empty_operands;
diff --git a/src/goto-instrument/accelerate/polynomial.cpp b/src/goto-instrument/accelerate/polynomial.cpp
index 5f9c7a09d8f..5df1999a120 100644
--- a/src/goto-instrument/accelerate/polynomial.cpp
+++ b/src/goto-instrument/accelerate/polynomial.cpp
@@ -139,7 +139,7 @@ void polynomialt::from_expr(const exprt &expr)
   else if(expr.id()==ID_constant)
   {
     monomialt monomial;
-    monomial.coeff = numeric_cast_v<int>(expr);
+    monomial.coeff = numeric_cast_v<int>(to_constant_expr(expr));
 
     monomials.push_back(monomial);
   }
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 0a2bf473358..cf955bfd891 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -498,7 +498,7 @@ exprt interpretert::get_value(
     }
     else
     {
-      count = numeric_cast_v<mp_integer>(size_expr);
+      count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
     }
 
     // Retrieve the value for each member in the array
@@ -567,7 +567,7 @@ exprt interpretert::get_value(
     }
     else
     {
-      count = numeric_cast_v<mp_integer>(size_expr);
+      count = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
     }
 
     // Retrieve the value for each member in the array
@@ -1026,7 +1026,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());
+      const constant_exprt size_const = from_integer(i[0], size_expr.type());
       const mp_integer size_mp = numeric_cast_v<mp_integer>(size_const);
       return subtype_size*size_mp;
     }
diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp
index fc53f1bed9f..42b1601de06 100644
--- a/src/goto-programs/remove_vector.cpp
+++ b/src/goto-programs/remove_vector.cpp
@@ -92,7 +92,7 @@ static void remove_vector(exprt &expr)
       array_typet array_type=to_array_type(expr.type());
 
       const mp_integer dimension =
-        numeric_cast_v<mp_integer>(array_type.size());
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
       const typet subtype=array_type.subtype();
       // do component-wise:
@@ -119,7 +119,7 @@ static void remove_vector(exprt &expr)
       array_typet array_type=to_array_type(expr.type());
 
       const mp_integer dimension =
-        numeric_cast_v<mp_integer>(array_type.size());
+        numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
 
       const typet subtype=array_type.subtype();
       // do component-wise:
@@ -150,7 +150,8 @@ static void remove_vector(exprt &expr)
         // (vector-type) x ==> { x, x, ..., x }
         remove_vector(expr.type());
         array_typet array_type = to_array_type(expr.type());
-        const auto dimension = numeric_cast_v<std::size_t>(array_type.size());
+        const auto dimension =
+          numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
         exprt casted_op =
           typecast_exprt::conditional_cast(op, array_type.subtype());
         expr = array_exprt(exprt::operandst(dimension, casted_op), array_type);
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 485db078dd1..62471fce7ad 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -72,9 +72,13 @@ bool boolbvt::literal(
       std::size_t element_width=boolbv_width(index_expr.type());
       CHECK_RETURN(element_width != 0);
 
-      mp_integer index = numeric_cast_v<mp_integer>(index_expr.index());
+      const auto &index = index_expr.index();
+      PRECONDITION(index.id() == ID_constant);
+      mp_integer index_int =
+        numeric_cast_v<mp_integer>(to_constant_expr(index));
 
-      std::size_t offset = numeric_cast_v<std::size_t>(index * element_width);
+      std::size_t offset =
+        numeric_cast_v<std::size_t>(index_int * element_width);
 
       return literal(index_expr.array(), bit+offset, dest);
     }
diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp
index a5f21f48bbb..abad73b2a45 100644
--- a/src/solvers/flattening/boolbv_extractbit.cpp
+++ b/src/solvers/flattening/boolbv_extractbit.cpp
@@ -19,11 +19,13 @@ Author: Daniel Kroening, kroening@kroening.com
 literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
 {
   const bvt &src_bv = convert_bv(expr.src());
+  const auto &index = expr.index();
 
   // constant?
-  if(expr.index().is_constant())
+  if(index.is_constant())
   {
-    mp_integer index_as_integer = numeric_cast_v<mp_integer>(expr.index());
+    mp_integer index_as_integer =
+      numeric_cast_v<mp_integer>(to_constant_expr(index));
 
     if(index_as_integer < 0 || index_as_integer >= src_bv.size())
       return prop.new_variable(); // out of range!
@@ -42,7 +44,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
   else
   {
     std::size_t src_bv_width = boolbv_width(expr.src().type());
-    std::size_t index_bv_width = boolbv_width(expr.index().type());
+    std::size_t index_bv_width = boolbv_width(index.type());
 
     if(src_bv_width == 0 || index_bv_width == 0)
       return SUB::convert_rest(expr);
@@ -52,7 +54,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     unsignedbv_typet index_type(index_width);
 
     equal_exprt equality(
-      typecast_exprt::conditional_cast(expr.index(), index_type), exprt());
+      typecast_exprt::conditional_cast(index, index_type), exprt());
 
     if(prop.has_set_to())
     {
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index 218a65b2dd7..89916842e50 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -61,7 +61,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     }
 
     // Must have a finite size
-    mp_integer array_size = numeric_cast_v<mp_integer>(array_type.size());
+    mp_integer array_size =
+      numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+
     {
       // see if the index address is constant
       // many of these are compacted by simplify_expr
diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp
index e6fa39b16a3..487b6d921a7 100644
--- a/src/solvers/flattening/boolbv_quantifier.cpp
+++ b/src/solvers/flattening/boolbv_quantifier.cpp
@@ -87,8 +87,10 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
         continue;
       if(expr_eq(var_expr, x.op0()) && x.op1().id()==ID_constant)
       {
-        exprt over_expr=x.op1();
+        const constant_exprt &over_expr = to_constant_expr(x.op1());
+
         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
@@ -115,7 +117,7 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr)
         continue;
       if(expr_eq(var_expr, y.op0()) && y.op1().id()==ID_constant)
       {
-        exprt over_expr=y.op1();
+        const constant_exprt &over_expr = to_constant_expr(y.op1());
         mp_integer over_i = numeric_cast_v<mp_integer>(over_expr);
         over_i-=1;
         res=from_integer(over_i, y.op1().type());
@@ -149,8 +151,8 @@ instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
   if(min_i.is_false() || max_i.is_false())
     return nullopt;
 
-  mp_integer lb = numeric_cast_v<mp_integer>(min_i);
-  mp_integer ub = numeric_cast_v<mp_integer>(max_i);
+  mp_integer lb = numeric_cast_v<mp_integer>(to_constant_expr(min_i));
+  mp_integer ub = numeric_cast_v<mp_integer>(to_constant_expr(max_i));
 
   if(lb>ub)
     return nullopt;
diff --git a/src/solvers/flattening/boolbv_shift.cpp b/src/solvers/flattening/boolbv_shift.cpp
index e0559811aba..5e8971ff493 100644
--- a/src/solvers/flattening/boolbv_shift.cpp
+++ b/src/solvers/flattening/boolbv_shift.cpp
@@ -47,11 +47,12 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
   else
     UNREACHABLE;
 
-  // we allow a constant as shift distance
+  // we optimise for the special case where the shift distance
+  // is a constant
 
   if(expr.op1().is_constant())
   {
-    mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
+    mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
 
     std::size_t distance;
 
diff --git a/src/solvers/flattening/boolbv_update.cpp b/src/solvers/flattening/boolbv_update.cpp
index 2f702af036f..39684f614cb 100644
--- a/src/solvers/flattening/boolbv_update.cpp
+++ b/src/solvers/flattening/boolbv_update.cpp
@@ -74,13 +74,18 @@ void boolbvt::convert_update_rec(
     bvt index_bv=convert_bv(designator.op0());
 
     const array_typet &array_type=to_array_type(type);
-
     const typet &subtype = array_type.subtype();
+    const exprt &size_expr = array_type.size();
 
     std::size_t element_size=boolbv_width(subtype);
 
+    DATA_INVARIANT(
+      size_expr.id() == ID_constant,
+      "array in update expression should be constant-sized");
+
     // iterate over array
-    const std::size_t size = numeric_cast_v<std::size_t>(array_type.size());
+    const std::size_t size =
+      numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
 
     bvt tmp_bv=bv;
 
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 6eaf78a4b72..e32a04a35e7 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -178,7 +178,8 @@ void bv_refinementt::check_SAT(approximationt &a)
     o1.unpack(a.op1_value);
 
     // get actual rounding mode
-    exprt rounding_mode_expr = get(float_op.rounding_mode());
+    constant_exprt rounding_mode_expr =
+      to_constant_expr(get(float_op.rounding_mode()));
     const std::size_t rounding_mode_int =
       numeric_cast_v<std::size_t>(rounding_mode_expr);
     ieee_floatt::rounding_modet rounding_mode =
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index accbd0c4430..fb6ba0fca79 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -1314,7 +1314,8 @@ void smt2_convt::convert_expr(const exprt &expr)
 
       if(shift_expr.distance().type().id() == ID_integer)
       {
-        mp_integer i = numeric_cast_v<mp_integer>(shift_expr.distance());
+        const mp_integer i =
+          numeric_cast_v<mp_integer>(to_constant_expr(shift_expr.distance()));
 
         // shift distance must be bit vector
         std::size_t width_op0 = boolbv_width(shift_expr.op().type());
@@ -1450,9 +1451,10 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     const extractbit_exprt &extractbit_expr = to_extractbit_expr(expr);
 
-    if(expr.op1().is_constant())
+    if(extractbit_expr.index().is_constant())
     {
-      mp_integer i = numeric_cast_v<mp_integer>(extractbit_expr.index());
+      const mp_integer i =
+        numeric_cast_v<mp_integer>(to_constant_expr(extractbit_expr.index()));
 
       out << "(= ((_ extract " << i << " " << i << ") ";
       flatten2bv(extractbit_expr.src());
@@ -1477,8 +1479,10 @@ void smt2_convt::convert_expr(const exprt &expr)
       extractbits_expr.upper().is_constant() &&
       extractbits_expr.lower().is_constant())
     {
-      mp_integer op1_i = numeric_cast_v<mp_integer>(extractbits_expr.upper());
-      mp_integer op2_i = numeric_cast_v<mp_integer>(extractbits_expr.lower());
+      mp_integer op1_i =
+        numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.upper()));
+      mp_integer op2_i =
+        numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.lower()));
 
       if(op2_i>op1_i)
         std::swap(op1_i, op2_i);
@@ -2158,7 +2162,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       // must be constant
       if(src.is_constant())
       {
-        mp_integer i = numeric_cast_v<mp_integer>(src);
+        mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(src));
         out << "(_ bv" << i << " " << to_width << ")";
       }
       else
@@ -2663,8 +2667,10 @@ void smt2_convt::convert_struct(const struct_exprt &expr)
 void smt2_convt::flatten_array(const exprt &expr)
 {
   const array_typet &array_type = to_array_type(expr.type());
+  const auto &size_expr = array_type.size();
+  PRECONDITION(size_expr.id() == ID_constant);
 
-  mp_integer size = numeric_cast_v<mp_integer>(array_type.size());
+  mp_integer size = numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
   CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array");
 
   out << "(let ((?far ";
diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index a8a3f5ea78d..bfd8ec002e5 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -46,15 +46,15 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
 {
   if(expr.id() == ID_constant)
   {
-    const auto &value = to_constant_expr(expr).get_value();
-
+    const auto &constant_expr = to_constant_expr(expr);
+    const auto &value = constant_expr.get_value();
     const typet &expr_type = expr.type();
 
     if(expr_type.id() == ID_unsignedbv)
     {
       const std::size_t width = to_unsignedbv_type(expr_type).get_width();
 
-      const auto int_value = numeric_cast_v<mp_integer>(expr);
+      const auto int_value = numeric_cast_v<mp_integer>(constant_expr);
 
       out << "(_ bv" << int_value << " " << width << ")";
     }
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp
index 11035f7b03c..0ee6dd582f4 100644
--- a/src/solvers/strings/string_refinement.cpp
+++ b/src/solvers/strings/string_refinement.cpp
@@ -972,7 +972,7 @@ static std::string string_of_array(const array_exprt &arr)
     return std::string("");
 
   exprt size_expr = to_array_type(arr.type()).size();
-  auto n = numeric_cast_v<std::size_t>(size_expr);
+  auto n = numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
   return utf16_constant_array_to_java(arr, n);
 }
 
@@ -1203,10 +1203,10 @@ static exprt negation_of_not_contains_constraint(
   const std::function<exprt(const exprt &)> &get)
 {
   // If the for all is vacuously true, the negation is false.
-  const auto lbe =
-    numeric_cast_v<mp_integer>(get(constraint.exists_lower_bound));
-  const auto ube =
-    numeric_cast_v<mp_integer>(get(constraint.exists_upper_bound));
+  const auto lbe = numeric_cast_v<mp_integer>(
+    to_constant_expr(get(constraint.exists_lower_bound)));
+  const auto ube = numeric_cast_v<mp_integer>(
+    to_constant_expr(get(constraint.exists_upper_bound)));
   const auto univ_bounds = and_exprt(
     binary_relation_exprt(get(constraint.univ_lower_bound), ID_le, univ_var),
     binary_relation_exprt(get(constraint.univ_upper_bound), ID_gt, univ_var));
diff --git a/src/solvers/strings/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp
index 0204f66e0b5..c946859fdd4 100644
--- a/src/solvers/strings/string_refinement_util.cpp
+++ b/src/solvers/strings/string_refinement_util.cpp
@@ -62,7 +62,8 @@ sparse_arrayt::sparse_arrayt(const with_exprt &expr)
   while(can_cast_expr<with_exprt>(ref.get()))
   {
     const auto &with_expr = expr_dynamic_cast<with_exprt>(ref.get());
-    const auto current_index = numeric_cast_v<std::size_t>(with_expr.where());
+    const auto current_index =
+      numeric_cast_v<std::size_t>(to_constant_expr(with_expr.where()));
     entries[current_index] = with_expr.new_value();
     ref = with_expr.old();
   }
diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h
index f7309e27071..894d6625c92 100644
--- a/src/util/arith_tools.h
+++ b/src/util/arith_tools.h
@@ -153,7 +153,7 @@ Target numeric_cast_v(const mp_integer &arg)
 /// \param arg: constant expression
 /// \return value of type Target
 template <typename Target>
-Target numeric_cast_v(const exprt &arg)
+Target numeric_cast_v(const constant_exprt &arg)
 {
   const auto maybe = numeric_castt<Target>{}(arg);
   INVARIANT_WITH_DIAGNOSTICS(
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index b95efc2fef2..129ddcce025 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1657,8 +1657,12 @@ exprt simplify_exprt::bits2expr(
   else if(type.id()==ID_array)
   {
     const array_typet &array_type=to_array_type(type);
+    const auto &size_expr = array_type.size();
 
-    const std::size_t n_el = numeric_cast_v<std::size_t>(array_type.size());
+    PRECONDITION(size_expr.is_constant());
+
+    const std::size_t number_of_elements =
+      numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
 
     const auto el_size_opt = pointer_offset_bits(array_type.subtype(), ns);
     CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
@@ -1666,9 +1670,9 @@ exprt simplify_exprt::bits2expr(
     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);
+    result.reserve_operands(number_of_elements);
 
-    for(std::size_t i=0; i<n_el; ++i)
+    for(std::size_t i = 0; i < number_of_elements; ++i)
     {
       std::string el_bits=std::string(bits, i*el_size, el_size);
       exprt el = bits2expr(el_bits, array_type.subtype(), little_endian);
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 2cda819d3a3..1b8cb6cf777 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -32,7 +32,8 @@ 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();
-    const mp_integer value = numeric_cast_v<mp_integer>(expr.op());
+    const mp_integer value =
+      numeric_cast_v<mp_integer>(to_constant_expr(expr.op()));
     std::vector<mp_integer> bytes;
 
     // take apart
@@ -1763,8 +1764,8 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
 
       if(changed)
       {
-        // adjust constant
-        mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
+        // adjust the constant on the RHS
+        mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
         i-=constant;
         expr.op1()=from_integer(i, expr.op1().type());
 
@@ -1893,7 +1894,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     }
     else if(expr.id()==ID_gt)
     {
-      mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
+      mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
 
       if(i==max)
       {
@@ -1917,7 +1918,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     }
     else if(expr.id()==ID_le)
     {
-      mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
+      mp_integer i = numeric_cast_v<mp_integer>(to_constant_expr(expr.op1()));
 
       if(i==max)
       {
diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp
index 5e7105c8792..ccd065bb79e 100644
--- a/src/util/ssa_expr.cpp
+++ b/src/util/ssa_expr.cpp
@@ -40,7 +40,8 @@ static void build_ssa_identifier_rec(
 
     build_ssa_identifier_rec(index.array(), l0, l1, l2, os, l1_object_os);
 
-    const mp_integer idx = numeric_cast_v<mp_integer>(index.index());
+    const mp_integer idx =
+      numeric_cast_v<mp_integer>(to_constant_expr(index.index()));
     os << '[' << idx << ']';
     l1_object_os << '[' << idx << ']';
   }
diff --git a/unit/testing-utils/require_expr.cpp b/unit/testing-utils/require_expr.cpp
index 2147aeed587..57400f27b6c 100644
--- a/unit/testing-utils/require_expr.cpp
+++ b/unit/testing-utils/require_expr.cpp
@@ -29,7 +29,7 @@ index_exprt require_expr::require_index(const exprt &expr, int expected_index)
   const index_exprt &index_expr=to_index_expr(expr);
   REQUIRE(index_expr.index().id()==ID_constant);
   const mp_integer index_integer_value =
-    numeric_cast_v<mp_integer>(index_expr.index());
+    numeric_cast_v<mp_integer>(to_constant_expr(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 1c0ab7b035c..79cc704bc7e 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -37,7 +37,8 @@ TEST_CASE("Simplify pointer_offset(address of array index)")
   exprt simp=simplify_expr(p_o, ns);
 
   REQUIRE(simp.id()==ID_constant);
-  const mp_integer offset_value = numeric_cast_v<mp_integer>(simp);
+  const mp_integer offset_value =
+    numeric_cast_v<mp_integer>(to_constant_expr(simp));
   REQUIRE(offset_value==1);
 }
 
@@ -57,7 +58,8 @@ TEST_CASE("Simplify const pointer offset")
   exprt simp=simplify_expr(p_o, ns);
 
   REQUIRE(simp.id()==ID_constant);
-  const mp_integer offset_value = numeric_cast_v<mp_integer>(simp);
+  const mp_integer offset_value =
+    numeric_cast_v<mp_integer>(to_constant_expr(simp));
   REQUIRE(offset_value==1234);
 }