diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index cbd36d3ccb60..870f66b2f0aa 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -150,7 +150,7 @@ void rw_range_sett::get_objects_byte_extract(
   auto object_size_bits_opt = pointer_offset_bits(be.op().type(), ns);
   const exprt simp_offset=simplify_expr(be.offset(), ns);
 
-  auto index = numeric_cast<mp_integer>(simp_offset);
+  auto index = numeric_cast<bytest>(simp_offset);
   if(
     range_start.is_unknown() || !index.has_value() ||
     !object_size_bits_opt.has_value())
@@ -159,8 +159,8 @@ void rw_range_sett::get_objects_byte_extract(
   }
   else
   {
-    *index *= be.get_bits_per_byte();
-    if(*index >= *object_size_bits_opt)
+    bitst index_bits = bytes_to_bits(*index, be.get_bits_per_byte());
+    if(index_bits >= *object_size_bits_opt)
       return;
 
     endianness_mapt map(
@@ -168,16 +168,16 @@ void rw_range_sett::get_objects_byte_extract(
       be.id()==ID_byte_extract_little_endian,
       ns);
     range_spect offset = range_start;
-    if(*index > 0)
+    if(index_bits > bitst{0})
     {
       offset += range_spect::to_range_spect(
-        map.map_bit(numeric_cast_v<std::size_t>(*index)));
+        bitst{map.map_bit(numeric_cast_v<std::size_t>(index_bits))});
     }
     else
     {
       // outside the bounds of immediate byte-extract operand, might still be in
       // bounds of a parent object
-      offset += range_spect::to_range_spect(*index);
+      offset += range_spect::to_range_spect(index_bits);
     }
     get_objects_rec(mode, be.op(), offset, size);
   }
@@ -197,7 +197,7 @@ void rw_range_sett::get_objects_shift(
                            ? range_spect::to_range_spect(*op_bits)
                            : range_spect::unknown();
 
-  const auto dist = numeric_cast<mp_integer>(simp_distance);
+  const auto dist = numeric_cast<bitst>(simp_distance);
   if(
     range_start.is_unknown() || size.is_unknown() || src_size.is_unknown() ||
     !dist.has_value())
@@ -312,7 +312,7 @@ void rw_range_sett::get_objects_index(
     get_objects_rec(
       mode,
       expr.array(),
-      range_start + range_spect::to_range_spect(*index) * sub_size,
+      range_start + range_spect::to_range_spect(bitst{*index}) * sub_size,
       size);
   }
 }
@@ -342,7 +342,7 @@ void rw_range_sett::get_objects_array(
     range_start.is_unknown() ? range_spect{0} : range_start;
   range_spect full_r_e =
     size.is_unknown()
-      ? sub_size * range_spect::to_range_spect(expr.operands().size())
+      ? sub_size * range_spect::to_range_spect(bitst{expr.operands().size()})
       : full_r_s + size;
 
   for(const auto &op : expr.operands())
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index a6c1bf227fbe..078b1791bda3 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -76,15 +76,15 @@ class range_spect
     return *this == unknown();
   }
 
-  static range_spect to_range_spect(const mp_integer &size)
+  static range_spect to_range_spect(const bitst &size)
   {
     // The size need not fit into the analysis platform's width of a signed long
     // (as an example, it could be an unsigned size_t max, or perhaps the source
     // platform has much wider types than the analysis platform.
-    if(!size.is_long())
+    if(!size.get().is_long())
       return range_spect::unknown();
 
-    mp_integer::llong_t ll = size.to_long();
+    mp_integer::llong_t ll = size.get().to_long();
     if(
       ll > std::numeric_limits<range_spect::value_type>::max() ||
       ll < std::numeric_limits<range_spect::value_type>::min())
@@ -128,7 +128,7 @@ class range_spect
   {
     if(is_unknown() || other.is_unknown())
       return range_spect::unknown();
-    return range_spect::to_range_spect(mp_integer{v} + mp_integer{other.v});
+    return range_spect::to_range_spect(bitst{v} + bitst{other.v});
   }
 
   range_spect &operator+=(const range_spect &other)
@@ -142,7 +142,7 @@ class range_spect
   {
     if(is_unknown() || other.is_unknown())
       return range_spect::unknown();
-    return range_spect::to_range_spect(mp_integer{v} - mp_integer{other.v});
+    return range_spect::to_range_spect(bitst{v} - bitst{other.v});
   }
 
   range_spect &operator-=(const range_spect &other)
@@ -156,7 +156,8 @@ class range_spect
   {
     if(is_unknown() || other.is_unknown())
       return range_spect::unknown();
-    return range_spect::to_range_spect(mp_integer{v} * mp_integer{other.v});
+    return range_spect::to_range_spect(
+      bitst{mp_integer{v} * mp_integer{other.v}});
   }
 
 private:
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 749353af3cef..2c97ee8e9cf0 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -125,9 +125,10 @@ static std::string architecture_string(const std::string &value, const char *s)
 template <typename T>
 static std::string architecture_string(T value, const char *s)
 {
-  return std::string("const " CPROVER_PREFIX "integer " CPROVER_PREFIX
-                     "architecture_") +
-         std::string(s) + "=" + std::to_string(value) + ";\n";
+  std::ostringstream os;
+  os << "const " << CPROVER_PREFIX "integer " << CPROVER_PREFIX "architecture_"
+     << s << '=' << value << ";\n";
+  return os.str();
 }
 
 /// The maximum allocation size is determined by the number of bits that
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index df210afc6cf0..ee5161ef6d27 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -1085,7 +1085,7 @@ void c_typecheck_baset::typecheck_expr_alignof(exprt &expr)
   }
 
   // we only care about the type
-  mp_integer a=alignment(argument_type, *this);
+  bytest a = alignment(argument_type, *this);
 
   exprt tmp=from_integer(a, size_type());
   tmp.add_source_location()=expr.source_location();
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 8643386266e4..2e0722d1bb5f 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3726,8 +3726,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_bswap)
     return convert_function(
       src,
-      "__builtin_bswap" + integer2string(*pointer_offset_bits(
-                            to_unary_expr(src).op().type(), ns)));
+      "__builtin_bswap" +
+        integer2string(
+          pointer_offset_bits(to_unary_expr(src).op().type(), ns)->get()));
 
   else if(has_prefix(src.id_string(), "byte_extract"))
     return convert_byte_extract(to_byte_extract_expr(src), precedence = 16);
diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index d7996e6d8315..9328fdaf5376 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
-mp_integer alignment(const typet &type, const namespacet &ns)
+bytest alignment(const typet &type, const namespacet &ns)
 {
   // we need to consider a number of different cases:
   // - alignment specified in the source, which will be recorded in
@@ -37,32 +37,30 @@ 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 = 0;
+  bytest a_int{0};
 
   // we trust it blindly, no matter how nonsensical
   if(given_alignment.is_not_nil())
   {
-    const auto a = numeric_cast<mp_integer>(given_alignment);
+    const auto a = numeric_cast<bytest>(given_alignment);
     if(a.has_value())
       a_int = *a;
   }
 
   // alignment but no packing
-  if(a_int>0 && !type.get_bool(ID_C_packed))
+  if(a_int > bytest{0} && !type.get_bool(ID_C_packed))
     return a_int;
   // no alignment, packing
-  else if(a_int==0 && type.get_bool(ID_C_packed))
-    return 1;
+  else if(a_int == bytest{0} && type.get_bool(ID_C_packed))
+    return bytest{1};
 
   // compute default
-  mp_integer result;
+  bytest result{1};
 
   if(type.id()==ID_array)
     result = alignment(to_array_type(type).element_type(), ns);
   else if(type.id()==ID_struct || type.id()==ID_union)
   {
-    result=1;
-
     // get the max
     // (should really be the smallest common denominator)
     for(const auto &c : to_struct_union_type(type).components())
@@ -90,12 +88,10 @@ mp_integer alignment(const typet &type, const namespacet &ns)
     // we align these according to the 'underlying type'
     result = alignment(to_c_bit_field_type(type).underlying_type(), ns);
   }
-  else
-    result=1;
 
   // if an alignment had been provided and packing was requested, take
   // the smallest alignment
-  if(a_int>0 && a_int<result)
+  if(a_int > bytest{0} && a_int < result)
     result=a_int;
 
   return result;
@@ -172,7 +168,7 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
   struct_typet::componentst &components=type.components();
 
   std::size_t bit_field_bits = 0, underlying_bits = 0;
-  mp_integer offset = 0;
+  bytest offset{0};
 
   bool is_packed = type.get_bool(ID_C_packed);
 
@@ -205,26 +201,27 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
         const std::size_t pad_bits =
           underlying_bits - (bit_field_bits % underlying_bits);
         it = pad_bit_field(components, it, pad_bits);
-        offset += (bit_field_bits + pad_bits) / config.ansi_c.char_width;
+        offset +=
+          bytest{(bit_field_bits + pad_bits) / config.ansi_c.char_width};
         underlying_bits = bit_field_bits = 0;
       }
       else
       {
-        offset += bit_field_bits / config.ansi_c.char_width;
+        offset += bytest{bit_field_bits / config.ansi_c.char_width};
         underlying_bits = bit_field_bits = 0;
       }
 
       // pad up to underlying type unless the struct is packed
       if(!is_packed)
       {
-        const mp_integer a = alignment(it->type(), ns);
-        if(a > 1)
+        const bytest a = alignment(it->type(), ns);
+        if(a > bytest{1})
         {
-          const mp_integer displacement = offset % a;
+          const bytest displacement = offset % a;
 
-          if(displacement != 0)
+          if(displacement != bytest{0})
           {
-            const mp_integer pad_bytes = a - displacement;
+            const bytest pad_bytes = a - displacement;
             std::size_t pad_bits =
               numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
             it = pad(components, it, pad_bits);
@@ -250,7 +247,7 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
       {
         // keep track of offset
         const auto size = pointer_offset_size(it->type(), ns);
-        if(size.has_value() && *size >= 1)
+        if(size.has_value() && *size >= bytest{1})
           offset += *size;
       }
     }
@@ -263,19 +260,19 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
     const std::size_t pad =
       underlying_bits - (bit_field_bits % underlying_bits);
     pad_bit_field(components, components.end(), pad);
-    offset += (bit_field_bits + pad) / config.ansi_c.char_width;
+    offset += bytest{(bit_field_bits + pad) / config.ansi_c.char_width};
   }
   else
-    offset += bit_field_bits / config.ansi_c.char_width;
+    offset += bytest{bit_field_bits / config.ansi_c.char_width};
 
   // alignment of the struct
   // Note that this is done even if the struct is packed.
-  const mp_integer a = alignment(type, ns);
-  const mp_integer displacement = offset % a;
+  const bytest a = alignment(type, ns);
+  const bytest displacement = offset % a;
 
-  if(displacement != 0)
+  if(displacement != bytest{0})
   {
-    const mp_integer pad_bytes = a - displacement;
+    const bytest pad_bytes = a - displacement;
     const std::size_t pad_bits =
       numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
     pad(components, components.end(), pad_bits);
@@ -330,8 +327,8 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
     }
   }
 
-  mp_integer offset=0;
-  mp_integer max_alignment=0;
+  bytest offset{0};
+  bytest max_alignment{0};
   std::size_t bit_field_bits=0;
   const bool struct_is_packed = type.get_bool(ID_C_packed);
 
@@ -341,7 +338,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
       it++)
   {
     const typet it_type=it->type();
-    mp_integer a=1;
+    bytest a{1};
 
     if(it_type.id()==ID_c_bit_field)
     {
@@ -362,7 +359,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
         bit_field_bits += w;
         const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
         bit_field_bits %= config.ansi_c.char_width;
-        offset+=bytes;
+        offset += bytest{bytes};
         continue;
       }
     }
@@ -375,7 +372,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
       ++bit_field_bits;
       const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
       bit_field_bits %= config.ansi_c.char_width;
-      offset += bytes;
+      offset += bytest{bytes};
       continue;
     }
     else
