From 638d91c5b94081bfb0293a5b6f7a6fd127cac56c Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 31 Oct 2018 21:19:26 +0000
Subject: [PATCH] Use numeric_cast<mp_integer> instead of deprecated
 to_integer(exprt)

This reduces the number of warnings flagged, in particular in Visual-Studio
builds. Also turn tests of the size of ID_vector types being constants into
invariants as was already done in some places.
---
 src/ansi-c/padding.cpp                        | 26 +++---
 src/ansi-c/type2name.cpp                      | 19 ++--
 src/cpp/cpp_typecheck_constructor.cpp         | 10 +--
 src/goto-symex/build_goto_trace.cpp           |  6 +-
 src/solvers/flattening/boolbv.cpp             |  8 +-
 src/solvers/flattening/boolbv_byte_update.cpp |  6 +-
 src/solvers/flattening/boolbv_extractbit.cpp  |  2 +-
 src/solvers/flattening/boolbv_width.cpp       | 24 ++---
 src/solvers/flattening/boolbv_with.cpp        |  8 +-
 src/util/endianness_map.cpp                   | 14 ++-
 src/util/expr_initializer.cpp                 | 23 ++---
 src/util/pointer_offset_size.cpp              | 77 +++++++---------
 src/util/simplify_expr.cpp                    | 87 +++++++++----------
 src/util/simplify_expr_array.cpp              | 17 ++--
 14 files changed, 154 insertions(+), 173 deletions(-)

diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index d0180334e50..1df5ac652fa 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -35,12 +35,15 @@ mp_integer alignment(const typet &type, const namespacet &ns)
   const exprt &given_alignment=
     static_cast<const exprt &>(type.find(ID_C_alignment));
 
-  mp_integer a_int;
+  mp_integer a_int = 0;
 
   // we trust it blindly, no matter how nonsensical
-  if(given_alignment.is_nil() ||
-     to_integer(given_alignment, a_int))
-    a_int=0;
+  if(given_alignment.is_not_nil())
+  {
+    const auto a = numeric_cast<mp_integer>(given_alignment);
+    if(a.has_value())
+      a_int = *a;
+  }
 
   // alignment but no packing
   if(a_int>0 && !type.get_bool(ID_C_packed))
@@ -402,17 +405,16 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
   }
 
   // any explicit alignment for the struct?
-  if(type.find(ID_C_alignment).is_not_nil())
+  const exprt &alignment =
+    static_cast<const exprt &>(type.find(ID_C_alignment));
+  if(alignment.is_not_nil())
   {
-    const exprt &alignment=
-      static_cast<const exprt &>(type.find(ID_C_alignment));
     if(alignment.id()!=ID_default)
     {
-      exprt tmp=alignment;
-      simplify(tmp, ns);
-      mp_integer tmp_i;
-      if(!to_integer(tmp, tmp_i) && tmp_i>max_alignment)
-        max_alignment=tmp_i;
+      const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));
+
+      if(tmp_i.has_value() && *tmp_i > max_alignment)
+        max_alignment = *tmp_i;
     }
   }
   // Is the struct packed, without any alignment specification?
diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
index 57b23492753..18b8bf692e1 100644
--- a/src/ansi-c/type2name.cpp
+++ b/src/ansi-c/type2name.cpp
@@ -178,14 +178,19 @@ static std::string type2name(
   }
   else if(type.id()==ID_array)
   {
-    const array_typet &t=to_array_type(type);
-    mp_integer size;
-    if(t.size().id()==ID_symbol)
-      result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
-    else if(to_integer(t.size(), size))
-      result+="ARR?";
+    const exprt &size = to_array_type(type).size();
+
+    if(size.id() == ID_symbol)
+      result += "ARR" + id2string(to_symbol_expr(size).get_identifier());
     else
-      result+="ARR"+integer2string(size);
+    {
+      const auto size_int = numeric_cast<mp_integer>(size);
+
+      if(!size_int.has_value())
+        result += "ARR?";
+      else
+        result += "ARR" + integer2string(*size_int);
+    }
   }
   else if(
     type.id() == ID_symbol_type || type.id() == ID_c_enum_tag ||
diff --git a/src/cpp/cpp_typecheck_constructor.cpp b/src/cpp/cpp_typecheck_constructor.cpp
index 4932f09e8f5..fa3752b22d7 100644
--- a/src/cpp/cpp_typecheck_constructor.cpp
+++ b/src/cpp/cpp_typecheck_constructor.cpp
@@ -395,13 +395,11 @@ void cpp_typecheckt::default_assignop_value(
         continue;
       }
 
-      mp_integer size;
-      bool to_int=to_integer(size_expr, size);
-      CHECK_RETURN(!to_int);
-      CHECK_RETURN(size>=0);
+      const auto size = numeric_cast<mp_integer>(size_expr);
+      CHECK_RETURN(!size.has_value());
+      CHECK_RETURN(*size >= 0);
 
-      exprt::operandst empty_operands;
-      for(mp_integer i=0; i < size; ++i)
+      for(mp_integer i = 0; i < *size; ++i)
         copy_array(source_location, mem_name, i, arg_name, block);
     }
     else
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
index e09f79ac778..65a6bb2f38b 100644
--- a/src/goto-symex/build_goto_trace.cpp
+++ b/src/goto-symex/build_goto_trace.cpp
@@ -228,7 +228,11 @@ void build_goto_trace(
         exprt clock_value=prop_conv.get(
           symbol_exprt(partial_order_concurrencyt::rw_clock_id(it)));
 
-        to_integer(clock_value, current_time);
+        const auto cv = numeric_cast<mp_integer>(clock_value);
+        if(cv.has_value())
+          current_time = *cv;
+        else
+          current_time = 0;
       }
       else if(it->is_atomic_end() && current_time<0)
         current_time*=-1;
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index fdaaaa16ccd..eb82d4c1803 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -323,9 +323,9 @@ bvt boolbvt::convert_lambda(const exprt &expr)
   const exprt &array_size=
     to_array_type(expr.type()).size();
 
-  mp_integer size;
+  const auto size = numeric_cast<mp_integer>(array_size);
 
-  if(to_integer(array_size, size))
+  if(!size.has_value())
     return conversion_failed(expr);
 
   typet counter_type=expr.op0().type();
@@ -333,7 +333,7 @@ bvt boolbvt::convert_lambda(const exprt &expr)
   bvt bv;
   bv.resize(width);
 
