diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
index e79c6f3d90d..aa5356c0712 100644
--- a/src/goto-symex/partial_order_concurrency.cpp
+++ b/src/goto-symex/partial_order_concurrency.cpp
@@ -166,9 +166,8 @@ void partial_order_concurrencyt::build_clock_type(
 {
   assert(!numbering.empty());
 
-  mp_integer width=address_bits(numbering.size());
-  assert(width<std::numeric_limits<unsigned>::max());
-  clock_type=unsignedbv_typet(integer2unsigned(width));
+  std::size_t width = address_bits(numbering.size());
+  clock_type = unsignedbv_typet(width);
 }
 
 exprt partial_order_concurrencyt::before(
diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp
index 7dbea100aeb..a2da9cc3352 100644
--- a/src/solvers/flattening/boolbv_extractbit.cpp
+++ b/src/solvers/flattening/boolbv_extractbit.cpp
@@ -52,10 +52,8 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     if(width_op0==0 || width_op1==0)
       return SUB::convert_rest(expr);
 
-    mp_integer index_width=
-      std::max(address_bits(width_op0), mp_integer(width_op1));
-
-    unsignedbv_typet index_type(integer2size_t(index_width));
+    std::size_t index_width = std::max(address_bits(width_op0), width_op1);
+    unsignedbv_typet index_type(index_width);
 
     equal_exprt equality;
     equality.lhs()=operands[1]; // index operand
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index c8c5408946a..a5f32a2fe5f 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -122,7 +122,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
 
     if(size>=1)
     {
-      entry.total_width=integer2unsigned(address_bits(size));
+      entry.total_width = address_bits(size);
       assert(entry.total_width!=0);
     }
   }
@@ -180,7 +180,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   {
     // get number of necessary bits
     std::size_t size=to_enumeration_type(type).elements().size();
-    entry.total_width=integer2unsigned(address_bits(size));
+    entry.total_width = address_bits(size);
     assert(entry.total_width!=0);
   }
   else if(type_id==ID_c_enum)
diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
index b1810b85d0e..01aaef02a07 100644
--- a/src/solvers/floatbv/float_bv.cpp
+++ b/src/solvers/floatbv/float_bv.cpp
@@ -233,7 +233,7 @@ exprt float_bvt::from_signed_integer(
   result.exponent=
     from_integer(
       src_width-1,
-      signedbv_typet(address_bits(src_width-1).to_long()+1));
+      signedbv_typet(address_bits(src_width - 1) + 1));
 
   return rounder(result, rm, spec);
 }
@@ -253,7 +253,7 @@ exprt float_bvt::from_unsigned_integer(
   result.exponent=
     from_integer(
       src_width-1,
-      signedbv_typet(address_bits(src_width-1).to_long()+1));
+      signedbv_typet(address_bits(src_width - 1) + 1));
 
   result.sign=false_exprt();
 