@@ -396,15 +393,15 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
       max_alignment=a;
 
     if(
-      a != 1 &&
+      a != bytest{1} &&
       (!struct_is_packed || it_type.find(ID_C_alignment).is_not_nil()))
     {
       // we may need to align it
-      const mp_integer displacement = offset % a;
+      const bytest displacement = offset % a;
 
-      if(displacement!=0)
+      if(displacement != bytest{0})
       {
-        const mp_integer pad_bytes = a - displacement;
+        const bytest pad_bytes = a - displacement;
         const std::size_t pad_bits =
           numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
         it = pad(components, it, pad_bits);
@@ -425,7 +422,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
   {
     if(alignment.id()!=ID_default)
     {
-      const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));
+      const auto tmp_i = numeric_cast<bytest>(simplify_expr(alignment, ns));
 
       if(tmp_i.has_value() && *tmp_i > max_alignment)
         max_alignment = *tmp_i;
@@ -438,14 +435,14 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
   // There may be a need for 'end of struct' padding.
   // We use 'max_alignment'.
 
-  if(max_alignment>1)
+  if(max_alignment > bytest{1})
   {
     // we may need to align it
-    mp_integer displacement=offset%max_alignment;
+    bytest displacement = offset % max_alignment;
 
-    if(displacement!=0)
+    if(displacement != bytest{0})
     {
-      mp_integer pad_bytes = max_alignment - displacement;
+      bytest pad_bytes = max_alignment - displacement;
       std::size_t pad_bits =
         numeric_cast_v<std::size_t>(pad_bytes * config.ansi_c.char_width);
       pad(components, components.end(), pad_bits);
@@ -464,9 +461,9 @@ void add_padding(struct_typet &type, const namespacet &ns)
 
 void add_padding(union_typet &type, const namespacet &ns)
 {
-  mp_integer max_alignment_bits =
-    alignment(type, ns) * config.ansi_c.char_width;
-  mp_integer size_bits=0;
+  bitst max_alignment_bits =
+    bytes_to_bits(alignment(type, ns), config.ansi_c.char_width);
+  bitst size_bits{0};
 
   // check per component, and ignore those without fixed size
   for(const auto &c : type.components())
@@ -480,7 +477,7 @@ void add_padding(union_typet &type, const namespacet &ns)
   if(type.get_bool(ID_C_packed))
   {
     // The size needs to be a multiple of 1 char only.
-    max_alignment_bits = config.ansi_c.char_width;
+    max_alignment_bits = bitst{config.ansi_c.char_width};
   }
 
   if(config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)
@@ -491,18 +488,17 @@ void add_padding(union_typet &type, const namespacet &ns)
       if(c.type().id() == ID_c_bit_field)
       {
         auto w = underlying_width(to_c_bit_field_type(c.type()), ns);
-        if(w.has_value() && w.value() > max_alignment_bits)
-          max_alignment_bits = w.value();
+        if(w.has_value() && bitst{w.value()} > max_alignment_bits)
+          max_alignment_bits = bitst{w.value()};
       }
   }
 
   // The size must be a multiple of the alignment, or
   // we add a padding member to the union.
 
-  if(size_bits%max_alignment_bits!=0)
+  if(size_bits % max_alignment_bits != bitst{0})
   {
-    mp_integer padding_bits=
-      max_alignment_bits-(size_bits%max_alignment_bits);
+    bitst padding_bits = max_alignment_bits - (size_bits % max_alignment_bits);
 
     unsignedbv_typet padding_type(
       numeric_cast_v<std::size_t>(size_bits + padding_bits));
diff --git a/src/ansi-c/padding.h b/src/ansi-c/padding.h
index f030df79aa3e..9b2ac0efad28 100644
--- a/src/ansi-c/padding.h
+++ b/src/ansi-c/padding.h
@@ -19,7 +19,7 @@ class struct_typet;
 class typet;
 class union_typet;
 
-mp_integer alignment(const typet &type, const namespacet &);
+bytest alignment(const typet &type, const namespacet &);
 void add_padding(struct_typet &type, const namespacet &);
 void add_padding(union_typet &type, const namespacet &);
 
diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
index 6e8521005321..8fdd09ed3053 100644
--- a/src/ansi-c/type2name.cpp
+++ b/src/ansi-c/type2name.cpp
@@ -76,7 +76,7 @@ static std::string pointer_offset_bits_as_string(
 {
   auto bits = pointer_offset_bits(type, ns);
   CHECK_RETURN(bits.has_value());
-  return integer2string(*bits);
+  return integer2string(bits->get());
 }
 
 static std::string type2name(
diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp
index 6dc8a74b7497..a96deb2109e8 100644
--- a/src/cprover/bv_pointers_wide.cpp
+++ b/src/cprover/bv_pointers_wide.cpp
@@ -209,7 +209,7 @@ std::optional<bvt> bv_pointers_widet::convert_address_of_rec(const exprt &expr)
 
     // get size
     auto size = pointer_offset_size(array_type.element_type(), ns);
-    CHECK_RETURN(size.has_value() && *size >= 0);
+    CHECK_RETURN(size.has_value() && *size >= bytest{0});
 
     bv = offset_arithmetic(type, bv, *size, index);
     CHECK_RETURN(bv.size() == bits);
@@ -231,7 +231,8 @@ std::optional<bvt> bv_pointers_widet::convert_address_of_rec(const exprt &expr)
     const std::size_t bits = boolbv_width(type);
     CHECK_RETURN(bv_opt->size() == bits);
 
-    bvt bv = offset_arithmetic(type, *bv_opt, 1, byte_extract_expr.offset());
+    bvt bv =
+      offset_arithmetic(type, *bv_opt, bytest{1}, byte_extract_expr.offset());
     CHECK_RETURN(bv.size() == bits);
     return std::move(bv);
   }
@@ -402,14 +403,12 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
 
     bvt bv;
 
-    mp_integer size = 0;
-    std::size_t count = 0;
+    std::optional<bytest> size;
 
     for(const auto &op : plus_expr.operands())
     {
       if(op.type().id() == ID_pointer)
       {
-        count++;
         bv = convert_bv(op);
         CHECK_RETURN(bv.size() == bits);
 
@@ -418,13 +417,17 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
           pointer_base_type.id() != ID_empty,
           "no pointer arithmetic over void pointers");
         auto size_opt = pointer_offset_size(pointer_base_type, ns);
-        CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
-        size = *size_opt;
+        CHECK_RETURN(size_opt.has_value() && *size_opt >= bytest{0});
+        INVARIANT(
+          !size.has_value(),
+          "there should be exactly one pointer-type operand in a pointer-type "
+          "sum");
+        size = std::move(size_opt);
       }
     }
 
     INVARIANT(
-      count == 1,
+      size.has_value(),
       "there should be exactly one pointer-type operand in a pointer-type sum");
 
     const std::size_t offset_bits = get_offset_width(type);
@@ -452,7 +455,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
       sum = bv_utils.add(sum, op_bv);
     }
 
-    return offset_arithmetic(type, bv, size, sum);
+    return offset_arithmetic(type, bv, *size, sum);
   }
   else if(expr.id() == ID_minus)
   {
@@ -481,7 +484,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
       pointer_base_type.id() != ID_empty,
       "no pointer arithmetic over void pointers");
     auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
-    CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+    CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > bytest{0});
     return offset_arithmetic(type, bv, *element_size_opt, neg_op1);
   }
   else if(
@@ -533,7 +536,7 @@ bvt bv_pointers_widet::convert_pointer_type(const exprt &expr)
 
     // get element size
     auto size = pointer_offset_size(element_address_expr.element_type(), ns);
-    CHECK_RETURN(size.has_value() && *size >= 0);
+    CHECK_RETURN(size.has_value() && *size >= bytest{0});
 
     // add offset
     bv = offset_arithmetic(
@@ -618,11 +621,13 @@ bvt bv_pointers_widet::convert_bitvector(const exprt &expr)
         lhs_pt.base_type().id() != ID_empty,
         "no pointer arithmetic over void pointers");
       auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
-      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+      CHECK_RETURN(
+        element_size_opt.has_value() && *element_size_opt > bytest{0});
 
-      if(*element_size_opt != 1)
+      if(*element_size_opt != bytest{1})
       {
-        bvt element_size_bv = bv_utils.build_constant(*element_size_opt, width);
+        bvt element_size_bv =
+          bv_utils.build_constant(element_size_opt->get(), width);
         difference = bv_utils.divider(
           difference, element_size_bv, bv_utilst::representationt::SIGNED);
       }
@@ -769,7 +774,7 @@ exprt bv_pointers_widet::bv_get_rec(
 
   pointer_logict::pointert pointer{
     numeric_cast_v<std::size_t>(binary2integer(value_addr, false)),
-    binary2integer(value_offset, false)};
+    bytest{binary2integer(value_offset, false)}};
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};
@@ -790,18 +795,18 @@ bvt bv_pointers_widet::encode(const mp_integer &addr, const pointer_typet &type)
 bvt bv_pointers_widet::offset_arithmetic(
   const pointer_typet &type,
   const bvt &bv,
-  const mp_integer &x)
+  const bytest &x)
 {
   const std::size_t offset_bits = get_offset_width(type);
 
   return offset_arithmetic(
-    type, bv, 1, bv_utils.build_constant(x, offset_bits));
+    type, bv, bytest{1}, bv_utils.build_constant(x.get(), offset_bits));
 }
 
 bvt bv_pointers_widet::offset_arithmetic(
   const pointer_typet &type,
   const bvt &bv,
-  const mp_integer &factor,
+  const bytest &factor,
   const exprt &index)
 {
   bvt bv_index = convert_bv(index);
@@ -819,16 +824,16 @@ bvt bv_pointers_widet::offset_arithmetic(
 bvt bv_pointers_widet::offset_arithmetic(
   const pointer_typet &type,
   const bvt &bv,
-  const mp_integer &factor,
+  const bytest &factor,
   const bvt &index)
 {
   bvt bv_index;
 
-  if(factor == 1)
+  if(factor == bytest{1})
     bv_index = index;
   else
   {
-    bvt bv_factor = bv_utils.build_constant(factor, index.size());
+    bvt bv_factor = bv_utils.build_constant(factor.get(), index.size());
     bv_index = bv_utils.signed_multiplier(index, bv_factor);
   }
 
diff --git a/src/cprover/bv_pointers_wide.h b/src/cprover/bv_pointers_wide.h
index 1c1f0be60fb0..d7c8f34ff02f 100644
--- a/src/cprover/bv_pointers_wide.h
+++ b/src/cprover/bv_pointers_wide.h
@@ -67,16 +67,16 @@ class bv_pointers_widet : public boolbvt
   [[nodiscard]] std::optional<bvt> convert_address_of_rec(const exprt &);
 
   [[nodiscard]] bvt
-  offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
+  offset_arithmetic(const pointer_typet &, const bvt &, const bytest &);
   [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
-    const mp_integer &factor,
+    const bytest &factor,
     const exprt &index);
   [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
-    const mp_integer &factor,
+    const bytest &factor,
     const bvt &index_bv);
 
   struct postponedt
diff --git a/src/cprover/endianness_map_wide.cpp b/src/cprover/endianness_map_wide.cpp
index f3d2d03229d7..77c312942812 100644
--- a/src/cprover/endianness_map_wide.cpp
+++ b/src/cprover/endianness_map_wide.cpp
@@ -18,7 +18,7 @@ void endianness_map_widet::build_little_endian(const typet &src)
   {
     auto s = pointer_offset_bits(src, ns);
     CHECK_RETURN(s.has_value());
-    s.value() = s.value() * 2;
+    s.value() = bitst{s.value() * 2};
 
     const std::size_t new_size = map.size() + numeric_cast_v<std::size_t>(*s);
     map.reserve(new_size);
diff --git a/src/goto-instrument/alignment_checks.cpp b/src/goto-instrument/alignment_checks.cpp
index ff1d63f9d3ed..e708acb33c91 100644
--- a/src/goto-instrument/alignment_checks.cpp
+++ b/src/goto-instrument/alignment_checks.cpp
@@ -36,7 +36,7 @@ void print_struct_alignment_problems(
           it_mem != components.end();
           it_mem++)
       {
-        mp_integer cumulated_length = 0;
+        bytest cumulated_length{0};
         bool first_time_seen_from = true;
 
         // if the instruction cannot be aligned to the address,
diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp
index a2185e2f9ab6..713586cfdb92 100644
--- a/src/goto-instrument/count_eloc.cpp
+++ b/src/goto-instrument/count_eloc.cpp
@@ -186,7 +186,7 @@ void print_global_state_size(const goto_modelt &goto_model)
     }
   }
 
-  mp_integer total_size = 0;
+  bitst total_size{0};
 
   for(const auto &symbol_entry : goto_model.symbol_table.symbols)
   {
@@ -201,7 +201,7 @@ void print_global_state_size(const goto_modelt &goto_model)
     }
 
     const auto bits = pointer_offset_bits(symbol.type, ns);
-    if(bits.has_value() && bits.value() > 0)
+    if(bits.has_value() && bits.value() > bitst{0})
       total_size += bits.value();
   }
 
diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h
index e873546db7ad..d87986aa7fc4 100644
--- a/src/goto-programs/interpreter_class.h
+++ b/src/goto-programs/interpreter_class.h
@@ -287,13 +287,13 @@ class interpretert
 
   bool byte_offset_to_memory_offset(
     const typet &source_type,
-    const mp_integer &byte_offset,
+    const bytest &byte_offset,
     mp_integer &result);
 
   bool memory_offset_to_byte_offset(
     const typet &source_type,
     const mp_integer &cell_offset,
-    mp_integer &result);
+    bytest &result);
 
   mp_vectort evaluate(const exprt &);
 
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 65570975ce9e..d3e1aea16289 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -159,7 +159,7 @@ bool interpretert::count_type_leaves(const typet &ty, mp_integer &result)
 /// \return Offset into a vector of interpreter values; returns true on error
 bool interpretert::byte_offset_to_memory_offset(
   const typet &source_type,
-  const mp_integer &offset,
+  const bytest &offset,
   mp_integer &result)
 {
   if(source_type.id()==ID_struct)
@@ -206,7 +206,7 @@ bool interpretert::byte_offset_to_memory_offset(
 
     mp_integer array_size=array_size_vec[0];
     auto elem_size_bytes = pointer_offset_size(at.element_type(), ns);
-    if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
+    if(!elem_size_bytes.has_value() || *elem_size_bytes == bytest{0})
       return true;
 
     mp_integer elem_size_leaves;
@@ -228,7 +228,7 @@ bool interpretert::byte_offset_to_memory_offset(
   {
     result=0;
     // Can't currently subdivide a primitive.
-    return offset!=0;
+    return offset != bytest{0};
   }
 }
 
@@ -241,7 +241,7 @@ bool interpretert::byte_offset_to_memory_offset(
 bool interpretert::memory_offset_to_byte_offset(
   const typet &source_type,
   const mp_integer &full_cell_offset,
-  mp_integer &result)
+  bytest &result)
 {
   if(source_type.id()==ID_struct)
   {
@@ -255,7 +255,7 @@ bool interpretert::memory_offset_to_byte_offset(
         return true;
       if(component_count>cell_offset)
       {
-        mp_integer subtype_result;
+        bytest subtype_result{0};
         bool ret=memory_offset_to_byte_offset(
           comp.type(), cell_offset, subtype_result);
         const auto member_offset_result =
@@ -292,7 +292,7 @@ bool interpretert::memory_offset_to_byte_offset(
     if(this_idx>=array_size_vec[0])
       return true;
 
-    mp_integer subtype_result;
+    bytest subtype_result{0};
     bool ret = memory_offset_to_byte_offset(
       at.element_type(), full_cell_offset % elem_count, subtype_result);
     result = subtype_result + ((*elem_size) * this_idx);
@@ -301,7 +301,7 @@ bool interpretert::memory_offset_to_byte_offset(
   else
   {
     // Primitive type.
-    result=0;
+    result = bytest{0};
     return full_cell_offset!=0;
   }
 }
@@ -794,9 +794,9 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
         auto obj_type = address_to_symbol(address).type();
 
         mp_integer offset=address_to_offset(address);
-        mp_integer byte_offset;
+        bytest byte_offset{0};
         if(!memory_offset_to_byte_offset(obj_type, offset, byte_offset))
-          return {byte_offset};
+          return {byte_offset.get()};
       }
     }
     return {};
@@ -1071,7 +1071,9 @@ mp_integer interpretert::evaluate_address(
     {
       mp_integer memory_offset;
       if(!byte_offset_to_memory_offset(
-           byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
+           byte_extract_expr.op0().type(),
+           bytest{extract_offset[0]},
+           memory_offset))
         return evaluate_address(byte_extract_expr.op0(), fail_quietly) +
                memory_offset;
     }
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
index fe2e8b941309..a0a8b3f96fbe 100644
--- a/src/goto-programs/vcd_goto_trace.cpp
+++ b/src/goto-programs/vcd_goto_trace.cpp
@@ -100,7 +100,7 @@ void output_vcd(
 
         const auto width = pointer_offset_bits(type, ns);
 
-        if(width.has_value() && (*width) >= 1)
+        if(width.has_value() && (*width) >= bitst{1})
           out << "$var reg " << (*width) << " V" << number << " " << identifier
               << " $end"
               << "\n";
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
index f2c88ae4b1b6..e21c20b2e460 100644
--- a/src/goto-symex/goto_symex.cpp
+++ b/src/goto-symex/goto_symex.cpp
@@ -53,8 +53,8 @@ void goto_symext::symex_assign(
   log.conditional_output(
     log.debug(), [this, &lhs](messaget::mstreamt &mstream) {
       mstream << "Assignment to " << format(lhs) << " ["
-              << pointer_offset_bits(lhs.type(), ns).value_or(0) << " bits]"
-              << messaget::eom;
+              << pointer_offset_bits(lhs.type(), ns).value_or(bitst{0})
+              << " bits]" << messaget::eom;
     });
 
   // rvalues present within the lhs (for example, "some_array[this_rvalue]" or
diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp
index 32aa569e307a..dbb8a25e9d8f 100644
--- a/src/goto-symex/shadow_memory_util.cpp
+++ b/src/goto-symex/shadow_memory_util.cpp
@@ -980,8 +980,7 @@ normalize(const object_descriptor_exprt &expr, const namespacet &ns)
   }
 
   object_descriptor_exprt result = expr;
-  mp_integer offset =
-    numeric_cast_v<mp_integer>(to_constant_expr(expr.offset()));
+  bytest offset = numeric_cast_v<bytest>(to_constant_expr(expr.offset()));
   exprt object = expr.object();
 
   while(true)
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index f20cfc9c4f30..201ff57e1bc6 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -83,9 +83,9 @@ void goto_symext::symex_allocate(
       {
         // Did the size get multiplied?
         auto elem_size = pointer_offset_size(*tmp_type, ns);
-        const auto alloc_size = numeric_cast<mp_integer>(tmp_size);
+        const auto alloc_size = numeric_cast<bytest>(tmp_size);
 
-        if(!elem_size.has_value() || *elem_size==0)
+        if(!elem_size.has_value() || *elem_size == bytest{0})
         {
         }
         else if(
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index f4beccfb669f..67d17eaa5046 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -141,19 +141,18 @@ exprt goto_symext::address_arithmetic(
       result = index_exprt(result, from_integer(0, c_index_type()));
 
     // handle field-sensitive SSA symbol
-    mp_integer offset=0;
+    std::optional<bytest> offset_opt;
     if(is_ssa_expr(expr))
     {
-      auto offset_opt = compute_pointer_offset(expr, ns);
+      offset_opt = compute_pointer_offset(expr, ns);
       PRECONDITION(offset_opt.has_value());
-      offset = *offset_opt;
     }
 
-    if(offset>0)
+    if(offset_opt.has_value() && *offset_opt > bytest{0})
     {
       const byte_extract_exprt be = make_byte_extract(
         to_ssa_expr(expr).get_l1_object(),
-        from_integer(offset, c_index_type()),
+        from_integer(*offset_opt, c_index_type()),
         expr.type());
 
       result = address_arithmetic(be, state, keep_array);
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 404f04fec723..33d2e45d0726 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -500,11 +500,10 @@ void goto_symext::symex_goto(statet &state)
       guardt guard{true_exprt{}, guard_manager};
 
       log.conditional_output(
-        log.debug(),
-        [this, &new_lhs](messaget::mstreamt &mstream) {
-          mstream << "Assignment to " << new_lhs.get_identifier()
-                  << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
-                  << messaget::eom;
+        log.debug(), [this, &new_lhs](messaget::mstreamt &mstream) {
+          mstream << "Assignment to " << new_lhs.get_identifier() << " ["
+                  << pointer_offset_bits(new_lhs.type(), ns).value_or(bitst{0})
+                  << " bits]" << messaget::eom;
         });
 
       target.assignment(
@@ -842,8 +841,8 @@ static void merge_names(
   log.conditional_output(
     log.debug(), [ns, &new_lhs](messaget::mstreamt &mstream) {
       mstream << "Assignment to " << new_lhs.get_identifier() << " ["
-              << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
-              << messaget::eom;
+              << pointer_offset_bits(new_lhs.type(), ns).value_or(bitst{0})
+              << " bits]" << messaget::eom;
     });
 
   target.assignment(
diff --git a/src/goto-synthesizer/cegis_evaluator.cpp b/src/goto-synthesizer/cegis_evaluator.cpp
index bdb3d960dd81..1cb8848f9cac 100644
--- a/src/goto-synthesizer/cegis_evaluator.cpp
+++ b/src/goto-synthesizer/cegis_evaluator.cpp
@@ -230,7 +230,7 @@ mp_integer cegis_evaluatort::evaluate_rec_int(
   {
     if(cex.object_sizes.find(expr.operands()[0]) != cex.object_sizes.end())
     {
-      result = cex.object_sizes.at(expr.operands()[0]);
+      result = cex.object_sizes.at(expr.operands()[0]).get();
     }
     else
     {
@@ -268,7 +268,7 @@ mp_integer cegis_evaluatort::evaluate_rec_int(
       {
         // Use havoc values only if we are evaluating the expression against
         // the negative example---is_positive is false.
-        result = cex.havoced_pointer_offsets.at(expr.operands()[0]);
+        result = cex.havoced_pointer_offsets.at(expr.operands()[0]).get();
       }
       else if(
         cex.loop_entry_offsets.find(expr.operands()[0]) !=
@@ -276,7 +276,7 @@ mp_integer cegis_evaluatort::evaluate_rec_int(
       {
         // The pointer is not havoced. So look up the offset in the loop-entry
         // set instead.
-        result = cex.loop_entry_offsets.at(expr.operands()[0]);
+        result = cex.loop_entry_offsets.at(expr.operands()[0]).get();
       }
       else
       {
@@ -292,7 +292,8 @@ mp_integer cegis_evaluatort::evaluate_rec_int(
         cex.loop_entry_offsets.find(expr.operands()[0].operands()[0]) !=
         cex.loop_entry_offsets.end())
       {
-        result = cex.loop_entry_offsets.at(expr.operands()[0].operands()[0]);
+        result =
+          cex.loop_entry_offsets.at(expr.operands()[0].operands()[0]).get();
       }
       else
       {
diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp
index 57bbfdf30fbb..c8a323565e00 100644
--- a/src/goto-synthesizer/cegis_verifier.cpp
+++ b/src/goto-synthesizer/cegis_verifier.cpp
@@ -366,13 +366,13 @@ cext cegis_verifiert::build_cex(
   const source_locationt &loop_entry_loc)
 {
   // Valuations of havoced variables right after havoc instructions.
-  std::unordered_map<exprt, mp_integer, irep_hash> object_sizes;
+  std::unordered_map<exprt, bytest, irep_hash> object_sizes;
   std::unordered_map<exprt, mp_integer, irep_hash> havoced_values;
-  std::unordered_map<exprt, mp_integer, irep_hash> havoced_pointer_offsets;
+  std::unordered_map<exprt, bytest, irep_hash> havoced_pointer_offsets;
 
   // Loop-entry valuations of havoced variables.
   std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_values;
-  std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_offsets;
+  std::unordered_map<exprt, bytest, irep_hash> loop_entry_offsets;
 
   // Live variables upon the loop head.
   std::set<exprt> live_variables;
@@ -438,8 +438,8 @@ cext cegis_verifiert::build_cex(
               step.full_lhs_value.get_string(ID_value), width, is_signed);
           }
 
-          // Store the value into the the map for havoced value if this step
-          // is a loop havocing instruction.
+          // Store the value into the map for havoced value if this step is a
+          // loop havocing instruction.
           if(loop_havoc_set.count(step.pc))
           {
             havoced_values[step.full_lhs] = bvrep2integer(
@@ -459,12 +459,7 @@ cext cegis_verifiert::build_cex(
               step.full_lhs_value);
 
           pointer_arithmetict pointer_arithmetic(
-            pointer_constant_expr->symbolic_pointer());
-          if(pointer_constant_expr->symbolic_pointer().id() == ID_typecast)
-          {
-            pointer_arithmetic = pointer_arithmetict(
-              pointer_constant_expr->symbolic_pointer().operands()[0]);
-          }
+            skip_typecast(pointer_constant_expr->symbolic_pointer()));
 
           // Extract object size.
           exprt &underlying_array = pointer_arithmetic.pointer;
@@ -481,33 +476,33 @@ cext cegis_verifiert::build_cex(
             }
             UNREACHABLE;
           }
-          mp_integer object_size =
+          bytest object_size =
             pointer_offset_size(to_array_type(underlying_array.type()), ns)
               .value();
-          object_sizes[step.full_lhs] = object_size;
+          object_sizes.emplace(step.full_lhs, object_size);
 
           // Extract offsets.
-          mp_integer offset = 0;
+          bytest offset{0};
           if(pointer_arithmetic.offset.is_not_nil())
           {
             constant_exprt offset_expr =
               expr_dynamic_cast<constant_exprt>(pointer_arithmetic.offset);
-            offset = bvrep2integer(
-              offset_expr.get_value(), size_type().get_width(), false);
+            offset = bytest{bvrep2integer(
+              offset_expr.get_value(), size_type().get_width(), false)};
           }
 
           // Store the offset into the map for loop_entry if we haven't
           // entered the loop.
           if(!entered_loop)
           {
-            loop_entry_offsets[step.full_lhs] = offset;
+            loop_entry_offsets.emplace(step.full_lhs, offset);
           }
 
-          // Store the offset into the the map for havoced offset if this step
-          // is a loop havocing instruction.
+          // Store the offset into the map for havoced offset if this step is a
+          // loop havocing instruction.
           if(loop_havoc_set.count(step.pc))
           {
-            havoced_pointer_offsets[step.full_lhs] = offset;
+            havoced_pointer_offsets.emplace(step.full_lhs, offset);
           }
         }
       }
diff --git a/src/goto-synthesizer/cegis_verifier.h b/src/goto-synthesizer/cegis_verifier.h
index dc1e1aaa5be3..0655eb46687a 100644
--- a/src/goto-synthesizer/cegis_verifier.h
+++ b/src/goto-synthesizer/cegis_verifier.h
@@ -43,12 +43,11 @@ class cext
   };
 
   cext(
-    const std::unordered_map<exprt, mp_integer, irep_hash> &object_sizes,
+    const std::unordered_map<exprt, bytest, irep_hash> &object_sizes,
     const std::unordered_map<exprt, mp_integer, irep_hash> &havoced_values,
-    const std::unordered_map<exprt, mp_integer, irep_hash>
-      &havoced_pointer_offsets,
+    const std::unordered_map<exprt, bytest, irep_hash> &havoced_pointer_offsets,
     const std::unordered_map<exprt, mp_integer, irep_hash> &loop_entry_values,
-    const std::unordered_map<exprt, mp_integer, irep_hash> &loop_entry_offsets,
+    const std::unordered_map<exprt, bytest, irep_hash> &loop_entry_offsets,
     const std::set<exprt> &live_variables)
     : object_sizes(object_sizes),
       havoced_values(havoced_values),
@@ -75,17 +74,17 @@ class cext
   // and pointer offsets.
 
   // __CPROVER_OBJECT_SIZE
-  std::unordered_map<exprt, mp_integer, irep_hash> object_sizes;
+  std::unordered_map<exprt, bytest, irep_hash> object_sizes;
   // all the valuation of havoced variables with primitive type.
   std::unordered_map<exprt, mp_integer, irep_hash> havoced_values;
   // __CPROVER_POINTER_OFFSET
-  std::unordered_map<exprt, mp_integer, irep_hash> havoced_pointer_offsets;
+  std::unordered_map<exprt, bytest, irep_hash> havoced_pointer_offsets;
 
   // We also collect loop-entry evaluations of havoced variables.
   // __CPROVER_loop_entry
   std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_values;
   // __CPROVER_POINTER_OFFSET(__CPROVER_loop_entry( ))
-  std::unordered_map<exprt, mp_integer, irep_hash> loop_entry_offsets;
+  std::unordered_map<exprt, bytest, irep_hash> loop_entry_offsets;
 
   // Set of live variables upon loop head.
   std::set<exprt> live_variables;
diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp
index 645ec3c27258..2698c3356a3d 100644
--- a/src/memory-analyzer/analyze_symbol.cpp
+++ b/src/memory-analyzer/analyze_symbol.cpp
@@ -34,7 +34,7 @@ gdb_value_extractort::gdb_value_extractort(
 
 gdb_value_extractort::memory_scopet::memory_scopet(
   const memory_addresst &begin,
-  const mp_integer &byte_size,
+  const bytest &byte_size,
   const irep_idt &name)
   : begin_int(safe_string2size_t(begin.address_string, 0)),
     byte_size(byte_size),
@@ -48,13 +48,14 @@ size_t gdb_value_extractort::memory_scopet::address2size_t(
   return safe_string2size_t(point.address_string, 0);
 }
 
-mp_integer gdb_value_extractort::memory_scopet::distance(
+bytest gdb_value_extractort::memory_scopet::distance(
   const memory_addresst &point,
-  mp_integer member_size) const
+  bytest member_size) const
 {
   auto point_int = address2size_t(point);
   CHECK_RETURN(check_containment(point_int));
-  return (point_int - begin_int) / member_size;
+  return bytest{
+    (point_int - begin_int) / numeric_cast_v<std::size_t>(member_size)};
 }
 
 std::vector<gdb_value_extractort::memory_scopet>::iterator
@@ -77,18 +78,18 @@ gdb_value_extractort::find_dynamic_allocation(const memory_addresst &point)
     });
 }
 
-mp_integer gdb_value_extractort::get_malloc_size(irep_idt name)
+bytest gdb_value_extractort::get_malloc_size(irep_idt name)
 {
   const auto scope_it = find_dynamic_allocation(name);
   if(scope_it == dynamically_allocated.end())
-    return 1;
+    return bytest{1};
   else
     return scope_it->size();
 }
 
 std::optional<std::string> gdb_value_extractort::get_malloc_pointee(
   const memory_addresst &point,
-  mp_integer member_size)
+  const bytest &member_size)
 {
   const auto scope_it = find_dynamic_allocation(point);
   if(scope_it == dynamically_allocated.end())
@@ -96,14 +97,16 @@ std::optional<std::string> gdb_value_extractort::get_malloc_pointee(
 
   const auto pointer_distance = scope_it->distance(point, member_size);
   return id2string(scope_it->id()) +
-         (pointer_distance > 0 ? "+" + integer2string(pointer_distance) : "");
+         (pointer_distance > bytest{0}
+            ? "+" + integer2string(pointer_distance.get())
+            : "");
 }
 
-mp_integer gdb_value_extractort::get_type_size(const typet &type) const
+bytest gdb_value_extractort::get_type_size(const typet &type) const
 {
   const auto maybe_size = pointer_offset_bits(type, ns);
   CHECK_RETURN(maybe_size.has_value());
-  return *maybe_size / CHAR_BIT;
+  return bits_to_bytes_trunc(*maybe_size, CHAR_BIT);
 }
 
 void gdb_value_extractort::analyze_symbols(
@@ -134,7 +137,7 @@ void gdb_value_extractort::analyze_symbols(
 
       if(symbol_size > 1)
         dynamically_allocated.emplace_back(
-          symbol_value.address, symbol_size, id);
+          symbol_value.address, bytest{symbol_size}, id);
       memory_map[id] = symbol_value;
     }
   }
@@ -312,7 +315,8 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
     return index_exprt{
       struct_symbol_expr,
       from_integer(
-        member_offset / get_type_size(to_pointer_type(expr.type()).base_type()),
+        bytest{member_offset} /
+          get_type_size(to_pointer_type(expr.type()).base_type()),
         c_index_type())};
   }
   if(struct_symbol->type.id() == ID_pointer)
@@ -325,7 +329,7 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
 
   const auto maybe_member_expr = get_subexpression_at_offset(
     struct_symbol_expr,
-    member_offset,
+    bytest{member_offset},
     to_pointer_type(expr.type()).base_type(),
     ns);
   DATA_INVARIANT(
@@ -396,10 +400,10 @@ exprt gdb_value_extractort::get_non_char_pointer_value(
     // expected positions. Since the allocated size is an over-approximation we
     // may end up querying past the allocated bounds and building a larger array
     // with meaningless values.
-    mp_integer allocated_size = get_malloc_size(c_converter.convert(expr));
+    bytest allocated_size = get_malloc_size(c_converter.convert(expr));
     // get the sizeof(target_type) and thus the number of elements
     const auto number_of_elements = allocated_size / get_type_size(target_type);
-    if(allocated_size != 1 && number_of_elements > 1)
+    if(allocated_size != bytest{1} && number_of_elements > 1)
     {
       array_exprt::operandst elements;
       // build the operands by querying for an index expression
@@ -554,7 +558,10 @@ exprt gdb_value_extractort::get_pointer_value(
     if(target_expr.type().id() == ID_array)
     {
       const auto result_indexed_expr = get_subexpression_at_offset(
-        target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
+        target_expr,
+        bytest{0},
+        to_pointer_type(zero_expr.type()).base_type(),
+        ns);
       CHECK_RETURN(result_indexed_expr.has_value());
       if(result_indexed_expr->type() == zero_expr.type())
         return *result_indexed_expr;
diff --git a/src/memory-analyzer/analyze_symbol.h b/src/memory-analyzer/analyze_symbol.h
index e37f6fe6765f..54f05cadc5da 100644
--- a/src/memory-analyzer/analyze_symbol.h
+++ b/src/memory-analyzer/analyze_symbol.h
@@ -95,7 +95,7 @@ class gdb_value_extractort
   {
   private:
     size_t begin_int;
-    mp_integer byte_size;
+    bytest byte_size;
     irep_idt name;
 
     /// Convert base-16 memory address to a natural number
@@ -108,13 +108,14 @@ class gdb_value_extractort
     /// \return true if the point is inside this scope
     bool check_containment(const size_t &point_int) const
     {
-      return point_int >= begin_int && (begin_int + byte_size) > point_int;
+      return point_int >= begin_int &&
+             (bytest{begin_int} + byte_size) > bytest{point_int};
     }
 
   public:
     memory_scopet(
       const memory_addresst &begin,
-      const mp_integer &byte_size,
+      const bytest &byte_size,
       const irep_idt &name);
 
     /// Check if \p point points somewhere in this memory scope
@@ -129,8 +130,7 @@ class gdb_value_extractort
     /// \param point: memory address to have the offset computed
     /// \param member_size: size of one element of this scope in bytes
     /// \return `n' such that \p point is the n-th element of this scope
-    mp_integer
-    distance(const memory_addresst &point, mp_integer member_size) const;
+    bytest distance(const memory_addresst &point, bytest member_size) const;
 
     /// Getter for the name of this memory scope
     /// \return the name as irep id
@@ -141,7 +141,7 @@ class gdb_value_extractort
 
     /// Getter for the allocation size of this memory scope
     /// \return the size in bytes
-    mp_integer size() const
+    bytest size() const
     {
       return byte_size;
     }
@@ -172,7 +172,7 @@ class gdb_value_extractort
   /// Search for the size of the allocated memory for \p name
   /// \param name: name of the pointer used during allocation
   /// \return the size if have a record of \p name's allocation (1 otherwise)
-  mp_integer get_malloc_size(irep_idt name);
+  bytest get_malloc_size(irep_idt name);
 
   /// Build the pointee string for address \p point assuming it points to a
   ///   dynamic allocation of `n' elements each of size \p member_size. E.g.:
@@ -186,12 +186,12 @@ class gdb_value_extractort
   /// \param member_size: size of each allocated element
   /// \return pointee as a string if we have a record of the allocation
   std::optional<std::string>
-  get_malloc_pointee(const memory_addresst &point, mp_integer member_size);
+  get_malloc_pointee(const memory_addresst &point, const bytest &member_size);
 
   /// Wrapper for call get_offset_pointer_bits
   /// \param type: type to get the size of
   /// \return the size of the type in bytes
-  mp_integer get_type_size(const typet &type) const;
+  bytest get_type_size(const typet &type) const;
 
   /// Assign the gdb-extracted value for \p symbol_name to its symbol
   ///   expression and then process outstanding assignments that this
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index ca0ef7a0cbbe..1a8e1281cf5d 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -348,7 +348,7 @@ bool value_sett::eval_pointer_offset(
       get_value_set(to_pointer_offset_expr(expr).pointer(), ns, true);
 
     exprt new_expr;
-    mp_integer previous_offset=0;
+    bytest previous_offset{0};
 
     const object_map_dt &object_map=reference_set.read();
     for(object_map_dt::const_iterator
@@ -625,7 +625,7 @@ void value_sett::get_value_set_rec(
       insert(
         dest,
         exprt(ID_null_object, to_pointer_type(expr_type).base_type()),
-        mp_integer{0});
+        bytest{0});
     }
     else if(expr_type.id()==ID_unsignedbv ||
             expr_type.id()==ID_signedbv)
@@ -657,7 +657,7 @@ void value_sett::get_value_set_rec(
 
       if(op.is_zero())
       {
-        insert(dest, exprt(ID_null_object, empty_typet{}), mp_integer{0});
+        insert(dest, exprt(ID_null_object, empty_typet{}), bytest{0});
       }
       else
       {
@@ -745,13 +745,13 @@ void value_sett::get_value_set_rec(
 
         auto size = pointer_offset_size(pointer_base_type, ns);
 
-        if(!size.has_value() || (*size) == 0)
+        if(!size.has_value() || (*size) == bytest{0})
         {
           i.reset();
         }
         else
         {
-          *i *= *size;
+          *i *= size->get();
 
           if(expr.id()==ID_minus)
           {
@@ -793,7 +793,7 @@ void value_sett::get_value_set_rec(
 
       // adjust by offset
       if(offset && i.has_value())
-        *offset += *i;
+        *offset += bytest{*i};
       else
         offset.reset();
 
@@ -873,7 +873,7 @@ void value_sett::get_value_set_rec(
       dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
-      insert(dest, dynamic_object, mp_integer{0});
+      insert(dest, dynamic_object, bytest{0});
     }
     else if(statement==ID_cpp_new ||
             statement==ID_cpp_new_array)
@@ -886,7 +886,7 @@ void value_sett::get_value_set_rec(
       dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
-      insert(dest, dynamic_object, mp_integer{0});
+      insert(dest, dynamic_object, bytest{0});
     }
     else
       insert(dest, exprt(ID_unknown, original_type));
@@ -1112,7 +1112,7 @@ void value_sett::get_value_set_rec(
       if(eval_pointer_offset(offset, ns))
         simplify(offset, ns);
 
-      const auto offset_int = numeric_cast<mp_integer>(offset);
+      const auto offset_int = numeric_cast<bytest>(offset);
       const auto type_size = pointer_offset_size(expr.type(), ns);
 
       const struct_typet &struct_type = to_struct_type(op_type);
@@ -1317,7 +1317,7 @@ void value_sett::get_reference_set_rec(
       to_array_type(expr.type()).element_type().id() == ID_array)
       insert(dest, expr);
     else
-      insert(dest, expr, mp_integer{0});
+      insert(dest, expr, bytest{0});
 
     return;
   }
@@ -1346,7 +1346,7 @@ void value_sett::get_reference_set_rec(
 
     const index_exprt &index_expr=to_index_expr(expr);
     const exprt &array=index_expr.array();
-    const exprt &offset=index_expr.index();
+    const exprt &index = index_expr.index();
 
     DATA_INVARIANT(
       array.type().id() == ID_array, "index takes array-typed operand");
@@ -1374,19 +1374,19 @@ void value_sett::get_reference_set_rec(
           from_integer(0, c_index_type()));
 
         offsett o = a_it->second;
-        const auto i = numeric_cast<mp_integer>(offset);
+        const auto i = numeric_cast<mp_integer>(index);
 
-        if(offset.is_zero())
+        if(index.is_zero())
         {
         }
         else if(i.has_value() && o)
         {
           auto size = pointer_offset_size(array_type.element_type(), ns);
 
-          if(!size.has_value() || *size == 0)
+          if(!size.has_value() || *size == bytest{0})
             o.reset();
           else
-            *o = *i * (*size);
+            *o = bytest{*i * (*size)};
         }
         else
           o.reset();
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 5c71946acd8b..c2811ededaec 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <unordered_set>
 
-#include <util/mp_arith.h>
 #include <util/reference_counting.h>
 #include <util/sharing_map.h>
 
@@ -78,7 +77,7 @@ class value_sett
 
   /// Represents the offset into an object: either a unique integer offset,
   /// or an unknown value, represented by `!offset`.
-  typedef std::optional<mp_integer> offsett;
+  typedef std::optional<bytest> offsett;
 
   /// Represents a set of expressions (`exprt` instances) with corresponding
   /// offsets (`offsett` instances). This is the RHS set of a single row of
@@ -146,10 +145,8 @@ class value_sett
   /// \param dest: object map to update
   /// \param src: expression to add
   /// \param offset_value: offset into `src`
-  bool insert(
-    object_mapt &dest,
-    const exprt &src,
-    const mp_integer &offset_value) const
+  bool
+  insert(object_mapt &dest, const exprt &src, const bytest &offset_value) const
   {
     return insert(dest, object_numbering.number(src), offsett(offset_value));
   }
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index f36cc67b453d..98d916f08a4c 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -619,12 +619,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       auto element_size =
         pointer_offset_size(to_array_type(root_object_type).element_type(), ns);
       CHECK_RETURN(element_size.has_value());
-      CHECK_RETURN(*element_size > 0);
+      CHECK_RETURN(*element_size > bytest{0});
 
-      const auto offset_int =
-        numeric_cast_v<mp_integer>(to_constant_expr(offset));
+      const auto offset_int = numeric_cast_v<bytest>(to_constant_expr(offset));
 
-      if(offset_int % *element_size == 0)
+      if(offset_int % *element_size == bytest{0})
       {
         index_exprt index_expr{
           root_object,
@@ -774,14 +773,14 @@ bool value_set_dereferencet::memory_model_bytes(
   auto from_type_element_type_size =
     from_type.id() == ID_array
       ? pointer_offset_size(to_array_type(from_type).element_type(), ns)
-      : std::optional<mp_integer>{};
+      : std::optional<bytest>{};
 
   auto to_type_size = pointer_offset_size(to_type, ns);
 
   if(
     from_type.id() == ID_array && from_type_element_type_size.has_value() &&
-    *from_type_element_type_size == 1 && to_type_size.has_value() &&
-    *to_type_size == 1 &&
+    *from_type_element_type_size == bytest{1} && to_type_size.has_value() &&
+    *to_type_size == bytest{1} &&
     is_a_bv_type(to_array_type(from_type).element_type()) &&
     is_a_bv_type(to_type))
   {
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index 01cb688063f1..2d0164098f11 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -61,13 +61,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   // see if the byte number is constant and within bounds, else work from the
   // root object
   const auto op_bytes_opt = pointer_offset_size(expr.op().type(), ns);
-  auto index = numeric_cast<mp_integer>(expr.offset());
+  auto index = numeric_cast<bytest>(expr.offset());
 
   if(
-    (!index.has_value() || !op_bytes_opt.has_value() ||
-     *index < 0 || *index >= *op_bytes_opt) &&
-    (expr.op().id() == ID_member ||
-     expr.op().id() == ID_index ||
+    (!index.has_value() || !op_bytes_opt.has_value() || *index < bytest{0} ||
+     *index >= *op_bytes_opt) &&
+    (expr.op().id() == ID_member || expr.op().id() == ID_index ||
      expr.op().id() == ID_byte_extract_big_endian ||
      expr.op().id() == ID_byte_extract_little_endian))
   {
@@ -106,14 +105,17 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   // see if the byte number is constant
   if(index.has_value())
   {
-    const mp_integer offset = *index * expr.get_bits_per_byte();
+    const bitst offset = bytes_to_bits(*index, expr.get_bits_per_byte());
 
     for(std::size_t i=0; i<width; i++)
+    {
+      const bitst offset_plus_i = offset + bitst{i};
       // out of bounds?
-      if(offset + i < 0 || offset + i >= op_bv.size())
+      if(offset_plus_i < bitst{0} || offset_plus_i >= bitst{op_bv.size()})
         bv[i]=prop.new_variable();
       else
-        bv[i] = op_bv[numeric_cast_v<std::size_t>(offset + i)];
+        bv[i] = op_bv[numeric_cast_v<std::size_t>(offset_plus_i)];
+    }
   }
   else
   {
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index e40162aa1f26..9736e601fb3b 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -304,7 +304,8 @@ std::optional<bvt> bv_pointerst::convert_address_of_rec(const exprt &expr)
     const std::size_t bits = boolbv_width(type);
     CHECK_RETURN(bv_opt->size() == bits);
 
-    bvt bv = offset_arithmetic(type, *bv_opt, 1, byte_extract_expr.offset());
+    bvt bv =
+      offset_arithmetic(type, *bv_opt, bytest{1}, byte_extract_expr.offset());
     CHECK_RETURN(bv.size()==bits);
     return std::move(bv);
   }
@@ -453,7 +454,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     bvt bv;
 
-    mp_integer size=0;
+    bytest size{0};
     std::size_t count=0;
 
     for(const auto &op : plus_expr.operands())
@@ -469,7 +470,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
           pointer_base_type.id() != ID_empty,
           "no pointer arithmetic over void pointers");
         auto size_opt = pointer_offset_size(pointer_base_type, ns);
-        CHECK_RETURN(size_opt.has_value() && *size_opt >= 0);
+        CHECK_RETURN(size_opt.has_value() && *size_opt >= bytest{0});
         size = *size_opt;
       }
     }
@@ -534,7 +535,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       pointer_base_type.id() != ID_empty,
       "no pointer arithmetic over void pointers");
     auto element_size_opt = pointer_offset_size(pointer_base_type, ns);
-    CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+    CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > bytest{0});
     return offset_arithmetic(type, bv, *element_size_opt, neg_op1);
   }
   else if(expr.id()==ID_byte_extract_little_endian ||
@@ -585,7 +586,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     // get element size
     auto size = pointer_offset_size(element_address_expr.element_type(), ns);
-    CHECK_RETURN(size.has_value() && *size >= 0);
+    CHECK_RETURN(size.has_value() && *size >= bytest{0});
 
     // add offset
     bv = offset_arithmetic(
@@ -646,11 +647,13 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
         lhs_pt.base_type().id() != ID_empty,
         "no pointer arithmetic over void pointers");
       auto element_size_opt = pointer_offset_size(lhs_pt.base_type(), ns);
-      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+      CHECK_RETURN(
+        element_size_opt.has_value() && *element_size_opt > bytest{0});
 
-      if(*element_size_opt != 1)
+      if(*element_size_opt != bytest{1})
       {
-        bvt element_size_bv = bv_utils.build_constant(*element_size_opt, width);
+        bvt element_size_bv =
+          bv_utils.build_constant(element_size_opt->get(), width);
         difference = bv_utils.divider(
           difference, element_size_bv, bv_utilst::representationt::SIGNED);
       }
@@ -802,7 +805,7 @@ exprt bv_pointerst::bv_get_rec(
 
   pointer_logict::pointert pointer{
     numeric_cast_v<std::size_t>(binary2integer(value_addr, false)),
-    binary2integer(value_offset, false)};
+    bytest{binary2integer(value_offset, false)}};
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};
@@ -823,18 +826,18 @@ bvt bv_pointerst::encode(const mp_integer &addr, const pointer_typet &type)
 bvt bv_pointerst::offset_arithmetic(
   const pointer_typet &type,
   const bvt &bv,
-  const mp_integer &x)
+  const bytest &x)
 {
   const std::size_t offset_bits = get_offset_width(type);
 
   return offset_arithmetic(
-    type, bv, 1, bv_utils.build_constant(x, offset_bits));
+    type, bv, bytest{1}, bv_utils.build_constant(x.get(), offset_bits));
 }
 
 bvt bv_pointerst::offset_arithmetic(
   const pointer_typet &type,
   const bvt &bv,
-  const mp_integer &factor,
+  const bytest &factor,
   const exprt &index)
 {
   bvt bv_index=convert_bv(index);
@@ -868,22 +871,22 @@ bvt bv_pointerst::offset_arithmetic(
   const std::size_t offset_bits = get_offset_width(type);
   bv_index = bv_utils.extension(bv_index, offset_bits, rep);
 
-  return offset_arithmetic(type, bv, 1, bv_index);
+  return offset_arithmetic(type, bv, bytest{1}, bv_index);
 }
 
 bvt bv_pointerst::offset_arithmetic(
   const pointer_typet &type,
   const bvt &bv,
-  const mp_integer &factor,
+  const bytest &factor,
   const bvt &index)
 {
   bvt bv_index;
 
-  if(factor==1)
+  if(factor == bytest{1})
     bv_index=index;
   else
   {
-    bvt bv_factor=bv_utils.build_constant(factor, index.size());
+    bvt bv_factor = bv_utils.build_constant(factor.get(), index.size());
     bv_index = bv_utils.signed_multiplier(index, bv_factor);
   }
 
diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h
index 4486351fde07..2db42f4d62b8 100644
--- a/src/solvers/flattening/bv_pointers.h
+++ b/src/solvers/flattening/bv_pointers.h
@@ -54,11 +54,11 @@ class bv_pointerst:public boolbvt
   [[nodiscard]] std::optional<bvt> convert_address_of_rec(const exprt &);
 
   [[nodiscard]] bvt
-  offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
+  offset_arithmetic(const pointer_typet &, const bvt &, const bytest &);
   [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
-    const mp_integer &factor,
+    const bytest &factor,
     const exprt &index);
   [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &type,
@@ -68,7 +68,7 @@ class bv_pointerst:public boolbvt
   [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
-    const mp_integer &factor,
+    const bytest &factor,
     const bvt &index_bv);
 
   struct postponedt
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index c5b866d6104b..f70c09a98f43 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -61,7 +61,7 @@ exprt pointer_logict::pointer_expr(
   const mp_integer &object,
   const pointer_typet &type) const
 {
-  return pointer_expr({object, 0}, type);
+  return pointer_expr({object, bytest{0}}, type);
 }
 
 exprt pointer_logict::pointer_expr(
@@ -70,7 +70,7 @@ exprt pointer_logict::pointer_expr(
 {
   if(pointer.object==null_object) // NULL?
   {
-    if(pointer.offset==0)
+    if(pointer.offset == bytest{0})
     {
       return null_pointer_exprt(type);
     }
@@ -106,8 +106,9 @@ exprt pointer_logict::pointer_expr(
 
     // a string constant must be array-typed with fixed size
     const array_typet &array_type = to_array_type(object_expr.type());
-    mp_integer array_size =
-      numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
+    // each array element is one byte
+    const bytest array_size =
+      numeric_cast_v<bytest>(to_constant_expr(array_type.size()));
     if(array_size > pointer.offset)
     {
       to_array_type(subtype).size() =
@@ -133,13 +134,13 @@ exprt pointer_logict::pointer_expr(
     return typecast_exprt::conditional_cast(base, type);
 
   const auto object_size = pointer_offset_size(be.op().type(), ns);
-  if(object_size.has_value() && *object_size <= 1)
+  if(object_size.has_value() && *object_size <= bytest{1})
   {
     return typecast_exprt::conditional_cast(
       plus_exprt(base, from_integer(pointer.offset, pointer_diff_type())),
       type);
   }
-  else if(object_size.has_value() && pointer.offset % *object_size == 0)
+  else if(object_size.has_value() && pointer.offset % *object_size == bytest{0})
   {
     return typecast_exprt::conditional_cast(
       plus_exprt(
diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h
index bcfd97b7a1f7..ec8a340713b0 100644
--- a/src/solvers/flattening/pointer_logic.h
+++ b/src/solvers/flattening/pointer_logic.h
@@ -27,9 +27,10 @@ class pointer_logict
 
   struct pointert
   {
-    mp_integer object, offset;
+    mp_integer object;
+    bytest offset;
 
-    pointert(mp_integer _obj, mp_integer _off)
+    pointert(mp_integer _obj, bytest _off)
       : object(std::move(_obj)), offset(std::move(_off))
     {
     }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 5b7ab53c4ea5..18b357f4d158 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -744,7 +744,8 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
 
     // split into object and offset
     mp_integer pow=power(2, width-config.bv_encoding.object_bits);
-    pointer_logict::pointert ptr{numeric_cast_v<std::size_t>(v / pow), v % pow};
+    pointer_logict::pointert ptr{
+      numeric_cast_v<std::size_t>(v / pow), bytest{v % pow}};
     return annotated_pointer_constant_exprt(
       bv_expr.get_value(),
       pointer_logic.pointer_expr(ptr, to_pointer_type(type)));
@@ -851,7 +852,7 @@ void smt2_convt::convert_address_of_rec(
     const irep_idt &component_name = member_expr.get_component_name();
 
     const auto offset = member_offset(struct_type, component_name, ns);
-    CHECK_RETURN(offset.has_value() && *offset >= 0);
+    CHECK_RETURN(offset.has_value() && *offset >= bytest{0});
 
     unsignedbv_typet index_type(boolbv_width(result_type));
 
@@ -1583,8 +1584,8 @@ void smt2_convt::convert_expr(const exprt &expr)
 
       if(shift_expr.distance().type().id() == ID_integer)
       {
-        const mp_integer i =
-          numeric_cast_v<mp_integer>(to_constant_expr(shift_expr.distance()));
+        const auto i =
+          numeric_cast_v<bitst>(to_constant_expr(shift_expr.distance()));
 
         // shift distance must be bit vector
         std::size_t width_op0 = boolbv_width(shift_expr.op().type());
@@ -1647,7 +1648,7 @@ void smt2_convt::convert_expr(const exprt &expr)
 
       out << ' ';
 
-      auto distance_int_op = numeric_cast<mp_integer>(shift_expr.distance());
+      auto distance_int_op = numeric_cast<bitst>(shift_expr.distance());
 
       if(distance_int_op.has_value())
       {
@@ -1799,8 +1800,8 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     if(extractbit_expr.index().is_constant())
     {
-      const mp_integer i =
-        numeric_cast_v<mp_integer>(to_constant_expr(extractbit_expr.index()));
+      const auto i =
+        numeric_cast_v<bitst>(to_constant_expr(extractbit_expr.index()));
 
       out << "(= ((_ extract " << i << " " << i << ") ";
       flatten2bv(extractbit_expr.src());
@@ -1825,10 +1826,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>(to_constant_expr(extractbits_expr.upper()));
-      mp_integer op2_i =
-        numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.lower()));
+      auto op1_i =
+        numeric_cast_v<bitst>(to_constant_expr(extractbits_expr.upper()));
+      auto op2_i =
+        numeric_cast_v<bitst>(to_constant_expr(extractbits_expr.lower()));
 
       if(op2_i>op1_i)
         std::swap(op1_i, op2_i);
@@ -3675,8 +3676,9 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
         base_type.id() != ID_empty, "no pointer arithmetic over void pointers");
 
       auto element_size_opt = pointer_offset_size(base_type, ns);
-      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 0);
-      mp_integer element_size = *element_size_opt;
+      CHECK_RETURN(
+        element_size_opt.has_value() && *element_size_opt >= bytest{0});
+      bytest element_size = *element_size_opt;
 
       // First convert the pointer operand
       out << "(let ((?pointerop ";
@@ -3693,7 +3695,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
           << ") ?pointerop) ";
       out << "(bvadd ((_ extract " << offset_bits - 1 << " 0) ?pointerop) ";
 
-      if(element_size >= 2)
+      if(element_size >= bytest{2})
       {
         out << "(bvmul ((_ extract " << offset_bits - 1 << " 0) ";
         convert_expr(i);
@@ -3834,10 +3836,11 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
       DATA_INVARIANT(
         base_type.id() != ID_empty, "no pointer arithmetic over void pointers");
       auto element_size_opt = pointer_offset_size(base_type, ns);
-      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt >= 1);
-      mp_integer element_size = *element_size_opt;
+      CHECK_RETURN(
+        element_size_opt.has_value() && *element_size_opt >= bytest{1});
+      bytest element_size = *element_size_opt;
 
-      if(element_size >= 2)
+      if(element_size >= bytest{2})
         out << "(bvsdiv ";
 
       INVARIANT(
@@ -3851,7 +3854,7 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
       convert_expr(expr.op1());
       out << ")";
 
-      if(element_size >= 2)
+      if(element_size >= bytest{2})
         out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
             << "))";
     }
diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h
index cfebbce7795d..5e99e2d89a95 100644
--- a/src/util/arith_tools.h
+++ b/src/util/arith_tools.h
@@ -54,6 +54,28 @@ struct numeric_castt<mp_integer> final
   }
 };
 
+template <typename Tag>
+struct numeric_castt<named_mp_integert<Tag>> final
+{
+  std::optional<named_mp_integert<Tag>> operator()(const exprt &expr) const
+  {
+    if(expr.id() != ID_constant)
+      return {};
+    else
+      return operator()(to_constant_expr(expr));
+  }
+
+  std::optional<named_mp_integert<Tag>>
+  operator()(const constant_exprt &expr) const
+  {
+    mp_integer out;
+    if(to_integer(expr, out))
+      return {};
+    else
+      return named_mp_integert<Tag>{out};
+  }
+};
+
 /// Convert mp_integer or expr to any integral type
 template <typename T>
 struct numeric_castt<T,
@@ -139,6 +161,14 @@ Target numeric_cast_v(const mp_integer &arg)
   return *maybe;
 }
 
+template <typename Target, typename Tag>
+Target numeric_cast_v(const named_mp_integert<Tag> &arg)
+{
+  const auto maybe = numeric_castt<Target>{}(arg.get());
+  INVARIANT(maybe, "bits should be convertible to target integral type");
+  return *maybe;
+}
+
 /// Convert an expression to integral type Target
 /// An invariant will fail if the conversion is not possible.
 /// \tparam Target: type to convert to
@@ -157,6 +187,12 @@ Target numeric_cast_v(const constant_exprt &arg)
 
 // PRECONDITION(false) in case of unsupported type
 constant_exprt from_integer(const mp_integer &int_value, const typet &type);
+template <typename Tag>
+inline constant_exprt
+from_integer(const named_mp_integert<Tag> &int_value, const typet &type)
+{
+  return from_integer(int_value.get(), type);
+}
 
 // ceil(log2(size))
 std::size_t address_bits(const mp_integer &size);
diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp
index 2b18e322f59c..37c02c426572 100644
--- a/src/util/c_types.cpp
+++ b/src/util/c_types.cpp
@@ -296,12 +296,12 @@ std::string c_type_as_string(const irep_idt &c_type)
     return "";
 }
 
-std::optional<std::pair<struct_union_typet::componentt, mp_integer>>
+std::optional<std::pair<struct_union_typet::componentt, bitst>>
 union_typet::find_widest_union_component(const namespacet &ns) const
 {
   const union_typet::componentst &comps = components();
 
-  std::optional<mp_integer> max_width;
+  std::optional<bitst> max_width;
   typet max_comp_type;
   irep_idt max_comp_name;
 
diff --git a/src/util/c_types.h b/src/util/c_types.h
index 7fbad42c8008..7cea41d785c1 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -160,7 +160,7 @@ class union_typet : public struct_union_typet
   /// \param ns: Namespace to resolve tag types.
   /// \return Pair of a componentt pointing to the maximum fixed bit-width
   ///   member of the union type and the bit width of that member.
-  std::optional<std::pair<struct_union_typet::componentt, mp_integer>>
+  std::optional<std::pair<struct_union_typet::componentt, bitst>>
   find_widest_union_component(const namespacet &ns) const;
 };
 
diff --git a/src/util/config.cpp b/src/util/config.cpp
index 50ce2192004d..aaac360fd93d 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -59,8 +59,8 @@ void configt::ansi_ct::set_LP64()
   char_is_unsigned=false;
   wchar_t_is_unsigned=false;
   wchar_t_width=4*8;
-  alignment=1;
-  memory_operand_size=int_width/8;
+  alignment = bytest{1};
+  memory_operand_size = bytest{int_width / 8};
 }
 
 /// int=64, long=64, pointer=64
@@ -83,8 +83,8 @@ void configt::ansi_ct::set_ILP64()
   char_is_unsigned=false;
   wchar_t_is_unsigned=false;
   wchar_t_width=4*8;
-  alignment=1;
-  memory_operand_size=int_width/8;
+  alignment = bytest{1};
+  memory_operand_size = bytest{int_width / 8};
 }
 
 /// int=32, long=32, pointer=64
@@ -103,8 +103,8 @@ void configt::ansi_ct::set_LLP64()
   char_is_unsigned=false;
   wchar_t_is_unsigned=false;
   wchar_t_width=4*8;
-  alignment=1;
-  memory_operand_size=int_width/8;
+  alignment = bytest{1};
+  memory_operand_size = bytest{int_width / 8};
 }
 
 /// int=32, long=32, pointer=32
@@ -123,8 +123,8 @@ void configt::ansi_ct::set_ILP32()
   char_is_unsigned=false;
   wchar_t_is_unsigned=false;
   wchar_t_width=4*8;
-  alignment=1;
-  memory_operand_size=int_width/8;
+  alignment = bytest{1};
+  memory_operand_size = bytest{int_width / 8};
 }
 
 /// int=16, long=32, pointer=32
@@ -143,8 +143,8 @@ void configt::ansi_ct::set_LP32()
   char_is_unsigned=false;
   wchar_t_is_unsigned=false;
   wchar_t_width=4*8;
-  alignment=1;
-  memory_operand_size=int_width/8;
+  alignment = bytest{1};
+  memory_operand_size = bytest{int_width / 8};
 }
 
 void configt::ansi_ct::set_arch_spec_i386()
@@ -1298,9 +1298,10 @@ void configt::set_from_symbol_table(const symbol_table_baset &symbol_table)
   // ts_18661_3_Floatn_types are not architectural features,
   // and thus not stored in namespace
 
-  ansi_c.alignment=unsigned_from_ns(ns, "alignment");
+  ansi_c.alignment = bytest{unsigned_from_ns(ns, "alignment")};
 
-  ansi_c.memory_operand_size=unsigned_from_ns(ns, "memory_operand_size");
+  ansi_c.memory_operand_size =
+    bytest{unsigned_from_ns(ns, "memory_operand_size")};
 
   ansi_c.endianness=(ansi_ct::endiannesst)unsigned_from_ns(ns, "endianness");
 
diff --git a/src/util/config.h b/src/util/config.h
index 5929c64f6a32..04b69c632396 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ieee_float.h"
 #include "irep.h"
+#include "mp_arith.h"
 
 #include <list>
 #include <optional>
@@ -133,7 +134,7 @@ class configt
 public:
   struct ansi_ct
   {
-    // for ANSI-C
+    // for ANSI-C, measured in bits (using bitst would add some type safety)
     std::size_t int_width;
     std::size_t long_int_width;
     std::size_t bool_width;
@@ -190,11 +191,11 @@ class configt
     void set_LP32();  // int=16, long=32, pointer=32
 
     // minimum alignment (in structs) measured in bytes
-    std::size_t alignment;
+    bytest alignment = bytest{0};
 
     // maximum minimum size of the operands for a machine
     // instruction (in bytes)
-    std::size_t memory_operand_size;
+    bytest memory_operand_size = bytest{0};
 
     enum class endiannesst
     {
diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp
index a04952856bce..f96e6d4ae901 100644
--- a/src/util/expr_util.cpp
+++ b/src/util/expr_util.cpp
@@ -268,11 +268,11 @@ bool can_forward_propagatet::is_constant(const exprt &expr) const
     if(!extract_bits.has_value())
       return false;
 
-    const mp_integer offset_bits =
+    const bitst offset_bits{
       numeric_cast_v<mp_integer>(to_constant_expr(be->offset())) *
-      be->get_bits_per_byte();
+      be->get_bits_per_byte()};
 
-    return offset_bits >= 0 && offset_bits + *extract_bits <= *op_bits;
+    return offset_bits >= bitst{0} && offset_bits + *extract_bits <= *op_bits;
   }
   else if(auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
   {
@@ -287,12 +287,12 @@ bool can_forward_propagatet::is_constant(const exprt &expr) const
     if(!src_bits.has_value())
       return false;
 
-    const mp_integer lower_bound =
-      numeric_cast_v<mp_integer>(to_constant_expr(eb->lower()));
-    const mp_integer upper_bound =
-      numeric_cast_v<mp_integer>(to_constant_expr(eb->upper()));
+    const bitst lower_bound =
+      numeric_cast_v<bitst>(to_constant_expr(eb->lower()));
+    const bitst upper_bound =
+      numeric_cast_v<bitst>(to_constant_expr(eb->upper()));
 
-    return lower_bound >= 0 && lower_bound <= upper_bound &&
+    return lower_bound >= bitst{0} && lower_bound <= upper_bound &&
            upper_bound < src_bits;
   }
   else
diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp
index 1d0409c16c66..ac046e25ea08 100644
--- a/src/util/lower_byte_operators.cpp
+++ b/src/util/lower_byte_operators.cpp
@@ -185,14 +185,14 @@ static array_exprt bv_to_array_expr(
     to_bitvector_type(bitvector_expr.type()).get_width();
   if(!num_elements.has_value())
   {
-    if(!subtype_bits.has_value() || *subtype_bits == 0)
+    if(!subtype_bits.has_value() || *subtype_bits == bitst{0})
       num_elements = total_bits;
     else
       num_elements = total_bits / numeric_cast_v<std::size_t>(*subtype_bits);
   }
   DATA_INVARIANT(
     !num_elements.has_value() || !subtype_bits.has_value() ||
-      *subtype_bits * *num_elements == total_bits,
+      *subtype_bits * *num_elements == bitst{total_bits},
     "subtype width times array size should be total bitvector width");
 
   exprt::operandst operands;
@@ -239,7 +239,7 @@ static vector_exprt bv_to_vector_expr(
   DATA_INVARIANT(
     !subtype_bits.has_value() ||
       *subtype_bits * num_elements ==
-        to_bitvector_type(bitvector_expr.type()).get_width(),
+        bitst{to_bitvector_type(bitvector_expr.type()).get_width()},
     "subtype width times vector size should be total bitvector width");
 
   exprt::operandst operands;
@@ -409,8 +409,8 @@ static exprt bv_to_expr(
 static exprt unpack_rec(
   const exprt &src,
   bool little_endian,
-  const std::optional<mp_integer> &offset_bytes,
-  const std::optional<mp_integer> &max_bytes,
+  const std::optional<bytest> &offset_bytes,
+  const std::optional<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns,
   bool unpack_byte_array = false);
@@ -538,23 +538,26 @@ static exprt unpack_array_vector_no_known_bounds(
 static exprt unpack_array_vector(
   const exprt &src,
   const std::optional<mp_integer> &src_size,
-  const mp_integer &element_bits,
+  const bitst &element_bits,
   bool little_endian,
-  const std::optional<mp_integer> &offset_bytes,
-  const std::optional<mp_integer> &max_bytes,
+  const std::optional<bytest> &offset_bytes,
+  const std::optional<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns)
 {
-  const std::size_t el_bytes = numeric_cast_v<std::size_t>(
-    (element_bits + bits_per_byte - 1) / bits_per_byte);
+  const bytest el_bytes = bits_to_bytes_ceil(element_bits, bits_per_byte);
 
   if(!src_size.has_value() && !max_bytes.has_value())
   {
     PRECONDITION_WITH_DIAGNOSTICS(
-      el_bytes > 0 && element_bits % bits_per_byte == 0,
+      el_bytes > bytest{0} && element_bits % bitst{bits_per_byte} == bitst{0},
       "unpacking of arrays with non-byte-aligned elements is not supported");
     return unpack_array_vector_no_known_bounds(
-      src, el_bytes, little_endian, bits_per_byte, ns);
+      src,
+      numeric_cast_v<std::size_t>(el_bytes),
+      little_endian,
+      bits_per_byte,
+      ns);
   }
 
   exprt::operandst byte_operands;
@@ -562,13 +565,15 @@ static exprt unpack_array_vector(
 
   // refine the number of elements to extract in case the element width is known
   // and a multiple of bytes; otherwise we will expand the entire array/vector
-  std::optional<mp_integer> num_elements = src_size;
-  if(element_bits > 0 && element_bits % bits_per_byte == 0)
+  std::optional<mp_integer> num_elements;
+  if(src_size.has_value())
+    num_elements = *src_size;
+  if(element_bits > bitst{0} && element_bits % bitst{bits_per_byte} == bitst{0})
   {
     if(!num_elements.has_value())
     {
       // turn bytes into elements, rounding up
-      num_elements = (*max_bytes + el_bytes - 1) / el_bytes;
+      num_elements = (*max_bytes + el_bytes - bytest{1}) / el_bytes;
     }
 
     if(offset_bytes.has_value())
@@ -588,7 +593,7 @@ static exprt unpack_array_vector(
   // array/vector is unknown; if element_bits was usable above this will
   // have been turned into a number of elements already
   if(!num_elements)
-    num_elements = *max_bytes;
+    num_elements = max_bytes->get();
 
   const exprt src_simp = simplify_expr(src, ns);
   const typet index_type = src_simp.type().id() == ID_array
@@ -614,13 +619,11 @@ static exprt unpack_array_vector(
     // recursively unpack each element so that we eventually just have an array
     // of bytes left
 
-    const std::optional<mp_integer> element_max_bytes =
-      max_bytes
-        ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
-        : std::optional<mp_integer>{};
-    const std::size_t element_max_bytes_int =
-      element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
-                        : el_bytes;
+    const std::optional<bytest> element_max_bytes =
+      max_bytes ? std::min(el_bytes, *max_bytes - bytest{byte_operands.size()})
+                : std::optional<bytest>{};
+    const std::size_t element_max_bytes_int = numeric_cast_v<std::size_t>(
+      element_max_bytes ? *element_max_bytes : el_bytes);
 
     exprt sub = unpack_rec(
       element, little_endian, {}, element_max_bytes, bits_per_byte, ns, true);
@@ -629,7 +632,7 @@ static exprt unpack_array_vector(
     byte_operands.insert(
       byte_operands.end(), sub_operands.begin(), sub_operands.end());
 
-    if(max_bytes && byte_operands.size() >= *max_bytes)
+    if(max_bytes && bytest{byte_operands.size()} >= *max_bytes)
       break;
   }
 
@@ -655,8 +658,8 @@ static void process_bit_fields(
   std::size_t total_bits,
   exprt::operandst &dest,
   bool little_endian,
-  const std::optional<mp_integer> &offset_bytes,
-  const std::optional<mp_integer> &max_bytes,
+  const std::optional<bytest> &offset_bytes,
+  const std::optional<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns)
 {
@@ -691,19 +694,19 @@ static void process_bit_fields(
 static array_exprt unpack_struct(
   const exprt &src,
   bool little_endian,
-  const std::optional<mp_integer> &offset_bytes,
-  const std::optional<mp_integer> &max_bytes,
+  const std::optional<bytest> &offset_bytes,
+  const std::optional<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns)
 {
   const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
   const struct_typet::componentst &components = struct_type.components();
 
-  std::optional<mp_integer> offset_in_member;
-  std::optional<mp_integer> max_bytes_left;
+  std::optional<bytest> offset_in_member;
+  std::optional<bytest> max_bytes_left;
   std::optional<std::pair<exprt::operandst, std::size_t>> bit_fields;
 
-  mp_integer member_offset_bits = 0;
+  bitst member_offset_bits{0};
   exprt::operandst byte_operands;
   for(auto it = components.begin(); it != components.end(); ++it)
   {
@@ -725,7 +728,7 @@ static array_exprt unpack_struct(
       simplify(member, ns);
 
     // Is it a byte-aligned member?
-    if(member_offset_bits % bits_per_byte == 0)
+    if(member_offset_bits % bitst{bits_per_byte} == bitst{0})
     {
       if(bit_fields.has_value())
       {
@@ -743,24 +746,27 @@ static array_exprt unpack_struct(
 
       if(offset_bytes.has_value())
       {
-        offset_in_member = *offset_bytes - member_offset_bits / bits_per_byte;
+        offset_in_member =
+          *offset_bytes - bytest{member_offset_bits / bitst{bits_per_byte}};
         // if the offset is negative, offset_in_member remains unset, which has
         // the same effect as setting it to zero
-        if(*offset_in_member < 0)
+        if(*offset_in_member < bytest{0})
           offset_in_member.reset();
       }
 
       if(max_bytes.has_value())
       {
-        max_bytes_left = *max_bytes - member_offset_bits / bits_per_byte;
-        if(*max_bytes_left < 0)
+        max_bytes_left =
+          *max_bytes - bytest{member_offset_bits / bitst{bits_per_byte}};
+        if(*max_bytes_left < bytest{0})
           break;
       }
     }
 
     if(
-      member_offset_bits % bits_per_byte != 0 ||
-      (component_bits.has_value() && *component_bits % bits_per_byte != 0))
+      member_offset_bits % bitst{bits_per_byte} != bitst{0} ||
+      (component_bits.has_value() &&
+       *component_bits % bitst{bits_per_byte} != bitst{0}))
     {
       if(!bit_fields.has_value())
         bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
@@ -782,13 +788,13 @@ static array_exprt unpack_struct(
 
     if(
       component_bits.has_value() && offset_in_member.has_value() &&
-      *offset_in_member * bits_per_byte >= *component_bits)
+      bytes_to_bits(*offset_in_member, bits_per_byte) >= *component_bits)
     {
       // we won't actually need this component, fill in zeros instead of
       // computing an unpacking
       byte_operands.resize(
-        byte_operands.size() +
-          numeric_cast_v<std::size_t>(*component_bits / bits_per_byte),
+        byte_operands.size() + numeric_cast_v<std::size_t>(bits_to_bytes_trunc(
+                                 *component_bits, bits_per_byte)),
         from_integer(0, bv_typet{bits_per_byte}));
     }
     else
@@ -849,13 +855,13 @@ static array_exprt unpack_complex(
 
   auto subtype_bits = pointer_offset_bits(subtype, ns);
   CHECK_RETURN(subtype_bits.has_value());
-  CHECK_RETURN(*subtype_bits % bits_per_byte == 0);
+  CHECK_RETURN(*subtype_bits % bitst{bits_per_byte} == bitst{0});
 
   exprt sub_real = unpack_rec(
     complex_real_exprt{src},
     little_endian,
-    mp_integer{0},
-    *subtype_bits / bits_per_byte,
+    bytest{0},
+    bytest{*subtype_bits / bitst{bits_per_byte}},
     bits_per_byte,
     ns,
     true);
@@ -864,8 +870,8 @@ static array_exprt unpack_complex(
   exprt sub_imag = unpack_rec(
     complex_imag_exprt{src},
     little_endian,
-    mp_integer{0},
-    *subtype_bits / bits_per_byte,
+    bytest{0},
+    bytest{*subtype_bits / bitst{bits_per_byte}},
     bits_per_byte,
     ns,
     true);
@@ -895,8 +901,8 @@ static array_exprt unpack_complex(
 static exprt unpack_rec(
   const exprt &src,
   bool little_endian,
-  const std::optional<mp_integer> &offset_bytes,
-  const std::optional<mp_integer> &max_bytes,
+  const std::optional<bytest> &offset_bytes,
+  const std::optional<bytest> &max_bytes,
   const std::size_t bits_per_byte,
   const namespacet &ns,
   bool unpack_byte_array)
@@ -910,7 +916,7 @@ static exprt unpack_rec(
     CHECK_RETURN(element_bits.has_value());
 
     if(
-      !unpack_byte_array && *element_bits == bits_per_byte &&
+      !unpack_byte_array && *element_bits == bitst{bits_per_byte} &&
       can_cast_type<bitvector_typet>(subtype))
     {
       return src;
@@ -936,7 +942,7 @@ static exprt unpack_rec(
     CHECK_RETURN(element_bits.has_value());
 
     if(
-      !unpack_byte_array && *element_bits == bits_per_byte &&
+      !unpack_byte_array && *element_bits == bitst{bits_per_byte} &&
       can_cast_type<bitvector_typet>(subtype))
     {
       return src;
@@ -975,7 +981,7 @@ static exprt unpack_rec(
         member,
         little_endian,
         offset_bytes,
-        (widest_member->second + bits_per_byte - 1) / bits_per_byte,
+        bits_to_bytes_ceil(widest_member->second, bits_per_byte),
         bits_per_byte,
         ns,
         true);
@@ -1033,20 +1039,20 @@ static exprt unpack_rec(
     auto bits_opt = pointer_offset_bits(src.type(), ns);
     DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
 
-    const mp_integer total_bits = *bits_opt;
-    mp_integer last_bit = total_bits;
-    mp_integer bit_offset = 0;
+    const bitst total_bits = *bits_opt;
+    bitst last_bit = total_bits;
+    bitst bit_offset{0};
 
     if(max_bytes.has_value())
     {
-      const auto max_bits = *max_bytes * bits_per_byte;
+      const auto max_bits = bytes_to_bits(*max_bytes, bits_per_byte);
       if(little_endian)
       {
         last_bit = std::min(last_bit, max_bits);
       }
       else
       {
-        bit_offset = std::max(mp_integer{0}, last_bit - max_bits);
+        bit_offset = std::max(bitst{0}, last_bit - max_bits);
       }
     }
 
@@ -1057,13 +1063,14 @@ static exprt unpack_rec(
     array_typet array_type{
       bv_typet{bits_per_byte}, from_integer(0, size_type())};
 
-    for(; bit_offset < last_bit; bit_offset += bits_per_byte)
+    for(; bit_offset < last_bit; bit_offset += bitst{bits_per_byte})
     {
       PRECONDITION(
         pointer_offset_bits(src_as_bitvector.type(), ns).has_value());
       extractbits_exprt extractbits(
         src_as_bitvector,
-        from_integer(bit_offset + bits_per_byte - 1, array_type.index_type()),
+        from_integer(
+          bit_offset + bitst{bits_per_byte - 1}, array_type.index_type()),
         from_integer(bit_offset, array_type.index_type()),
         byte_type);
 
@@ -1099,7 +1106,7 @@ static exprt lower_byte_extract_array_vector(
   const byte_extract_exprt &src,
   const byte_extract_exprt &unpacked,
   const typet &subtype,
-  const mp_integer &element_bits,
+  const bitst &element_bits,
   const namespacet &ns)
 {
   std::optional<std::size_t> num_elements;
@@ -1117,7 +1124,7 @@ static exprt lower_byte_extract_array_vector(
       plus_exprt new_offset(
         unpacked.offset(),
         from_integer(
-          i * element_bits / src.get_bits_per_byte(),
+          i * element_bits / bitst{src.get_bits_per_byte()},
           unpacked.offset().type()));
 
       byte_extract_exprt tmp(unpacked);
@@ -1154,7 +1161,7 @@ static exprt lower_byte_extract_array_vector(
       mult_exprt{
         array_comprehension_index,
         from_integer(
-          element_bits / src.get_bits_per_byte(),
+          element_bits / bitst{src.get_bits_per_byte()},
           array_comprehension_index.type())},
       unpacked.offset().type())};
 
@@ -1185,7 +1192,9 @@ static std::optional<exprt> lower_byte_extract_complex(
   const typet &subtype = complex_type.subtype();
 
   auto subtype_bits = pointer_offset_bits(subtype, ns);
-  if(!subtype_bits.has_value() || *subtype_bits % src.get_bits_per_byte() != 0)
+  if(
+    !subtype_bits.has_value() ||
+    *subtype_bits % bitst{src.get_bits_per_byte()} != bitst{0})
     return {};
 
   // offset remains unchanged
@@ -1195,7 +1204,8 @@ static std::optional<exprt> lower_byte_extract_complex(
   const plus_exprt new_offset{
     unpacked.offset(),
     from_integer(
-      *subtype_bits / src.get_bits_per_byte(), unpacked.offset().type())};
+      *subtype_bits / bitst{src.get_bits_per_byte()},
+      unpacked.offset().type())};
   byte_extract_exprt imag{unpacked};
   imag.type() = subtype;
   imag.offset() = simplify_expr(new_offset, ns);
@@ -1274,9 +1284,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   else if(src.type().id() == ID_empty)
     upper_bound_opt = from_integer(0, size_type());
 
-  const auto lower_bound_int_opt = numeric_cast<mp_integer>(src.offset());
+  const auto lower_bound_int_opt = numeric_cast<bytest>(src.offset());
   const auto upper_bound_int_opt =
-    numeric_cast<mp_integer>(upper_bound_opt.value_or(nil_exprt()));
+    numeric_cast<bytest>(upper_bound_opt.value_or(nil_exprt()));
 
   byte_extract_exprt unpacked(src);
   unpacked.op() = unpack_rec(
@@ -1299,8 +1309,8 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     // stitching together consecutive elements down below
     auto element_bits = pointer_offset_bits(subtype, ns);
     if(
-      element_bits.has_value() && *element_bits >= 1 &&
-      *element_bits % src.get_bits_per_byte() == 0)
+      element_bits.has_value() && *element_bits >= bitst{1} &&
+      *element_bits % bitst{src.get_bits_per_byte()} == bitst{0})
     {
       return lower_byte_extract_array_vector(
         src, unpacked, subtype, *element_bits, ns);
@@ -1329,7 +1339,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
       // the next member would be misaligned, abort
       if(
         !component_bits.has_value() ||
-        *component_bits % src.get_bits_per_byte() != 0)
+        *component_bits % bitst{src.get_bits_per_byte()} != bitst{0})
       {
         failed = true;
         break;
@@ -1396,7 +1406,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   auto subtype_bits = pointer_offset_bits(*subtype, ns);
 
   DATA_INVARIANT(
-    subtype_bits.has_value() && *subtype_bits == src.get_bits_per_byte(),
+    subtype_bits.has_value() && *subtype_bits == bitst{src.get_bits_per_byte()},
     "offset bits are byte aligned");
 
   auto size_bits = pointer_offset_bits(unpacked.type(), ns);
@@ -1410,9 +1420,10 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     size_bits = op0_bits;
   }
 
-  mp_integer num_bytes =
-    (*size_bits) / src.get_bits_per_byte() +
-    (((*size_bits) % src.get_bits_per_byte() == 0) ? 0 : 1);
+  bytest num_bytes =
+    bytest{(*size_bits) / bitst{src.get_bits_per_byte()}} +
+    bytest{
+      (((*size_bits) % bitst{src.get_bits_per_byte()} == bitst{0}) ? 0 : 1)};
 
   // get 'width'-many bytes, and concatenate
   const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
@@ -1913,10 +1924,10 @@ static exprt lower_byte_update_array_vector_non_const(
 /// \return Array/vector expression reflecting all updates.
 static exprt lower_byte_update_single_element(
   const byte_update_exprt &src,
-  const mp_integer &offset_bits,
+  const bitst &offset_bits,
   const exprt &element_to_update,
-  const mp_integer &subtype_bits,
-  const mp_integer &bits_already_set,
+  const bitst &subtype_bits,
+  const bitst &bits_already_set,
   const exprt &value_as_byte_array,
   const std::optional<exprt> &non_const_update_bound,
   const namespacet &ns)
@@ -1928,33 +1939,38 @@ static exprt lower_byte_update_single_element(
   // will need to be updated using the same byte.
   std::size_t first = 0;
   // - An upper bound on the number of bytes required from value_as_byte_array.
-  mp_integer update_elements =
-    (subtype_bits + src.get_bits_per_byte() - 1) / src.get_bits_per_byte();
+  bytest update_elements =
+    bits_to_bytes_ceil(subtype_bits, src.get_bits_per_byte());
   // - The offset into the target element: If subtype_bits is greater or equal
   // to the size of a byte, then there may be an offset into the target element
   // that needs to be taken into account, and multiple bytes will be required.
-  mp_integer offset_bits_in_target_element = offset_bits - bits_already_set;
+  bitst offset_bits_in_target_element = offset_bits - bits_already_set;
 
-  if(offset_bits_in_target_element < 0)
+  if(offset_bits_in_target_element < bitst{0})
   {
     INVARIANT(
       value_as_byte_array.id() != ID_array ||
-        value_as_byte_array.operands().size() * src.get_bits_per_byte() >
-          -offset_bits_in_target_element,
+        bytes_to_bits(
+          bytest{value_as_byte_array.operands().size()},
+          src.get_bits_per_byte()) > -1 * offset_bits_in_target_element,
       "indices past the update should be handled below");
     first += numeric_cast_v<std::size_t>(
-      -offset_bits_in_target_element / src.get_bits_per_byte());
-    offset_bits_in_target_element +=
-      (-offset_bits_in_target_element / src.get_bits_per_byte()) *
-      src.get_bits_per_byte();
-    if(offset_bits_in_target_element < 0)
-      ++update_elements;
+      -1 * bits_to_bytes_trunc(
+             offset_bits_in_target_element, src.get_bits_per_byte()));
+    offset_bits_in_target_element += bytes_to_bits(
+      -1 * bits_to_bytes_trunc(
+             offset_bits_in_target_element, src.get_bits_per_byte()),
+      src.get_bits_per_byte());
+    if(offset_bits_in_target_element < bitst{0})
+      update_elements += bytest{1};
   }
   else
   {
-    update_elements -= offset_bits_in_target_element / src.get_bits_per_byte();
+    update_elements -= bits_to_bytes_trunc(
+      offset_bits_in_target_element, src.get_bits_per_byte());
     INVARIANT(
-      update_elements > 0, "indices before the update should be handled above");
+      update_elements > bytest{0},
+      "indices before the update should be handled above");
   }
 
   std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
@@ -1971,8 +1987,8 @@ static exprt lower_byte_update_single_element(
   exprt new_value;
 
   if(
-    offset_bits_in_target_element >= 0 &&
-    offset_bits_in_target_element % src.get_bits_per_byte() == 0)
+    offset_bits_in_target_element >= bitst{0} &&
+    offset_bits_in_target_element % bitst{src.get_bits_per_byte()} == bitst{0})
   {
     new_value = array_exprt{update_values, update_type};
   }
@@ -1980,21 +1996,21 @@ static exprt lower_byte_update_single_element(
   {
     if(src.id() == ID_byte_update_little_endian)
       std::reverse(update_values.begin(), update_values.end());
-    if(offset_bits_in_target_element < 0)
+    if(offset_bits_in_target_element < bitst{0})
     {
       if(src.id() == ID_byte_update_little_endian)
       {
         new_value = lshr_exprt{
           concatenation_exprt{
             update_values, bv_typet{update_size * src.get_bits_per_byte()}},
-          numeric_cast_v<std::size_t>(-offset_bits_in_target_element)};
+          numeric_cast_v<std::size_t>(-1 * offset_bits_in_target_element)};
       }
       else
       {
         new_value = shl_exprt{
           concatenation_exprt{
             update_values, bv_typet{update_size * src.get_bits_per_byte()}},
-          numeric_cast_v<std::size_t>(-offset_bits_in_target_element)};
+          numeric_cast_v<std::size_t>(-1 * offset_bits_in_target_element)};
       }
     }
     else
@@ -2033,7 +2049,7 @@ static exprt lower_byte_update_single_element(
 
     new_value = lower_byte_extract(byte_extract_expr, ns);
 
-    offset_bits_in_target_element = 0;
+    offset_bits_in_target_element = bitst{0};
   }
 
   // With an upper bound on the size of the update established, construct the
@@ -2091,7 +2107,7 @@ static exprt lower_byte_update_single_element(
 static exprt lower_byte_update_array_vector(
   const byte_update_exprt &src,
   const typet &subtype,
-  const std::optional<mp_integer> &subtype_bits,
+  const std::optional<bitst> &subtype_bits,
   const exprt &value_as_byte_array,
   const std::optional<exprt> &non_const_update_bound,
   const namespacet &ns)
@@ -2121,9 +2137,9 @@ static exprt lower_byte_update_array_vector(
 
   std::size_t num_elements =
     numeric_cast_v<std::size_t>(to_constant_expr(size));
-  mp_integer offset_bits =
-    numeric_cast_v<mp_integer>(to_constant_expr(src.offset())) *
-    src.get_bits_per_byte();
+  bitst offset_bits = bytes_to_bits(
+    numeric_cast_v<bytest>(to_constant_expr(src.offset())),
+    src.get_bits_per_byte());
 
   exprt::operandst elements;
   elements.reserve(num_elements);
@@ -2134,10 +2150,11 @@ static exprt lower_byte_update_array_vector(
     elements.push_back(index_exprt{src.op(), from_integer(i, index_type)});
 
   // the modified elements
-  for(;
-      i < num_elements &&
-      i * *subtype_bits < offset_bits + value_as_byte_array.operands().size() *
-                                          src.get_bits_per_byte();
+  for(; i < num_elements &&
+        i * *subtype_bits <
+          offset_bits + bytes_to_bits(
+                          bytest{value_as_byte_array.operands().size()},
+                          src.get_bits_per_byte());
       ++i)
   {
     elements.push_back(lower_byte_update_single_element(
@@ -2182,7 +2199,7 @@ static exprt lower_byte_update_struct(
   exprt::operandst elements;
   elements.reserve(struct_type.components().size());
 
-  mp_integer member_offset_bits = 0;
+  bitst member_offset_bits{0};
   for(const auto &comp : struct_type.components())
   {
     auto element_width = pointer_offset_bits(comp.type(), ns);
@@ -2196,7 +2213,7 @@ static exprt lower_byte_update_struct(
           from_integer(src.get_bits_per_byte(), src.offset().type())},
         from_integer(member_offset_bits, src.offset().type())},
       ns);
-    auto offset_bits = numeric_cast<mp_integer>(offset);
+    auto offset_bits = numeric_cast<bitst>(offset);
     if(!offset_bits.has_value() || !element_width.has_value())
     {
       // The offset to update is not constant, either because the original
@@ -2242,9 +2259,10 @@ static exprt lower_byte_update_struct(
     // offset
     if(
       *offset_bits >= *element_width ||
-      (value_as_byte_array.id() == ID_array && *offset_bits < 0 &&
-       -*offset_bits >=
-         value_as_byte_array.operands().size() * src.get_bits_per_byte()))
+      (value_as_byte_array.id() == ID_array && *offset_bits < bitst{0} &&
+       -1 * *offset_bits >= bytes_to_bits(
+                              bytest{value_as_byte_array.operands().size()},
+                              src.get_bits_per_byte())))
     {
       elements.push_back(member);
       member_offset_bits += *element_width;
@@ -2324,7 +2342,9 @@ static exprt lower_byte_update(
 
     auto element_width = pointer_offset_bits(*subtype, ns);
 
-    if(element_width.has_value() && *element_width == src.get_bits_per_byte())
+    if(
+      element_width.has_value() &&
+      *element_width == bitst{src.get_bits_per_byte()})
     {
       if(value_as_byte_array.id() != ID_array)
       {
@@ -2382,7 +2402,7 @@ static exprt lower_byte_update(
     // mask out the bits to be updated, shift the value according to the
     // offset and bit-or
     const auto type_width = pointer_offset_bits(src.type(), ns);
-    CHECK_RETURN(type_width.has_value() && *type_width > 0);
+    CHECK_RETURN(type_width.has_value() && *type_width > bitst{0});
     const std::size_t type_bits = numeric_cast_v<std::size_t>(*type_width);
 
     exprt::operandst update_bytes;
@@ -2424,8 +2444,8 @@ static exprt lower_byte_update(
       const exprt src_as_bytes = unpack_rec(
         val_before,
         src.id() == ID_byte_update_little_endian,
-        mp_integer{0},
-        mp_integer{update_bytes.size()},
+        bytest{0},
+        bytest{update_bytes.size()},
         src.get_bits_per_byte(),
         ns);
       CHECK_RETURN(src_as_bytes.id() == ID_array);
diff --git a/src/util/mp_arith.h b/src/util/mp_arith.h
index 99a6175c2b78..fd45fbbb14d7 100644
--- a/src/util/mp_arith.h
+++ b/src/util/mp_arith.h
@@ -10,6 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_MP_ARITH_H
 #define CPROVER_UTIL_MP_ARITH_H
 
+#include "invariant.h"
+
 #include <iosfwd>
 #include <string>
 
@@ -48,4 +50,178 @@ const mp_integer string2integer(const std::string &, unsigned base=10);
 const std::string integer2binary(const mp_integer &, std::size_t width);
 const mp_integer binary2integer(const std::string &, bool is_signed);
 
+// https://www.fluentcpp.com/2016/12/08/strong-types-for-strong-interfaces/
+#define BITS_COMPARISON(op)                                                    \
+  bool operator op(const bitst &other) const                                   \
+  {                                                                            \
+    return static_cast<const mp_integer &>(*this)                              \
+      op static_cast<const mp_integer &>(other);                               \
+  }                                                                            \
+  bool operator op(const mp_integer &other) const = delete
+
+template <typename Tag>
+class named_mp_integert
+{
+public:
+  explicit named_mp_integert(const mp_integer &generic) : value(generic)
+  {
+  }
+
+  explicit named_mp_integert(mp_integer &&generic) : value(std::move(generic))
+  {
+  }
+
+  const mp_integer &get() const
+  {
+    return value;
+  }
+
+  named_mp_integert &operator+=(const named_mp_integert &other)
+  {
+    value += other.value;
+    return *this;
+  }
+
+  named_mp_integert &operator-=(const named_mp_integert &other)
+  {
+    value -= other.value;
+    return *this;
+  }
+
+  named_mp_integert &operator%=(const named_mp_integert &other)
+  {
+    value %= other.value;
+    return *this;
+  }
+
+  bool operator<(const named_mp_integert &other) const
+  {
+    return value < other.value;
+  }
+
+  bool operator>(const named_mp_integert &other) const
+  {
+    return value > other.value;
+  }
+
+  bool operator<=(const named_mp_integert &other) const
+  {
+    return value <= other.value;
+  }
+
+  bool operator>=(const named_mp_integert &other) const
+  {
+    return value >= other.value;
+  }
+
+  bool operator==(const named_mp_integert &other) const
+  {
+    return value == other.value;
+  }
+
+  bool operator!=(const named_mp_integert &other) const
+  {
+    return value != other.value;
+  }
+
+private:
+  mp_integer value;
+};
+
+template <typename T>
+inline named_mp_integert<T>
+operator+(const named_mp_integert<T> &lhs, const named_mp_integert<T> &rhs)
+{
+  return named_mp_integert<T>{lhs} += rhs;
+}
+
+template <typename T>
+inline named_mp_integert<T>
+operator-(const named_mp_integert<T> &lhs, const named_mp_integert<T> &rhs)
+{
+  return named_mp_integert<T>{lhs} -= rhs;
+}
+
+template <typename T>
+inline named_mp_integert<T>
+operator*(const named_mp_integert<T> &lhs, const mp_integer &rhs)
+{
+  return named_mp_integert<T>{lhs.get() * rhs};
+}
+
+template <typename T>
+inline named_mp_integert<T>
+operator*(const mp_integer &lhs, const named_mp_integert<T> &rhs)
+{
+  return named_mp_integert<T>{lhs * rhs.get()};
+}
+
+template <typename T>
+inline named_mp_integert<T>
+operator%(const named_mp_integert<T> &lhs, const named_mp_integert<T> &rhs)
+{
+  PRECONDITION(rhs.get() > 0);
+  return named_mp_integert<T>{lhs} %= rhs;
+}
+
+template <typename T>
+inline named_mp_integert<T>
+operator/(const named_mp_integert<T> &lhs, const mp_integer &rhs)
+{
+  PRECONDITION(rhs > 0);
+  return named_mp_integert<T>{lhs.get() / rhs};
+}
+
+template <typename T>
+inline mp_integer
+operator/(const named_mp_integert<T> &lhs, const named_mp_integert<T> &rhs)
+{
+  // division yields just a number
+  PRECONDITION(rhs.get() > 0);
+  return lhs.get() / rhs.get();
+}
+
+template <typename T>
+inline std::ostream &
+operator<<(std::ostream &os, const named_mp_integert<T> &value)
+{
+  os << value.get();
+  return os;
+}
+
+struct bits_tagt
+{
+};
+using bitst = named_mp_integert<bits_tagt>;
+
+struct bytes_tagt
+{
+};
+using bytest = named_mp_integert<bytes_tagt>;
+
+/// Convert \p bytes to bits assuming \p bits_per_byte number of bits in one
+/// byte.
+inline bitst bytes_to_bits(const bytest &bytes, const mp_integer &bits_per_byte)
+{
+  return bitst{bytes.get() * bits_per_byte};
+}
+
+/// Convert \p bits to bytes assuming \p bits_per_byte number of bits in one
+/// byte, rounding downwards.
+inline bytest
+bits_to_bytes_trunc(const bitst &bits, const mp_integer &bits_per_byte)
+{
+  PRECONDITION(bits_per_byte > 0);
+  return bytest{bits.get() / bits_per_byte};
+}
+
+/// Convert \p bits to bytes assuming \p bits_per_byte number of bits in one
+/// byte, rounding upwards.
+inline bytest
+bits_to_bytes_ceil(const bitst &bits, const mp_integer &bits_per_byte)
+{
+  PRECONDITION(bits_per_byte > 0);
+  return bytest{(bits.get() + bits_per_byte - 1) / bits_per_byte};
+}
+
 #endif // CPROVER_UTIL_MP_ARITH_H
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index b0c4de893b46..8c845b00ba02 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -22,12 +22,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ssa_expr.h"
 #include "std_expr.h"
 
-std::optional<mp_integer> member_offset(
+std::optional<bytest> member_offset(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns)
 {
-  mp_integer result = 0;
+  bytest result{0};
   std::size_t bit_field_bits = 0;
 
   for(const auto &comp : type.components())
@@ -39,13 +39,13 @@ std::optional<mp_integer> member_offset(
     {
       const std::size_t w = to_c_bit_field_type(comp.type()).get_width();
       bit_field_bits += w;
-      result += bit_field_bits / config.ansi_c.char_width;
+      result += bytest{bit_field_bits / config.ansi_c.char_width};
       bit_field_bits %= config.ansi_c.char_width;
     }
     else if(comp.is_boolean())
     {
       ++bit_field_bits;
-      result += bit_field_bits / config.ansi_c.char_width;
+      result += bytest{bit_field_bits / config.ansi_c.char_width};
       bit_field_bits %= config.ansi_c.char_width;
     }
     else
@@ -63,12 +63,12 @@ std::optional<mp_integer> member_offset(
   return result;
 }
 
-std::optional<mp_integer> member_offset_bits(
+std::optional<bitst> member_offset_bits(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns)
 {
-  mp_integer offset=0;
+  bitst offset{0};
   const struct_typet::componentst &components=type.components();
 
   for(const auto &comp : components)
@@ -87,18 +87,18 @@ std::optional<mp_integer> member_offset_bits(
 }
 
 /// Compute the size of a type in bytes, rounding up to full bytes
-std::optional<mp_integer>
+std::optional<bytest>
 pointer_offset_size(const typet &type, const namespacet &ns)
 {
   auto bits = pointer_offset_bits(type, ns);
 
   if(bits.has_value())
-    return (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
+    return bits_to_bytes_ceil(*bits, config.ansi_c.char_width);
   else
     return {};
 }
 
-std::optional<mp_integer>
+std::optional<bitst>
 pointer_offset_bits(const typet &type, const namespacet &ns)
 {
   if(type.id()==ID_array)
@@ -138,7 +138,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   else if(type.id()==ID_struct)
   {
     const struct_typet &struct_type=to_struct_type(type);
-    mp_integer result=0;
+    bitst result{0};
 
     for(const auto &c : struct_type.components())
     {
@@ -158,7 +158,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
     const union_typet &union_type=to_union_type(type);
 
     if(union_type.components().empty())
-      return mp_integer{0};
+      return bitst{0};
 
     const auto widest_member = union_type.find_widest_union_component(ns);
 
@@ -175,12 +175,12 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
           type.id()==ID_c_bool ||
           type.id()==ID_c_bit_field)
   {
-    return mp_integer(to_bitvector_type(type).get_width());
+    return bitst{to_bitvector_type(type).get_width()};
   }
   else if(type.id()==ID_c_enum)
   {
-    return mp_integer(
-      to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width());
+    return bitst{
+      to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width()};
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -188,15 +188,15 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_bool)
   {
-    return mp_integer(1);
+    return bitst{1};
   }
   else if(type.id()==ID_pointer)
   {
     // the following is an MS extension
     if(type.get_bool(ID_C_ptr32))
-      return mp_integer(32);
+      return bitst{32};
 
-    return mp_integer(to_bitvector_type(type).get_width());
+    return bitst{to_bitvector_type(type).get_width()};
   }
   else if(type.id() == ID_union_tag)
   {
@@ -208,11 +208,11 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_code)
   {
-    return mp_integer(0);
+    return bitst{0};
   }
   else if(type.id()==ID_string)
   {
-    return mp_integer(32);
+    return bitst{32};
   }
   else
     return {};
@@ -290,9 +290,10 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
       auto bits = pointer_offset_bits(array_type, ns);
 
       if(bits.has_value())
+      {
         return from_integer(
-          (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,
-          size_type());
+          bits_to_bytes_ceil(*bits, config.ansi_c.char_width), size_type());
+      }
     }
 
     auto sub = size_of_expr(array_type.element_type(), ns);
@@ -319,9 +320,10 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
       auto bits = pointer_offset_bits(vector_type, ns);
 
       if(bits.has_value())
+      {
         return from_integer(
-          (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,
-          size_type());
+          bits_to_bytes_ceil(*bits, config.ansi_c.char_width), size_type());
+      }
     }
 
     auto sub = size_of_expr(vector_type.element_type(), ns);
@@ -397,7 +399,7 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
   {
     const union_typet &union_type=to_union_type(type);
 
-    mp_integer max_bytes=0;
+    bytest max_bytes{0};
     exprt result=from_integer(0, size_type());
 
     // compute max
@@ -411,7 +413,7 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
 
       if(!sub_bits.has_value())
       {
-        max_bytes=-1;
+        max_bytes = bytest{-1};
 
         auto sub_size_opt = size_of_expr(subtype, ns);
         if(!sub_size_opt.has_value())
@@ -420,10 +422,10 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
       }
       else
       {
-        mp_integer sub_bytes =
-          (*sub_bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
+        bytest sub_bytes =
+          bits_to_bytes_ceil(*sub_bits, config.ansi_c.char_width);
 
-        if(max_bytes>=0)
+        if(max_bytes >= bytest{0})
         {
           if(max_bytes<sub_bytes)
           {
@@ -504,7 +506,7 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
     return {};
 }
 
-std::optional<mp_integer>
+std::optional<bytest>
 compute_pointer_offset(const exprt &expr, const namespacet &ns)
 {
   if(expr.id()==ID_symbol)
@@ -513,7 +515,7 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
       return compute_pointer_offset(
         to_ssa_expr(expr).get_original_expr(), ns);
     else
-      return mp_integer(0);
+      return bytest{0};
   }
   else if(expr.id()==ID_index)
   {
@@ -530,7 +532,7 @@ 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.element_type(), ns);
 
-      if(sub_size.has_value() && *sub_size > 0)
+      if(sub_size.has_value() && *sub_size > bytest{0})
       {
         const auto i = numeric_cast<mp_integer>(index_expr.index());
         if(i.has_value())
@@ -561,18 +563,18 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
     }
   }
   else if(expr.id()==ID_string_constant)
-    return mp_integer(0);
+    return bytest{0};
 
   return {}; // don't know
 }
 
 std::optional<exprt> get_subexpression_at_offset(
   const exprt &expr,
-  const mp_integer &offset_bytes,
+  const bytest &offset_bytes,
   const typet &target_type_raw,
   const namespacet &ns)
 {
-  if(offset_bytes == 0 && expr.type() == target_type_raw)
+  if(offset_bytes == bytest{0} && expr.type() == target_type_raw)
   {
     exprt result = expr;
 
@@ -583,7 +585,7 @@ std::optional<exprt> get_subexpression_at_offset(
   }
 
   if(
-    offset_bytes == 0 && expr.type().id() == ID_pointer &&
+    offset_bytes == bytest{0} && expr.type().id() == ID_pointer &&
     target_type_raw.id() == ID_pointer)
   {
     return typecast_exprt(expr, target_type_raw);
@@ -598,7 +600,7 @@ std::optional<exprt> get_subexpression_at_offset(
   {
     const struct_typet &struct_type = to_struct_type(source_type);
 
-    mp_integer m_offset_bits = 0;
+    bitst m_offset_bits{0};
     for(const auto &component : struct_type.components())
     {
       const auto m_size_bits = pointer_offset_bits(component.type(), ns);
@@ -608,15 +610,18 @@ std::optional<exprt> get_subexpression_at_offset(
       // if this member completely contains the target, and this member is
       // byte-aligned, recurse into it
       if(
-        offset_bytes * config.ansi_c.char_width >= m_offset_bits &&
-        m_offset_bits % config.ansi_c.char_width == 0 &&
-        offset_bytes * config.ansi_c.char_width + *target_size_bits <=
+        bytes_to_bits(offset_bytes, config.ansi_c.char_width) >=
+          m_offset_bits &&
+        m_offset_bits % bitst{config.ansi_c.char_width} == bitst{0} &&
+        bytes_to_bits(offset_bytes, config.ansi_c.char_width) +
+            *target_size_bits <=
           m_offset_bits + *m_size_bits)
       {
         const member_exprt member(expr, component.get_name(), component.type());
         return get_subexpression_at_offset(
           member,
-          offset_bytes - m_offset_bits / config.ansi_c.char_width,
+          offset_bytes -
+            bits_to_bytes_trunc(m_offset_bits, config.ansi_c.char_width),
           target_type_raw,
           ns);
       }
@@ -634,17 +639,18 @@ std::optional<exprt> get_subexpression_at_offset(
     // no arrays of non-byte-aligned, zero-, or unknown-sized objects
     if(
       array_type.size().is_constant() && elem_size_bits.has_value() &&
-      *elem_size_bits > 0 && *elem_size_bits % config.ansi_c.char_width == 0 &&
+      *elem_size_bits > bitst{0} &&
+      *elem_size_bits % bitst{config.ansi_c.char_width} == bitst{0} &&
       *target_size_bits <= *elem_size_bits)
     {
       const mp_integer array_size =
         numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
-      const mp_integer elem_size_bytes =
-        *elem_size_bits / config.ansi_c.char_width;
+      const bytest elem_size_bytes{
+        *elem_size_bits / bitst{config.ansi_c.char_width}};
       const mp_integer index = offset_bytes / elem_size_bytes;
-      const auto offset_inside_elem = offset_bytes % elem_size_bytes;
-      const auto target_size_bytes =
-        *target_size_bits / config.ansi_c.char_width;
+      const bytest offset_inside_elem{offset_bytes % elem_size_bytes};
+      const bytest target_size_bytes{
+        *target_size_bits / bitst{config.ansi_c.char_width}};
       // only recurse if the cell completely contains the target
       if(
         index < array_size &&
@@ -675,7 +681,8 @@ std::optional<exprt> get_subexpression_at_offset(
 
       // if this member completely contains the target, recurse into it
       if(
-        offset_bytes * config.ansi_c.char_width + *target_size_bits <=
+        bytes_to_bits(offset_bytes, config.ansi_c.char_width) +
+          *target_size_bits <=
         *m_size_bits)
       {
         const member_exprt member(expr, component.get_name(), component.type());
@@ -695,7 +702,7 @@ std::optional<exprt> get_subexpression_at_offset(
   const typet &target_type,
   const namespacet &ns)
 {
-  const auto offset_bytes = numeric_cast<mp_integer>(offset);
+  const auto offset_bytes = numeric_cast<bytest>(offset);
 
   if(!offset_bytes.has_value())
     return {};
diff --git a/src/util/pointer_offset_size.h b/src/util/pointer_offset_size.h
index 97107b11b87a..573459eb9f54 100644
--- a/src/util/pointer_offset_size.h
+++ b/src/util/pointer_offset_size.h
@@ -23,23 +23,23 @@ class struct_typet;
 class typet;
 class member_exprt;
 
-std::optional<mp_integer> member_offset(
+std::optional<bytest> member_offset(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns);
 
-std::optional<mp_integer> member_offset_bits(
+std::optional<bitst> member_offset_bits(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns);
 
-std::optional<mp_integer>
+std::optional<bytest>
 pointer_offset_size(const typet &type, const namespacet &ns);
 
-std::optional<mp_integer>
+std::optional<bitst>
 pointer_offset_bits(const typet &type, const namespacet &ns);
 
-std::optional<mp_integer>
+std::optional<bytest>
 compute_pointer_offset(const exprt &expr, const namespacet &ns);
 
 std::optional<exprt>
@@ -54,7 +54,7 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns);
 
 std::optional<exprt> get_subexpression_at_offset(
   const exprt &expr,
-  const mp_integer &offset,
+  const bytest &offset,
   const typet &target_type,
   const namespacet &ns);
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 6112e4c45fe8..01c71fa13067 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -917,7 +917,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
           simplify_typecast(typecast_exprt(op_plus_expr.op1(), size_type()));
 
         // void*
-        if(*sub_size == 0 || *sub_size == 1)
+        if(*sub_size == bytest{0} || *sub_size == bytest{1})
           new_expr.op() = offset_expr;
         else
         {
@@ -987,7 +987,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     const auto step =
       pointer_offset_size(to_pointer_type(op_type).base_type(), ns);
 
-    if(step.has_value() && *step != 0)
+    if(step.has_value() && *step != bytest{0})
     {
       const typet size_t_type(size_type());
       auto new_expr = expr;
@@ -997,7 +997,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       for(auto &op : new_expr.op().operands())
       {
         exprt new_op = simplify_typecast(typecast_exprt(op, size_t_type));
-        if(op.type().id() != ID_pointer && *step > 1)
+        if(op.type().id() != ID_pointer && *step > bytest{1})
         {
           new_op =
             simplify_mult(mult_exprt(from_integer(*step, size_t_type), new_op));
@@ -1661,7 +1661,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   }
 
   const auto el_size = pointer_offset_bits(expr.type(), ns);
-  if(el_size.has_value() && *el_size < 0)
+  if(el_size.has_value() && *el_size < bitst{0})
     return unchanged(expr);
 
   // byte_extract(byte_extract(root, offset1), offset2) =>
@@ -1711,15 +1711,15 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   }
 
   // the following require a constant offset
-  auto offset = numeric_cast<mp_integer>(expr.offset());
-  if(!offset.has_value() || *offset < 0)
+  auto offset = numeric_cast<bytest>(expr.offset());
+  if(!offset.has_value() || *offset < bytest{0})
     return unchanged(expr);
 
   // try to simplify byte_extract(byte_update(...))
   auto const bu = expr_try_dynamic_cast<byte_update_exprt>(expr.op());
-  std::optional<mp_integer> update_offset;
+  std::optional<bytest> update_offset;
   if(bu)
-    update_offset = numeric_cast<mp_integer>(bu->offset());
+    update_offset = numeric_cast<bytest>(bu->offset());
   if(bu && el_size.has_value() && update_offset.has_value())
   {
     // byte_extract(byte_update(root, offset_u, value), offset_e) so that the
@@ -1730,8 +1730,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
     // extracted range fully lies within the update value simplifies to
     // byte_extract(value, offset_e - offset_u)
     if(
-      *offset * expr.get_bits_per_byte() + *el_size <=
-      *update_offset * bu->get_bits_per_byte())
+      bytes_to_bits(*offset, expr.get_bits_per_byte()) + *el_size <=
+      bytes_to_bits(*update_offset, bu->get_bits_per_byte()))
     {
       // extracting before the update
       auto tmp = expr;
@@ -1742,8 +1742,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       const auto update_size = pointer_offset_bits(bu->value().type(), ns))
     {
       if(
-        *offset * expr.get_bits_per_byte() >=
-        *update_offset * bu->get_bits_per_byte() + *update_size)
+        bytes_to_bits(*offset, expr.get_bits_per_byte()) >=
+        bytes_to_bits(*update_offset, bu->get_bits_per_byte()) + *update_size)
       {
         // extracting after the update
         auto tmp = expr;
@@ -1752,8 +1752,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       }
       else if(
         *offset >= *update_offset &&
-        *offset * expr.get_bits_per_byte() + *el_size <=
-          *update_offset * bu->get_bits_per_byte() + *update_size)
+        bytes_to_bits(*offset, expr.get_bits_per_byte()) + *el_size <=
+          bytes_to_bits(*update_offset, bu->get_bits_per_byte()) + *update_size)
       {
         // extracting from the update
         auto tmp = expr;
@@ -1768,12 +1768,13 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   // don't do any of the following if endianness doesn't match, as
   // bytes need to be swapped
   if(
-    *offset == 0 && ((expr.id() == ID_byte_extract_little_endian &&
-                      config.ansi_c.endianness ==
-                        configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN) ||
-                     (expr.id() == ID_byte_extract_big_endian &&
-                      config.ansi_c.endianness ==
-                        configt::ansi_ct::endiannesst::IS_BIG_ENDIAN)))
+    *offset == bytest{0} &&
+    ((expr.id() == ID_byte_extract_little_endian &&
+      config.ansi_c.endianness ==
+        configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN) ||
+     (expr.id() == ID_byte_extract_big_endian &&
+      config.ansi_c.endianness ==
+        configt::ansi_ct::endiannesst::IS_BIG_ENDIAN)))
   {
     // byte extract of full object is object
     if(expr.type() == expr.op().type())
@@ -1802,7 +1803,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
 
   // no proper simplification for expr.type()==void
   // or types of unknown size
-  if(!el_size.has_value() || *el_size == 0)
+  if(!el_size.has_value() || *el_size == bitst{0})
     return unchanged(expr);
 
   if(
@@ -1823,15 +1824,16 @@ simplify_exprt::simplify_byte_extract(const 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 * expr.get_bits_per_byte() + *el_size)
+    while(bitst{const_bits.size()} <
+          bytes_to_bits(*offset, expr.get_bits_per_byte()) + *el_size)
     {
       const_bits+=const_bits;
     }
 
     std::string el_bits = std::string(
       const_bits,
-      numeric_cast_v<std::size_t>(*offset * expr.get_bits_per_byte()),
+      numeric_cast_v<std::size_t>(
+        bytes_to_bits(*offset, expr.get_bits_per_byte())),
       numeric_cast_v<std::size_t>(*el_size));
 
     auto tmp = bits2expr(
@@ -1844,7 +1846,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   // in some cases we even handle non-const array_of
   if(
     expr.op().id() == ID_array_of &&
-    (*offset * expr.get_bits_per_byte()) % (*el_size) == 0 &&
+    bytes_to_bits(*offset, expr.get_bits_per_byte()) % (*el_size) == bitst{0} &&
     *el_size <=
       pointer_offset_bits(to_array_of_expr(expr.op()).what().type(), ns))
   {
@@ -1860,7 +1862,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
 
   if(
     bits.has_value() &&
-    mp_integer(bits->size()) >= *el_size + *offset * expr.get_bits_per_byte())
+    bitst{bits->size()} >=
+      *el_size + bytes_to_bits(*offset, expr.get_bits_per_byte()))
   {
     // make sure we don't lose bits with structs containing flexible array
     // members
@@ -1887,7 +1890,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
     {
       std::string bits_cut = std::string(
         bits.value(),
-        numeric_cast_v<std::size_t>(*offset * expr.get_bits_per_byte()),
+        numeric_cast_v<std::size_t>(
+          bytes_to_bits(*offset, expr.get_bits_per_byte())),
         numeric_cast_v<std::size_t>(*el_size));
 
       auto tmp = bits2expr(
@@ -1917,8 +1921,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
 
         // the next member would be misaligned, abort
         if(
-          !component_bits.has_value() || *component_bits == 0 ||
-          *component_bits % expr.get_bits_per_byte() != 0)
+          !component_bits.has_value() || *component_bits == bitst{0} ||
+          *component_bits % bitst{expr.get_bits_per_byte()} != bitst{0})
         {
           failed = true;
           break;
@@ -1967,14 +1971,16 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
     const array_typet &array_type = to_array_type(expr.op().type());
     const auto &element_bit_width =
       pointer_offset_bits(array_type.element_type(), ns);
-    if(element_bit_width.has_value() && *element_bit_width > 0)
+    if(element_bit_width.has_value() && *element_bit_width > bitst{0})
     {
       if(
-        *offset > 0 &&
-        *offset * expr.get_bits_per_byte() % *element_bit_width == 0)
+        *offset > bytest{0} &&
+        bytes_to_bits(*offset, expr.get_bits_per_byte()) % *element_bit_width ==
+          bitst{0})
       {
         const auto elements_to_erase = numeric_cast_v<std::size_t>(
-          (*offset * expr.get_bits_per_byte()) / *element_bit_width);
+          bytes_to_bits(*offset, expr.get_bits_per_byte()) /
+          *element_bit_width);
         array_exprt slice = to_array_expr(expr.op());
         slice.operands().erase(
           slice.operands().begin(),
@@ -1987,7 +1993,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
         be.offset() = from_integer(0, expr.offset().type());
         return changed(simplify_byte_extract(be));
       }
-      else if(*offset == 0 && *el_size % *element_bit_width == 0)
+      else if(*offset == bytest{0} && *el_size % *element_bit_width == bitst{0})
       {
         const auto elements_to_keep =
           numeric_cast_v<std::size_t>(*el_size / *element_bit_width);
@@ -2079,8 +2085,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
   // byte update of full object is byte_extract(new value)
   if(
-    offset.is_zero() && val_size.has_value() && *val_size > 0 &&
-    root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
+    offset.is_zero() && val_size.has_value() && *val_size > bitst{0} &&
+    root_size.has_value() && *root_size > bitst{0} && *val_size >= *root_size)
   {
     byte_extract_exprt be(
       matching_byte_extract_id,
@@ -2093,11 +2099,13 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
   }
 
   // update bits in a constant
-  const auto offset_int = numeric_cast<mp_integer>(offset);
+  const auto offset_int = numeric_cast<bytest>(offset);
   if(
-    root_size.has_value() && *root_size >= 0 && val_size.has_value() &&
-    *val_size >= 0 && offset_int.has_value() && *offset_int >= 0 &&
-    *offset_int * expr.get_bits_per_byte() + *val_size <= *root_size)
+    root_size.has_value() && *root_size >= bitst{0} && val_size.has_value() &&
+    *val_size >= bitst{0} && offset_int.has_value() &&
+    *offset_int >= bytest{0} &&
+    bytes_to_bits(*offset_int, expr.get_bits_per_byte()) + *val_size <=
+      *root_size)
   {
     auto root_bits =
       expr2bits(root, expr.id() == ID_byte_update_little_endian, ns);
@@ -2206,13 +2214,13 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
   }
 
   // the following require a constant offset
-  if(!offset_int.has_value() || *offset_int < 0)
+  if(!offset_int.has_value() || *offset_int < bytest{0})
     return unchanged(expr);
 
   const typet &op_type=ns.follow(root.type());
 
   // size must be known
-  if(!val_size.has_value() || *val_size == 0)
+  if(!val_size.has_value() || *val_size == bitst{0})
     return unchanged(expr);
 
   // Are we updating (parts of) a struct? Do individual member updates
@@ -2244,21 +2252,22 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 
       // is it a byte-sized member?
       if(
-        !m_size_bits.has_value() || *m_size_bits == 0 ||
-        (*m_size_bits) % expr.get_bits_per_byte() != 0)
+        !m_size_bits.has_value() || *m_size_bits == bitst{0} ||
+        (*m_size_bits) % bitst{expr.get_bits_per_byte()} != bitst{0})
       {
         result_expr.make_nil();
         break;
       }
 
-      mp_integer m_size_bytes = (*m_size_bits) / expr.get_bits_per_byte();
+      bytest m_size_bytes =
+        bits_to_bytes_trunc(*m_size_bits, expr.get_bits_per_byte());
 
       // is that member part of the update?
       if(*m_offset + m_size_bytes <= *offset_int)
         continue;
       // are we done updating?
       else if(
-        update_size.has_value() && *update_size > 0 &&
+        update_size.has_value() && *update_size > bytest{0} &&
         *m_offset >= *offset_int + *update_size)
       {
         break;
@@ -2275,7 +2284,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
       if(
         *m_offset < *offset_int ||
         (*m_offset == *offset_int && update_size.has_value() &&
-         *update_size > 0 && m_size_bytes > *update_size))
+         *update_size > bytest{0} && m_size_bytes > *update_size))
       {
         byte_update_exprt v(
           expr.id(),
@@ -2287,7 +2296,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
         to_with_expr(result_expr).new_value().swap(v);
       }
       else if(
-        update_size.has_value() && *update_size > 0 &&
+        update_size.has_value() && *update_size > bytest{0} &&
         *m_offset + m_size_bytes > *offset_int + *update_size)
       {
         // we don't handle this for the moment
@@ -2319,28 +2328,42 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
       pointer_offset_bits(to_type_with_subtype(op_type).subtype(), ns);
 
     if(
-      !el_size.has_value() || *el_size == 0 ||
-      (*el_size) % expr.get_bits_per_byte() != 0 ||
-      (*val_size) % expr.get_bits_per_byte() != 0)
+      !el_size.has_value() || *el_size == bitst{0} ||
+      (*el_size) % bitst{expr.get_bits_per_byte()} != bitst{0} ||
+      (*val_size) % bitst{expr.get_bits_per_byte()} != bitst{0})
     {
       return unchanged(expr);
     }
 
     exprt result=root;
 
-    mp_integer m_offset_bits=0, val_offset=0;
+    bitst m_offset_bits{0};
+    bytest val_offset{0};
     Forall_operands(it, result)
     {
-      if(*offset_int * expr.get_bits_per_byte() + (*val_size) <= m_offset_bits)
+      if(
+        bytes_to_bits(*offset_int, expr.get_bits_per_byte()) + (*val_size) <=
+        m_offset_bits)
+      {
         break;
+      }
 
-      if(*offset_int * expr.get_bits_per_byte() < m_offset_bits + *el_size)
+      if(
+        bytes_to_bits(*offset_int, expr.get_bits_per_byte()) <
+        m_offset_bits + *el_size)
       {
-        mp_integer bytes_req =
-          (m_offset_bits + *el_size) / expr.get_bits_per_byte() - *offset_int;
+        bytest bytes_req =
+          bits_to_bytes_trunc(
+            m_offset_bits + *el_size, expr.get_bits_per_byte()) -
+          *offset_int;
         bytes_req-=val_offset;
-        if(val_offset + bytes_req > (*val_size) / expr.get_bits_per_byte())
-          bytes_req = (*val_size) / expr.get_bits_per_byte() - val_offset;
+        if(
+          val_offset + bytes_req >
+          bits_to_bytes_trunc(*val_size, expr.get_bits_per_byte()))
+        {
+          bytes_req = bits_to_bytes_trunc(*val_size, expr.get_bits_per_byte()) -
+                      val_offset;
+        }
 
         byte_extract_exprt new_val(
           matching_byte_extract_id,
@@ -2355,7 +2378,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
           expr.id(),
           *it,
           from_integer(
-            *offset_int + val_offset - m_offset_bits / expr.get_bits_per_byte(),
+            *offset_int + val_offset -
+              bytest{m_offset_bits / bitst{expr.get_bits_per_byte()}},
             offset.type()),
           new_val,
           expr.get_bits_per_byte());
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 826cf4ae34db..171eb927b36b 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -620,10 +620,8 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
         offset_op0.is_constant() && offset_op1.is_constant() &&
         object_size.has_value() && element_size.has_value() &&
         element_size->is_constant() && !element_size->is_zero() &&
-        numeric_cast_v<mp_integer>(to_constant_expr(offset_op0)) <=
-          *object_size &&
-        numeric_cast_v<mp_integer>(to_constant_expr(offset_op1)) <=
-          *object_size)
+        numeric_cast_v<bytest>(to_constant_expr(offset_op0)) <= *object_size &&
+        numeric_cast_v<bytest>(to_constant_expr(offset_op1)) <= *object_size)
       {
         return changed(simplify_rec(div_exprt{
           minus_exprt{offset_op0, offset_op1},
@@ -1138,8 +1136,8 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
     return unchanged(expr);
   }
 
-  const auto start = numeric_cast<mp_integer>(expr.upper());
-  const auto end = numeric_cast<mp_integer>(expr.lower());
+  const auto start = numeric_cast<bitst>(expr.upper());
+  const auto end = numeric_cast<bitst>(expr.lower());
 
   if(!start.has_value())
     return unchanged(expr);
@@ -1152,7 +1150,9 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
   if(!width.has_value())
     return unchanged(expr);
 
-  if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width))
+  if(
+    *start < bitst{0} || *start >= (*width) || *end < bitst{0} ||
+    *end >= (*width))
     return unchanged(expr);
 
   DATA_INVARIANT(*start >= *end, "extractbits must have upper() >= lower()");
@@ -1161,12 +1161,12 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
   {
     const auto svalue = expr2bits(expr.src(), true, ns);
 
-    if(!svalue.has_value() || svalue->size() != *width)
+    if(!svalue.has_value() || bitst{svalue->size()} != *width)
       return unchanged(expr);
 
     std::string extracted_value = svalue->substr(
       numeric_cast_v<std::size_t>(*end),
-      numeric_cast_v<std::size_t>(*start - *end + 1));
+      numeric_cast_v<std::size_t>(*start - *end + bitst{1}));
 
     auto result = bits2expr(extracted_value, expr.type(), true, ns);
     if(!result.has_value())
@@ -1178,13 +1178,13 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
   {
     // the most-significant bit comes first in an concatenation_exprt, hence we
     // count down
-    mp_integer offset = *width;
+    bitst offset = *width;
 
     for(const auto &op : expr.src().operands())
     {
       auto op_width = pointer_offset_bits(op.type(), ns);
 
-      if(!op_width.has_value() || *op_width <= 0)
+      if(!op_width.has_value() || *op_width <= bitst{0})
         return unchanged(expr);
 
       if(*start < offset && offset <= *end + *op_width)
@@ -1207,14 +1207,14 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr)
     {
       extractbits_exprt result = *eb_src;
       result.type() = expr.type();
-      const mp_integer src_lower =
-        numeric_cast_v<mp_integer>(to_constant_expr(eb_src->lower()));
+      const bitst src_lower =
+        numeric_cast_v<bitst>(to_constant_expr(eb_src->lower()));
       result.lower() = from_integer(src_lower + *end, eb_src->lower().type());
       result.upper() = from_integer(src_lower + *start, eb_src->lower().type());
       return changed(simplify_extractbits(result));
     }
   }
-  else if(*end == 0 && *start + 1 == *width)
+  else if(*end == bitst{0} && *start + bitst{1} == *width)
   {
     typecast_exprt tc{expr.src(), expr.type()};
     return changed(simplify_typecast(tc));
@@ -1808,7 +1808,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
             pointer_offset_size(address_of->object().type(), ns);
           if(
             object_size.has_value() &&
-            numeric_cast_v<mp_integer>(to_constant_expr(offset)) < *object_size)
+            numeric_cast_v<bytest>(to_constant_expr(offset)) < *object_size)
           {
             return false_exprt();
           }
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index 0749edda7700..f0106f7e7360 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -124,7 +124,8 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
           pointer_type.base_type() = new_index_expr.type();
 
           typecast_exprt typecast_expr(
-            from_integer((*step_size) * (*index) + address, c_index_type()),
+            from_integer(
+              (*step_size) * (*index) + bytest{address}, c_index_type()),
             pointer_type);
 
           return dereference_exprt{typecast_expr};
@@ -168,7 +169,8 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
             to_dereference_expr(new_member_expr.struct_op()).pointer().type());
           pointer_type.base_type() = new_member_expr.type();
           typecast_exprt typecast_expr(
-            from_integer(address + *offset, c_index_type()), pointer_type);
+            from_integer(bytest{address} + *offset, c_index_type()),
+            pointer_type);
           return dereference_exprt{typecast_expr};
         }
       }
@@ -411,9 +413,9 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
         return unchanged(expr);
 
       // The constant address consists of OBJECT-ID || OFFSET.
-      mp_integer offset_bits =
-        *pointer_offset_bits(ptr.type(), ns) - config.bv_encoding.object_bits;
-      number%=power(2, offset_bits);
+      bitst offset_bits = *pointer_offset_bits(ptr.type(), ns) -
+                          bitst{config.bv_encoding.object_bits};
+      number %= power(2, offset_bits.get());
 
       return from_integer(number, expr.type());
     }
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index a270d01296f4..951bbd82d674 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -186,11 +186,10 @@ simplify_exprt::simplify_member(const member_exprt &expr)
 
     if(target_size.has_value())
     {
-      mp_integer target_bits = target_size.value() * config.ansi_c.char_width;
+      bitst target_bits = bytes_to_bits(*target_size, config.ansi_c.char_width);
       const auto bits = expr2bits(op, true, ns);
 
-      if(bits.has_value() &&
-         mp_integer(bits->size())>=target_bits)
+      if(bits.has_value() && bitst{bits->size()} >= target_bits)
       {
         std::string bits_cut =
           std::string(*bits, 0, numeric_cast_v<std::size_t>(target_bits));
@@ -221,7 +220,7 @@ simplify_exprt::simplify_member(const member_exprt &expr)
     // type and offset with respect to x.
     if(op_type.id() == ID_struct)
     {
-      std::optional<mp_integer> requested_offset =
+      const auto requested_offset =
         member_offset(to_struct_type(op_type), component_name, ns);
       if(requested_offset.has_value())
       {
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index 3b61acd4d084..6812d010092f 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -205,9 +205,9 @@ std::optional<exprt> bits2expr(
   if(
     !type_bits.has_value() ||
     (type.id() != ID_union && type.id() != ID_union_tag &&
-     *type_bits != bits.size()) ||
+     *type_bits != bitst{bits.size()}) ||
     ((type.id() == ID_union || type.id() == ID_union_tag) &&
-     *type_bits < bits.size()))
+     *type_bits < bitst{bits.size()}))
   {
     return {};
   }
@@ -298,11 +298,11 @@ std::optional<exprt> bits2expr(
     struct_exprt result({}, type);
     result.reserve_operands(components.size());
 
-    mp_integer m_offset_bits = 0;
+    bitst m_offset_bits{0};
     for(const auto &component : components)
     {
       const auto m_size = pointer_offset_bits(component.type(), ns);
-      CHECK_RETURN(m_size.has_value() && *m_size >= 0);
+      CHECK_RETURN(m_size.has_value() && *m_size >= bitst{0});
 
       std::string comp_bits = std::string(
         bits,
@@ -342,7 +342,7 @@ std::optional<exprt> bits2expr(
       numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
 
     const auto el_size_opt = pointer_offset_bits(array_type.element_type(), ns);
-    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
+    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > bitst{0});
 
     const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
 
@@ -369,7 +369,7 @@ std::optional<exprt> bits2expr(
 
     const auto el_size_opt =
       pointer_offset_bits(vector_type.element_type(), ns);
-    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
+    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > bitst{0});
 
     const std::size_t el_size = numeric_cast_v<std::size_t>(*el_size_opt);
 
@@ -393,7 +393,7 @@ std::optional<exprt> bits2expr(
     const complex_typet &complex_type = to_complex_type(type);
 
     const auto sub_size_opt = pointer_offset_bits(complex_type.subtype(), ns);
-    CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0);
+    CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > bitst{0});
 
     const std::size_t sub_size = numeric_cast_v<std::size_t>(*sub_size_opt);
 
diff --git a/unit/util/lower_byte_operators.cpp b/unit/util/lower_byte_operators.cpp
index 4f3ac9ba9be0..2975f0b99681 100644
--- a/unit/util/lower_byte_operators.cpp
+++ b/unit/util/lower_byte_operators.cpp
@@ -325,7 +325,7 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]")
             REQUIRE(type_bits_2);
 
             // for now only extract within bounds
-            if(*type_bits_2 + 16 > *type_bits)
+            if(*type_bits_2 + bitst{16} > *type_bits)
               continue;
 
             const auto type_bits_2_int =
@@ -480,7 +480,7 @@ SCENARIO("byte_update_lowering", "[core][util][lowering][byte_update]")
             REQUIRE(type_bits_2);
 
             // for now only update within bounds
-            if(*type_bits_2 + 16 > *type_bits)
+            if(*type_bits_2 + bitst{16} > *type_bits)
               continue;
 
             const auto type_bits_2_int =
diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp
index a091f1c7f421..64d9358af825 100644
--- a/unit/util/pointer_offset_size.cpp
+++ b/unit/util/pointer_offset_size.cpp
@@ -34,12 +34,12 @@ TEST_CASE("Build subexpression to access element at offset into array")
   symbol_exprt a("array", array_type);
 
   {
-    const auto result = get_subexpression_at_offset(a, 0, t, ns);
+    const auto result = get_subexpression_at_offset(a, bytest{0}, t, ns);
     REQUIRE(result.value() == index_exprt(a, from_integer(0, c_index_type())));
   }
 
   {
-    const auto result = get_subexpression_at_offset(a, 32 / 8, t, ns);
+    const auto result = get_subexpression_at_offset(a, bytest{32 / 8}, t, ns);
     REQUIRE(result.value() == index_exprt(a, from_integer(1, c_index_type())));
   }
 
@@ -57,7 +57,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
 
   {
     const signedbv_typet small_t(8);
-    const auto result = get_subexpression_at_offset(a, 1, small_t, ns);
+    const auto result = get_subexpression_at_offset(a, bytest{1}, small_t, ns);
     REQUIRE(
       result.value() == make_byte_extract(
                           index_exprt(a, from_integer(0, c_index_type())),
@@ -67,7 +67,7 @@ TEST_CASE("Build subexpression to access element at offset into array")
 
   {
     const signedbv_typet int16_t(16);
-    const auto result = get_subexpression_at_offset(a, 3, int16_t, ns);
+    const auto result = get_subexpression_at_offset(a, bytest{3}, int16_t, ns);
     // At offset 3 there are only 8 bits remaining in an element of type t so
     // not enough to fill a 16 bit int, so this cannot be transformed in an
     // index_exprt.
@@ -94,12 +94,12 @@ TEST_CASE("Build subexpression to access element at offset into struct")
   symbol_exprt s("struct", st);
 
   {
-    const auto result = get_subexpression_at_offset(s, 0, t, ns);
+    const auto result = get_subexpression_at_offset(s, bytest{0}, t, ns);
     REQUIRE(result.value() == member_exprt(s, "foo", t));
   }
 
   {
-    const auto result = get_subexpression_at_offset(s, 32 / 8, t, ns);
+    const auto result = get_subexpression_at_offset(s, bytest{32 / 8}, t, ns);
     REQUIRE(result.value() == member_exprt(s, "bar", t));
   }
 
@@ -117,7 +117,7 @@ TEST_CASE("Build subexpression to access element at offset into struct")
 
   {
     const signedbv_typet small_t(8);
-    const auto result = get_subexpression_at_offset(s, 1, small_t, ns);
+    const auto result = get_subexpression_at_offset(s, bytest{1}, small_t, ns);
     REQUIRE(
       result.value() ==
       make_byte_extract(