-  for(mp_integer i=0; i<size; ++i)
+  for(mp_integer i = 0; i < *size; ++i)
   {
     exprt counter=from_integer(i, counter_type);
 
@@ -343,7 +343,7 @@ bvt boolbvt::convert_lambda(const exprt &expr)
     const bvt &tmp=convert_bv(expr_op1);
 
     INVARIANT(
-      size * tmp.size() == width,
+      *size * tmp.size() == width,
       "total bitvector width shall equal the number of operands times the size "
       "per operand");
 
diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp
index 024128f1a79..0ccca1d2a11 100644
--- a/src/solvers/flattening/boolbv_byte_update.cpp
+++ b/src/solvers/flattening/boolbv_byte_update.cpp
@@ -38,11 +38,11 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 
   // see if the byte number is constant
 
-  mp_integer index;
-  if(!to_integer(offset_expr, index))
+  const auto index = numeric_cast<mp_integer>(offset_expr);
+  if(index.has_value())
   {
     // yes!
-    mp_integer offset=index*8;
+    const mp_integer offset = *index * 8;
 
     if(offset+update_width>mp_integer(bv.size()) || offset<0)
     {
diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp
index ce4637340fe..f29d7c548b0 100644
--- a/src/solvers/flattening/boolbv_extractbit.cpp
+++ b/src/solvers/flattening/boolbv_extractbit.cpp
@@ -28,7 +28,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     if(index_as_integer < 0 || index_as_integer >= src_bv.size())
       return prop.new_variable(); // out of range!
     else
-      return src_bv[integer2size_t(index_as_integer)];
+      return src_bv[numeric_cast_v<std::size_t>(index_as_integer)];
   }
 
   if(
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 144387cfa19..e9a43229175 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -128,16 +128,16 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     const array_typet &array_type=to_array_type(type);
     std::size_t sub_width=operator()(array_type.subtype());
 
-    mp_integer array_size;
+    const auto array_size = numeric_cast<mp_integer>(array_type.size());
 
-    if(to_integer(array_type.size(), array_size))
+    if(!array_size.has_value())
     {
       // we can still use the theory of arrays for this
       entry.total_width=0;
     }
     else
     {
-      mp_integer total=array_size*sub_width;
+      mp_integer total = *array_size * sub_width;
       if(total>(1<<30)) // realistic limit
         throw analysis_exceptiont("array too large for flattening");
 
@@ -149,21 +149,13 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     const vector_typet &vector_type=to_vector_type(type);
     std::size_t sub_width=operator()(vector_type.subtype());
 
-    mp_integer vector_size;
+    const auto vector_size = numeric_cast_v<mp_integer>(vector_type.size());
 
-    if(to_integer(vector_type.size(), vector_size))
-    {
-      // we can still use the theory of arrays for this
-      entry.total_width=0;
-    }
-    else
-    {
-      mp_integer total=vector_size*sub_width;
-      if(total>(1<<30)) // realistic limit
-        analysis_exceptiont("vector too large for flattening");
+    mp_integer total = vector_size * sub_width;
+    if(total > (1 << 30)) // realistic limit
+      analysis_exceptiont("vector too large for flattening");
 
-      entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
-    }
+    entry.total_width = numeric_cast_v<std::size_t>(vector_size * sub_width);
   }
   else if(type_id==ID_complex)
   {
diff --git a/src/solvers/flattening/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp
index f8613af41eb..093c76ccd5f 100644
--- a/src/solvers/flattening/boolbv_with.cpp
+++ b/src/solvers/flattening/boolbv_with.cpp
@@ -125,9 +125,9 @@ void boolbvt::convert_with_array(
 
   const exprt &array_size=type.size();
 
-  mp_integer size;
+  const auto size = numeric_cast<mp_integer>(array_size);
 
-  if(to_integer(array_size, size))
+  if(!size.has_value())
   {
     error().source_location=type.source_location();
     error() << "convert_with_array expects constant array size" << eom;
@@ -136,7 +136,7 @@ void boolbvt::convert_with_array(
 
   const bvt &op2_bv=convert_bv(op2);
 
-  if(size*op2_bv.size()!=prev_bv.size())
+  if(*size * op2_bv.size() != prev_bv.size())
   {
     error().source_location=type.source_location();
     error() << "convert_with_array: unexpected operand 2 width" << eom;
@@ -150,7 +150,7 @@ void boolbvt::convert_with_array(
     // Yes, it is!
     next_bv=prev_bv;
 
-    if(op1_value>=0 && op1_value<size) // bounds check
+    if(op1_value >= 0 && op1_value < *size) // bounds check
     {
       const std::size_t offset =
         numeric_cast_v<std::size_t>(op1_value * op2_bv.size());
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
index 12c2423e03c..fbc2ddff67d 100644
--- a/src/util/endianness_map.cpp
+++ b/src/util/endianness_map.cpp
@@ -92,13 +92,13 @@ void endianness_mapt::build_big_endian(const typet &src)
     const array_typet &array_type=to_array_type(src);
 
     // array size constant?
-    mp_integer s;
-    if(!to_integer(array_type.size(), s))
+    auto s = numeric_cast<mp_integer>(array_type.size());
+    if(s.has_value())
     {
-      while(s>0)
+      while(*s > 0)
       {
         build_big_endian(array_type.subtype());
-        --s;
+        --(*s);
       }
     }
   }
@@ -106,11 +106,9 @@ void endianness_mapt::build_big_endian(const typet &src)
   {
     const vector_typet &vector_type=to_vector_type(src);
 
-    mp_integer s;
-    if(to_integer(vector_type.size(), s))
-      CHECK_RETURN(false);
+    mp_integer s = numeric_cast_v<mp_integer>(vector_type.size());
 
-    while(s>0)
+    while(s > 0)
     {
       build_big_endian(vector_type.subtype());
       --s;
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index adae5ae42c5..384d23aee02 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -136,8 +136,6 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       if(tmpval.is_nil())
         return nil_exprt();
 
-      mp_integer array_size;
-
       if(array_type.size().id()==ID_infinity)
       {
         if(nondet)
@@ -147,7 +145,9 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
         value.add_source_location()=source_location;
         return std::move(value);
       }
-      else if(to_integer(array_type.size(), array_size))
+
+      const auto array_size = numeric_cast<mp_integer>(array_type.size());
+      if(!array_size.has_value())
       {
         if(nondet)
           return side_effect_expr_nondett(type, source_location);
@@ -155,11 +155,11 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
           return nil_exprt();
       }
 
-      if(array_size < 0)
+      if(*array_size < 0)
         return nil_exprt();
 
       array_exprt value(array_type);
-      value.operands().resize(integer2size_t(array_size), tmpval);
+      value.operands().resize(numeric_cast_v<std::size_t>(*array_size), tmpval);
       value.add_source_location()=source_location;
       return std::move(value);
     }
@@ -172,21 +172,14 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     if(tmpval.is_nil())
       return nil_exprt();
 
-    mp_integer vector_size;
-
-    if(to_integer(vector_type.size(), vector_size))
-    {
-      if(nondet)
-        return side_effect_expr_nondett(type, source_location);
-      else
-        return nil_exprt();
-    }
+    const mp_integer vector_size =
+      numeric_cast_v<mp_integer>(vector_type.size());
 
     if(vector_size < 0)
       return nil_exprt();
 
     vector_exprt value(vector_type);
-    value.operands().resize(integer2size_t(vector_size), tmpval);
+    value.operands().resize(numeric_cast_v<std::size_t>(vector_size), tmpval);
     value.add_source_location()=source_location;
 
     return std::move(value);
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 95d1a6046c1..800cb58d8d1 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -106,16 +106,12 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
     if(!sub.has_value())
       return {};
 
-    // get size
-    const exprt &size=to_array_type(type).size();
-
-    // constant?
-    mp_integer i;
-
-    if(to_integer(size, i))
-      return {}; // we cannot distinguish the elements
+    // get size - we can only distinguish the elements if the size is constant
+    const auto size = numeric_cast<mp_integer>(to_array_type(type).size());
+    if(!size.has_value())
+      return {};
 
-    return (*sub) * i;
+    return (*sub) * (*size);
   }
   else if(type.id()==ID_vector)
   {
@@ -124,15 +120,10 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
       return {};
 
     // get size
-    const exprt &size=to_vector_type(type).size();
+    const mp_integer size =
+      numeric_cast_v<mp_integer>(to_vector_type(type).size());
 
-    // constant?
-    mp_integer i;
-
-    if(to_integer(size, i))
-      return {}; // we cannot distinguish the elements
-
-    return (*sub) * i;
+    return (*sub) * size;
   }
   else if(type.id()==ID_complex)
   {
@@ -564,12 +555,12 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
       const auto &array_type = to_array_type(index_expr.array().type());
       auto sub_size = pointer_offset_size(array_type.subtype(), ns);
 
-      mp_integer i;
-
-      if(
-        sub_size.has_value() && *sub_size > 0 &&
-        !to_integer(index_expr.index(), i))
-        return (*o) + i * (*sub_size);
+      if(sub_size.has_value() && *sub_size > 0)
+      {
+        const auto i = numeric_cast<mp_integer>(index_expr.index());
+        if(i.has_value())
+          return (*o) + (*i) * (*sub_size);
+      }
     }
 
     // don't know
@@ -607,40 +598,38 @@ exprt build_sizeof_expr(
   const typet &type=
     static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
 
-  mp_integer type_size=-1, val=-1;
+  if(type.is_nil())
+    return nil_exprt();
 
-  if(type.is_not_nil())
-  {
-    auto tmp = pointer_offset_size(type, ns);
-    if(tmp.has_value())
-      type_size = *tmp;
-  }
+  const auto type_size = pointer_offset_size(type, ns);
+  auto val = numeric_cast<mp_integer>(expr);
 
-  if(type_size<0 ||
-     to_integer(expr, val) ||
-     val<type_size ||
-     (type_size==0 && val>0))
+  if(
+    !type_size.has_value() || *type_size < 0 || !val.has_value() ||
+    *val < *type_size || (*type_size == 0 && *val > 0))
+  {
     return nil_exprt();
+  }
 
   const typet t(size_type());
   DATA_INVARIANT(
-    address_bits(val + 1) <= *pointer_offset_bits(t, ns),
+    address_bits(*val + 1) <= *pointer_offset_bits(t, ns),
     "sizeof value does not fit size_type");
 
   mp_integer remainder=0;
 
-  if(type_size!=0)
+  if(*type_size != 0)
   {
-    remainder=val%type_size;
-    val-=remainder;
-    val/=type_size;
+    remainder = *val % *type_size;
+    *val -= remainder;
+    *val /= *type_size;
   }
 
   exprt result(ID_sizeof, t);
   result.set(ID_type_arg, type);
 
-  if(val>1)
-    result=mult_exprt(result, from_integer(val, t));
+  if(*val > 1)
+    result = mult_exprt(result, from_integer(*val, t));
   if(remainder>0)
     result=plus_exprt(result, from_integer(remainder, t));
 
@@ -735,10 +724,10 @@ exprt get_subexpression_at_offset(
   const typet &target_type,
   const namespacet &ns)
 {
-  mp_integer offset_const;
+  const auto offset_bytes = numeric_cast<mp_integer>(offset);
 
-  if(to_integer(offset, offset_const))
+  if(!offset_bytes.has_value())
     return nil_exprt();
   else
-    return get_subexpression_at_offset(expr, offset_const, target_type, ns);
+    return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
 }
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index a9fdceab3ba..b2ed428b031 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -78,18 +78,18 @@ bool simplify_exprt::simplify_abs(exprt &expr)
     else if(type.id()==ID_signedbv ||
             type.id()==ID_unsignedbv)
     {
-      mp_integer value;
-      if(!to_integer(expr.op0(), value))
+      auto value = numeric_cast<mp_integer>(expr.op0());
+      if(value.has_value())
       {
-        if(value>=0)
+        if(*value >= 0)
         {
           expr=expr.op0();
           return false;
         }
         else
         {
-          value.negate();
-          expr=from_integer(value, type);
+          value->negate();
+          expr = from_integer(*value, type);
           return false;
         }
       }
@@ -117,10 +117,10 @@ bool simplify_exprt::simplify_sign(exprt &expr)
     else if(type.id()==ID_signedbv ||
             type.id()==ID_unsignedbv)
     {
-      mp_integer value;
-      if(!to_integer(expr.op0(), value))
+      const auto value = numeric_cast<mp_integer>(expr.op0());
+      if(value.has_value())
       {
-        expr.make_bool(value>=0);
+        expr.make_bool(*value >= 0);
         return false;
       }
     }
@@ -1261,15 +1261,15 @@ bool simplify_exprt::simplify_with(exprt &expr)
     {
       while(expr.operands().size()>1)
       {
-        mp_integer i;
+        const auto i = numeric_cast<mp_integer>(expr.op1());
 
-        if(to_integer(expr.op1(), i))
+        if(!i.has_value())
           break;
 
-        if(i<0 || i>=expr.op0().operands().size())
+        if(*i < 0 || *i >= expr.op0().operands().size())
           break;
 
-        expr.op0().operands()[integer2size_t(i)].swap(expr.op2());
+        expr.op0().operands()[numeric_cast_v<std::size_t>(*i)].swap(expr.op2());
 
         expr.operands().erase(++expr.operands().begin());
         expr.operands().erase(++expr.operands().begin());
@@ -1309,15 +1309,15 @@ bool simplify_exprt::simplify_update(exprt &expr)
     if(e.id()==ID_index_designator &&
        value_ptr->id()==ID_array)
     {
-      mp_integer i;
+      const auto i = numeric_cast<mp_integer>(e.op0());
 
-      if(to_integer(e.op0(), i))
+      if(!i.has_value())
         return true;
 
-      if(i<0 || i>=value_ptr->operands().size())
+      if(*i < 0 || *i >= value_ptr->operands().size())
         return true;
 
-      value_ptr=&value_ptr->operands()[integer2size_t(i)];
+      value_ptr = &value_ptr->operands()[numeric_cast_v<std::size_t>(*i)];
     }
     else if(e.id()==ID_member_designator &&
             value_ptr->id()==ID_struct)
@@ -1675,13 +1675,13 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
   }
 
   // the following require a constant offset
-  mp_integer offset;
-  if(to_integer(expr.offset(), offset) || offset<0)
+  auto offset = numeric_cast<mp_integer>(expr.offset());
+  if(!offset.has_value() || *offset < 0)
     return true;
 
   // don't do any of the following if endianness doesn't match, as
   // bytes need to be swapped
-  if(offset == 0 && byte_extract_id() == expr.id())
+  if(*offset == 0 && byte_extract_id() == expr.id())
   {
     // byte extract of full object is object
     if(base_type_eq(expr.type(), expr.op().type(), ns))
@@ -1721,11 +1721,11 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty");
 
     // double the string until we have sufficiently many bits
-    while(mp_integer(const_bits.size()) < offset * 8 + *el_size)
+    while(mp_integer(const_bits.size()) < *offset * 8 + *el_size)
       const_bits+=const_bits;
 
     std::string el_bits = std::string(
-      const_bits, integer2size_t(offset * 8), integer2size_t(*el_size));
+      const_bits, integer2size_t(*offset * 8), integer2size_t(*el_size));
 
     exprt tmp=
       bits2expr(
@@ -1742,7 +1742,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 
   // in some cases we even handle non-const array_of
   if(
-    expr.op().id() == ID_array_of && (offset * 8) % (*el_size) == 0 &&
+    expr.op().id() == ID_array_of && (*offset * 8) % (*el_size) == 0 &&
     *el_size <= pointer_offset_bits(expr.op().op0().type(), ns))
   {
     expr.op()=index_exprt(expr.op(), expr.offset());
@@ -1758,14 +1758,12 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 
   // exact match of length only - otherwise we might lose bits of
   // flexible array members at the end of a struct
-  if(bits.has_value() &&
-     mp_integer(bits->size()) == el_size.value() + offset * 8)
+  if(bits.has_value() && mp_integer(bits->size()) == *el_size + *offset * 8)
   {
-    std::string bits_cut=
-      std::string(
-        bits.value(),
-        integer2size_t(offset*8),
-        integer2size_t(el_size.value()));
+    std::string bits_cut = std::string(
+      bits.value(),
+      integer2size_t(*offset * 8),
+      integer2size_t(el_size.value()));
 
     exprt tmp=
       bits2expr(
@@ -1783,7 +1781,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 
   // try to refine it down to extracting from a member or an index in an array
   exprt subexpr =
-    get_subexpression_at_offset(expr.op(), offset, expr.type(), ns);
+    get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns);
   if(subexpr.is_nil() || subexpr == expr)
     return true;
 
@@ -1913,8 +1911,8 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
   }
 
   // the following require a constant offset
-  mp_integer offset_int;
-  if(to_integer(offset, offset_int) || offset_int<0)
+  const auto offset_int = numeric_cast<mp_integer>(offset);
+  if(!offset_int.has_value() || *offset_int < 0)
     return true;
 
   const typet &op_type=ns.follow(root.type());
@@ -1960,12 +1958,12 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
       mp_integer m_size_bytes = (*m_size_bits) / 8;
 
       // is that member part of the update?
-      if(*m_offset + m_size_bytes <= offset_int)
+      if(*m_offset + m_size_bytes <= *offset_int)
         continue;
       // are we done updating?
       else if(
         update_size.has_value() && *update_size > 0 &&
-        *m_offset >= offset_int + *update_size)
+        *m_offset >= *offset_int + *update_size)
       {
         break;
       }
@@ -1979,21 +1977,21 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
 
       // are we updating on member boundaries?
       if(
-        m_offset < offset_int ||
-        (m_offset == offset_int && update_size.has_value() &&
+        *m_offset < *offset_int ||
+        (*m_offset == *offset_int && update_size.has_value() &&
          *update_size > 0 && m_size_bytes > *update_size))
       {
         byte_update_exprt v(
           ID_byte_update_little_endian,
           member_exprt(root, component.get_name(), component.type()),
-          from_integer(offset_int - *m_offset, offset.type()),
+          from_integer(*offset_int - *m_offset, offset.type()),
           value);
 
         to_with_expr(result_expr).new_value().swap(v);
       }
       else if(
         update_size.has_value() && *update_size > 0 &&
-        *m_offset + m_size_bytes > offset_int + *update_size)
+        *m_offset + m_size_bytes > *offset_int + *update_size)
       {
         // we don't handle this for the moment
         result_expr.make_nil();
@@ -2004,7 +2002,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
         byte_extract_exprt v(
           ID_byte_extract_little_endian,
           value,
-          from_integer(*m_offset - offset_int, offset.type()),
+          from_integer(*m_offset - *offset_int, offset.type()),
           component.type());
 
         to_with_expr(result_expr).new_value().swap(v);
@@ -2045,12 +2043,12 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
     mp_integer m_offset_bits=0, val_offset=0;
     Forall_operands(it, result)
     {
-      if(offset_int * 8 + (*val_size) <= m_offset_bits)
+      if(*offset_int * 8 + (*val_size) <= m_offset_bits)
         break;
 
-      if(offset_int * 8 < m_offset_bits + *el_size)
+      if(*offset_int * 8 < m_offset_bits + *el_size)
       {
-        mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - offset_int;
+        mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
         bytes_req-=val_offset;
         if(val_offset + bytes_req > (*val_size) / 8)
           bytes_req = (*val_size) / 8 - val_offset;
@@ -2062,10 +2060,11 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
           array_typet(unsignedbv_typet(8),
                       from_integer(bytes_req, offset.type())));
 
-        *it=byte_update_exprt(
+        *it = byte_update_exprt(
           expr.id(),
           *it,
-          from_integer(offset_int+val_offset-m_offset_bits/8, offset.type()),
+          from_integer(
+            *offset_int + val_offset - m_offset_bits / 8, offset.type()),
           new_val);
 
         simplify_rec(*it);
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index 0a4f0aa1dee..59e8be02dfc 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -116,40 +116,41 @@ bool simplify_exprt::simplify_index(exprt &expr)
   else if(array.id()==ID_constant ||
           array.id()==ID_array)
   {
-    mp_integer i;
+    const auto i = numeric_cast<mp_integer>(expr.op1());
 
-    if(to_integer(expr.op1(), i))
+    if(!i.has_value())
     {
     }
-    else if(i<0 || i>=array.operands().size())
+    else if(*i < 0 || *i >= array.operands().size())
     {
       // out of bounds
     }
     else
     {
       // ok
-      exprt tmp=array.operands()[integer2size_t(i)];
+      exprt tmp = array.operands()[numeric_cast_v<std::size_t>(*i)];
       expr.swap(tmp);
       return false;
     }
   }
   else if(array.id()==ID_string_constant)
   {
-    mp_integer i;
+    const auto i = numeric_cast<mp_integer>(expr.op1());
 
     const irep_idt &value=array.get(ID_value);
 
-    if(to_integer(expr.op1(), i))
+    if(!i.has_value())
     {
     }
-    else if(i<0 || i>value.size())
+    else if(*i < 0 || *i > value.size())
     {
       // out of bounds
     }
     else
     {
       // terminating zero?
-      char v=(i==value.size())?0:value[integer2size_t(i)];
+      const char v =
+        (*i == value.size()) ? 0 : value[numeric_cast_v<std::size_t>(*i)];
       exprt tmp=from_integer(v, expr.type());
       expr.swap(tmp);
       return false;