@@ -573,7 +573,7 @@ exprt float_bvt::limit_distance(
   const exprt &dist,
   mp_integer limit)
 {
-  std::size_t nb_bits=integer2unsigned(address_bits(limit));
+  std::size_t nb_bits = address_bits(limit);
   std::size_t dist_width=to_unsignedbv_type(dist.type()).get_width();
 
   if(dist_width<=nb_bits)
@@ -889,7 +889,7 @@ void float_bvt::normalization_shift(
   std::size_t exponent_bits=to_signedbv_type(exponent.type()).get_width();
   assert(fraction_bits!=0);
 
-  unsigned depth=integer2unsigned(address_bits(fraction_bits-1));
+  std::size_t depth = address_bits(fraction_bits - 1);
 
   if(exponent_bits<depth)
     exponent=typecast_exprt(exponent, signedbv_typet(depth));
@@ -1019,9 +1019,7 @@ exprt float_bvt::rounder(
         aligned_exponent=src.exponent;
 
   {
-    std::size_t exponent_bits=
-      std::max((std::size_t)integer2size_t(address_bits(spec.f)),
-               (std::size_t)spec.e)+1;
+    std::size_t exponent_bits = std::max(address_bits(spec.f), spec.e) + 1;
 
     // before normalization, make sure exponent is large enough
     if(to_signedbv_type(aligned_exponent.type()).get_width()<exponent_bits)
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index 6dd36849af8..600add64d5e 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -43,7 +43,7 @@ bvt float_utilst::from_signed_integer(const bvt &src)
   result.exponent=
     bv_utils.build_constant(
       src.size()-1,
-      address_bits(src.size()-1).to_long()+1);
+      address_bits(src.size() - 1) + 1);
 
   return rounder(result);
 }
@@ -58,7 +58,7 @@ bvt float_utilst::from_unsigned_integer(const bvt &src)
   result.exponent=
     bv_utils.build_constant(
       src.size()-1,
-      address_bits(src.size()-1).to_long()+1);
+      address_bits(src.size() - 1) + 1);
 
   result.sign=const_literal(false);
 
@@ -388,7 +388,7 @@ bvt float_utilst::limit_distance(
   const bvt &dist,
   mp_integer limit)
 {
-  std::size_t nb_bits=integer2unsigned(address_bits(limit));
+  std::size_t nb_bits = address_bits(limit);
 
   bvt upper_bits=dist;
   upper_bits.erase(upper_bits.begin(), upper_bits.begin()+nb_bits);
@@ -790,7 +790,7 @@ void float_utilst::normalization_shift(bvt &fraction, bvt &exponent)
   // The worst-case shift is the number of fraction
   // bits minus one, in case the faction is one exactly.
   assert(!fraction.empty());
-  unsigned depth=integer2unsigned(address_bits(fraction.size()-1));
+  std::size_t depth = address_bits(fraction.size() - 1);
 
   if(exponent.size()<depth)
     exponent=bv_utils.sign_extension(exponent, depth);
@@ -903,9 +903,7 @@ bvt float_utilst::rounder(const unbiased_floatt &src)
       aligned_exponent=src.exponent;
 
   {
-    std::size_t exponent_bits=
-      std::max((std::size_t)integer2size_t(address_bits(spec.f)),
-               (std::size_t)spec.e)+1;
+    std::size_t exponent_bits = std::max(address_bits(spec.f), spec.e) + 1;
 
     // before normalization, make sure exponent is large enough
     if(aligned_exponent.size()<exponent_bits)
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
index 680b5309775..f2e9af04ae0 100644
--- a/src/util/arith_tools.cpp
+++ b/src/util/arith_tools.cpp
@@ -8,10 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "arith_tools.h"
 
-#include <cassert>
-
 #include "fixedbv.h"
 #include "ieee_float.h"
+#include "invariant.h"
 #include "std_types.h"
 #include "std_expr.h"
 
@@ -207,11 +206,17 @@ constant_exprt from_integer(
 }
 
 /// ceil(log2(size))
-mp_integer address_bits(const mp_integer &size)
+std::size_t address_bits(const mp_integer &size)
 {
-  mp_integer result, x=2;
+  // in theory an arbitrary-precision integer could be as large as
+  // numeric_limits<std::size_t>::max() * CHAR_BIT (but then we would only be
+  // able to store 2^CHAR_BIT many of those; the implementation of mp_integer as
+  // BigInt is much more restricted as its size is stored as an unsigned int
+  std::size_t result = 1;
+
+  for(mp_integer x = 2; x < size; ++result, x *= 2) {}
 
-  for(result=1; x<size; result+=1, x*=2) {}
+  INVARIANT(power(2, result) >= size, "address_bits(size) >= log2(size)");
 
   return result;
 }
@@ -222,7 +227,7 @@ mp_integer address_bits(const mp_integer &size)
 mp_integer power(const mp_integer &base,
                  const mp_integer &exponent)
 {
-  assert(exponent>=0);
+  PRECONDITION(exponent >= 0);
 
   /* There are a number of special cases which are:
    *  A. very common
diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h
index 93fb4d315f2..7cf73b678b7 100644
--- a/src/util/arith_tools.h
+++ b/src/util/arith_tools.h
@@ -155,7 +155,7 @@ Target numeric_cast_v(const exprt &arg)
 constant_exprt from_integer(const mp_integer &int_value, const typet &type);
 
 // ceil(log2(size))
-mp_integer address_bits(const mp_integer &size);
+std::size_t address_bits(const mp_integer &size);
 
 mp_integer power(const mp_integer &base, const mp_integer &exponent);