diff --git a/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp b/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp
index af884aae201..b368d4dfac4 100644
--- a/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp
+++ b/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp
@@ -6,17 +6,18 @@ Author: Diffblue Ltd.
 
 \*******************************************************************/
 
+#include <util/byte_operators.h>
+#include <util/pointer_expr.h>
+#include <util/symbol_table.h>
+
 #include <goto-programs/goto_trace.h>
 
 #include <java_bytecode/java_trace_validation.h>
 #include <java_bytecode/java_types.h>
-
 #include <testing-utils/message.h>
 #include <testing-utils/use_catch.h>
 
-#include <util/byte_operators.h>
-#include <util/pointer_expr.h>
-#include <util/symbol_table.h>
+#include <climits>
 
 TEST_CASE("java trace validation", "[core][java_trace_validation]")
 {
@@ -36,9 +37,9 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
   const index_exprt index_plain =
     index_exprt(exprt(ID_nil, array_typet(typet(), nil_exprt())), exprt());
   const byte_extract_exprt byte_little_endian = byte_extract_exprt(
-    ID_byte_extract_little_endian, exprt(), exprt(), typet());
-  const byte_extract_exprt byte_big_endian =
-    byte_extract_exprt(ID_byte_extract_big_endian, exprt(), exprt(), typet());
+    ID_byte_extract_little_endian, exprt(), exprt(), CHAR_BIT, typet());
+  const byte_extract_exprt byte_big_endian = byte_extract_exprt(
+    ID_byte_extract_big_endian, exprt(), exprt(), CHAR_BIT, typet());
   const address_of_exprt valid_address = address_of_exprt(valid_symbol_expr);
   const address_of_exprt invalid_address = address_of_exprt(exprt());
   const struct_exprt struct_plain =
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 4b1c5861f7b..a231c2ff8ee 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -161,7 +161,7 @@ void rw_range_sett::get_objects_byte_extract(
   }
   else
   {
-    *index *= 8;
+    *index *= be.get_bits_per_byte();
     if(*index >= *object_size_bits_opt)
       return;
 
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index da621d2cbcc..f73d0a24a6a 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -383,7 +383,8 @@ void symex_assignt::assign_byte_extract(
   else
     UNREACHABLE;
 
-  const byte_update_exprt new_rhs{byte_update_id, lhs.op(), lhs.offset(), rhs};
+  const byte_update_exprt new_rhs{
+    byte_update_id, lhs.op(), lhs.offset(), rhs, lhs.get_bits_per_byte()};
   const expr_skeletont new_skeleton =
     full_lhs.compose(expr_skeletont::remove_op0(lhs));
   assign_rec(lhs.op(), new_skeleton, new_rhs, guard);
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index 734c2e86251..c2871932357 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -48,11 +48,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   #if 0
   if(expr.id()==ID_byte_extract_big_endian &&
      expr.type().id()==ID_c_bit_field &&
-     (width%8)!=0)
+     (width%expr.get_bits_per_byte())!=0)
   {
     byte_extract_exprt tmp=expr;
     // round up
-    to_c_bit_field_type(tmp.type()).set_width(width+8-width%8);
+    to_c_bit_field_type(tmp.type()).set_width(
+      width+expr.get_bits_per_byte()-width%expr.get_bits_per_byte());
     convert_byte_extract(tmp, bv);
     bv.resize(width); // chop down
     return;
@@ -83,6 +84,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
       expr.id(),
       o.root_object(),
       plus_exprt(o.offset(), expr.offset()),
+      expr.get_bits_per_byte(),
       expr.type());
 
     return convert_bv(be);
@@ -104,11 +106,9 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   bv.resize(width);
 
   // see if the byte number is constant
-  unsigned byte_width=8;
-
   if(index.has_value())
   {
-    const mp_integer offset = *index * byte_width;
+    const mp_integer offset = *index * expr.get_bits_per_byte();
 
     for(std::size_t i=0; i<width; i++)
       // out of bounds?
@@ -119,7 +119,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   }
   else
   {
-    std::size_t bytes=op_bv.size()/byte_width;
+    std::size_t bytes = op_bv.size() / expr.get_bits_per_byte();
 
     if(prop.has_set_to())
     {
@@ -136,7 +136,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
       for(std::size_t i=0; i<bytes; i++)
       {
-        std::size_t offset=i*byte_width;
+        std::size_t offset = i * expr.get_bits_per_byte();
 
         for(std::size_t j=0; j<width; j++)
           if(offset+j<op_bv.size())
@@ -159,7 +159,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
         literalt e =
           convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
 
-        std::size_t offset=i*byte_width;
+        std::size_t offset = i * expr.get_bits_per_byte();
 
         for(std::size_t j=0; j<width; j++)
         {
diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp
index 7e3da3c1711..9216e17c8ad 100644
--- a/src/solvers/flattening/boolbv_byte_update.cpp
+++ b/src/solvers/flattening/boolbv_byte_update.cpp
@@ -38,7 +38,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 
   const bvt &value_bv=convert_bv(value);
   std::size_t update_width=value_bv.size();
-  std::size_t byte_width=8;
+  std::size_t byte_width = expr.get_bits_per_byte();
 
   if(update_width>bv.size())
     update_width=bv.size();
@@ -49,7 +49,7 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
   if(index.has_value())
   {
     // yes!
-    const mp_integer offset = *index * 8;
+    const mp_integer offset = *index * byte_width;
 
     if(offset+update_width>mp_integer(bv.size()) || offset<0)
     {
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
index 6d9a747a82b..f374b813c51 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/src/solvers/lowering/byte_operators.cpp
@@ -407,6 +407,7 @@ static exprt unpack_rec(
   bool little_endian,
   const optionalt<mp_integer> &offset_bytes,
   const optionalt<mp_integer> &max_bytes,
+  const std::size_t bits_per_byte,
   const namespacet &ns,
   bool unpack_byte_array = false);
 
@@ -414,12 +415,14 @@ static exprt unpack_rec(
 /// \param src: Source expression of array or vector type
 /// \param lower_bound: First index into \p src to be included in the result
 /// \param upper_bound: First index into \p src to be excluded from the result
+/// \param bits_per_byte: number of bits that make up a byte
 /// \param ns: Namespace
 /// \return Sequence of bytes.
 static exprt::operandst instantiate_byte_array(
   const exprt &src,
   std::size_t lower_bound,
   std::size_t upper_bound,
+  const std::size_t bits_per_byte,
   const namespacet &ns)
 {
   PRECONDITION(lower_bound <= upper_bound);
@@ -437,7 +440,7 @@ static exprt::operandst instantiate_byte_array(
     can_cast_type<bitvector_typet>(
       to_type_with_subtype(src.type()).subtype()) &&
     to_bitvector_type(to_type_with_subtype(src.type()).subtype()).get_width() ==
-      8);
+      bits_per_byte);
   exprt::operandst bytes;
   bytes.reserve(upper_bound - lower_bound);
   for(std::size_t i = lower_bound; i < upper_bound; ++i)
@@ -453,12 +456,14 @@ static exprt::operandst instantiate_byte_array(
 /// \param src: array/vector to unpack
 /// \param el_bytes: byte width of array/vector elements
 /// \param little_endian: true, iff assumed endianness is little-endian
+/// \param bits_per_byte: number of bits that make up a byte
 /// \param ns: namespace for type lookups
 /// \return Array expression holding unpacked elements or array comprehension
 static exprt unpack_array_vector_no_known_bounds(
   const exprt &src,
   std::size_t el_bytes,
   bool little_endian,
+  const std::size_t bits_per_byte,
   const namespacet &ns)
 {
   // TODO we either need a symbol table here or make array comprehensions
@@ -474,8 +479,10 @@ static exprt unpack_array_vector_no_known_bounds(
                       div_exprt{array_comprehension_index,
                                 from_integer(el_bytes, c_index_type())}};
 
-  exprt sub = unpack_rec(element, little_endian, {}, {}, ns, false);
-  exprt::operandst sub_operands = instantiate_byte_array(sub, 0, el_bytes, ns);
+  exprt sub =
+    unpack_rec(element, little_endian, {}, {}, bits_per_byte, ns, false);
+  exprt::operandst sub_operands =
+    instantiate_byte_array(sub, 0, el_bytes, bits_per_byte, ns);
 
   exprt body = sub_operands.front();
   const mod_exprt offset{
@@ -496,9 +503,10 @@ static exprt unpack_array_vector_no_known_bounds(
   return array_comprehension_exprt{
     std::move(array_comprehension_index),
     std::move(body),
-    array_typet{bv_typet{8},
-                mult_exprt{array_vector_size,
-                           from_integer(el_bytes, array_vector_size.type())}}};
+    array_typet{
+      bv_typet{bits_per_byte},
+      mult_exprt{
+        array_vector_size, from_integer(el_bytes, array_vector_size.type())}}};
 }
 
 /// Rewrite an array or vector into its individual bytes.
@@ -512,6 +520,7 @@ static exprt unpack_array_vector_no_known_bounds(
 ///   with nil values
 /// \param max_bytes: if set, use as upper bound of the number of bytes to
 ///   unpack
+/// \param bits_per_byte: number of bits that make up a byte
 /// \param ns: namespace for type lookups
 /// \return Array expression holding unpacked elements or array comprehension
 static exprt unpack_array_vector(
@@ -521,18 +530,19 @@ static exprt unpack_array_vector(
   bool little_endian,
   const optionalt<mp_integer> &offset_bytes,
   const optionalt<mp_integer> &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 + 7) / 8);
+  const std::size_t el_bytes = numeric_cast_v<std::size_t>(
+    (element_bits + bits_per_byte - 1) / bits_per_byte);
 
   if(!src_size.has_value() && !max_bytes.has_value())
   {
     PRECONDITION_WITH_DIAGNOSTICS(
-      el_bytes > 0 && element_bits % 8 == 0,
+      el_bytes > 0 && element_bits % bits_per_byte == 0,
       "unpacking of arrays with non-byte-aligned elements is not supported");
     return unpack_array_vector_no_known_bounds(
-      src, el_bytes, little_endian, ns);
+      src, el_bytes, little_endian, bits_per_byte, ns);
   }
 
   exprt::operandst byte_operands;
@@ -541,7 +551,7 @@ 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
   optionalt<mp_integer> num_elements = src_size;
-  if(element_bits > 0 && element_bits % 8 == 0)
+  if(element_bits > 0 && element_bits % bits_per_byte == 0)
   {
     if(!num_elements.has_value())
     {
@@ -556,7 +566,7 @@ static exprt unpack_array_vector(
       // insert offset_bytes-many nil bytes into the output array
       byte_operands.resize(
         numeric_cast_v<std::size_t>(*offset_bytes - (*offset_bytes % el_bytes)),
-        from_integer(0, bv_typet{8}));
+        from_integer(0, bv_typet{bits_per_byte}));
     }
   }
 
@@ -595,10 +605,10 @@ static exprt unpack_array_vector(
       element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
                         : el_bytes;
 
-    exprt sub =
-      unpack_rec(element, little_endian, {}, element_max_bytes, ns, true);
+    exprt sub = unpack_rec(
+      element, little_endian, {}, element_max_bytes, bits_per_byte, ns, true);
     exprt::operandst sub_operands =
-      instantiate_byte_array(sub, 0, element_max_bytes_int, ns);
+      instantiate_byte_array(sub, 0, element_max_bytes_int, bits_per_byte, ns);
     byte_operands.insert(
       byte_operands.end(), sub_operands.begin(), sub_operands.end());
 
@@ -609,7 +619,7 @@ static exprt unpack_array_vector(
   const std::size_t size = byte_operands.size();
   return array_exprt(
     std::move(byte_operands),
-    array_typet{bv_typet{8}, from_integer(size, size_type())});
+    array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())});
 }
 
 /// Extract bytes from a sequence of bitvector-typed elements.
@@ -621,6 +631,7 @@ static exprt unpack_array_vector(
 ///   with nil values
 /// \param max_bytes: if set, use as upper bound of the number of bytes to
 ///   unpack
+/// \param bits_per_byte: number of bits that make up a byte
 /// \param ns: namespace for type lookups
 static void process_bit_fields(
   exprt::operandst &&bit_fields,
@@ -629,13 +640,20 @@ static void process_bit_fields(
   bool little_endian,
   const optionalt<mp_integer> &offset_bytes,
   const optionalt<mp_integer> &max_bytes,
+  const std::size_t bits_per_byte,
   const namespacet &ns)
 {
   const concatenation_exprt concatenation{std::move(bit_fields),
                                           bv_typet{total_bits}};
 
-  exprt sub =
-    unpack_rec(concatenation, little_endian, offset_bytes, max_bytes, ns, true);
+  exprt sub = unpack_rec(
+    concatenation,
+    little_endian,
+    offset_bytes,
+    max_bytes,
+    bits_per_byte,
+    ns,
+    true);
 
   dest.insert(
     dest.end(),
@@ -650,6 +668,7 @@ static void process_bit_fields(
 ///   with nil values
 /// \param max_bytes: if set, use as upper bound of the number of bytes to
 ///   unpack
+/// \param bits_per_byte: number of bits that make up a byte
 /// \param ns: namespace for type lookups
 /// \return array_exprt holding unpacked elements
 static array_exprt unpack_struct(
@@ -657,6 +676,7 @@ static array_exprt unpack_struct(
   bool little_endian,
   const optionalt<mp_integer> &offset_bytes,
   const optionalt<mp_integer> &max_bytes,
+  const std::size_t bits_per_byte,
   const namespacet &ns)
 {
   const struct_typet &struct_type = to_struct_type(ns.follow(src.type()));
@@ -688,7 +708,7 @@ static array_exprt unpack_struct(
       simplify(member, ns);
 
     // Is it a byte-aligned member?
-    if(member_offset_bits % 8 == 0)
+    if(member_offset_bits % bits_per_byte == 0)
     {
       if(bit_fields.has_value())
       {
@@ -699,13 +719,14 @@ static array_exprt unpack_struct(
           little_endian,
           offset_in_member,
           max_bytes_left,
+          bits_per_byte,
           ns);
         bit_fields.reset();
       }
 
       if(offset_bytes.has_value())
       {
-        offset_in_member = *offset_bytes - member_offset_bits / 8;
+        offset_in_member = *offset_bytes - member_offset_bits / 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)
@@ -714,15 +735,15 @@ static array_exprt unpack_struct(
 
       if(max_bytes.has_value())
       {
-        max_bytes_left = *max_bytes - member_offset_bits / 8;
+        max_bytes_left = *max_bytes - member_offset_bits / bits_per_byte;
         if(*max_bytes_left < 0)
           break;
       }
     }
 
     if(
-      member_offset_bits % 8 != 0 ||
-      (component_bits.has_value() && *component_bits % 8 != 0))
+      member_offset_bits % bits_per_byte != 0 ||
+      (component_bits.has_value() && *component_bits % bits_per_byte != 0))
     {
       if(!bit_fields.has_value())
         bit_fields = std::make_pair(exprt::operandst{}, std::size_t{0});
@@ -743,7 +764,13 @@ static array_exprt unpack_struct(
       "all preceding members should have been processed");
 
     exprt sub = unpack_rec(
-      member, little_endian, offset_in_member, max_bytes_left, ns, true);
+      member,
+      little_endian,
+      offset_in_member,
+      max_bytes_left,
+      bits_per_byte,
+      ns,
+      true);
 
     byte_operands.insert(
       byte_operands.end(),
@@ -755,6 +782,7 @@ static array_exprt unpack_struct(
   }
 
   if(bit_fields.has_value())
+  {
     process_bit_fields(
       std::move(bit_fields->first),
       bit_fields->second,
@@ -762,33 +790,41 @@ static array_exprt unpack_struct(
       little_endian,
       offset_in_member,
       max_bytes_left,
+      bits_per_byte,
       ns);
+  }
 
   const std::size_t size = byte_operands.size();
-  return array_exprt{std::move(byte_operands),
-                     array_typet{bv_typet{8}, from_integer(size, size_type())}};
+  return array_exprt{
+    std::move(byte_operands),
+    array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())}};
 }
 
 /// Rewrite a complex_exprt into its individual bytes.
 /// \param src: complex-typed expression to unpack
 /// \param little_endian: true, iff assumed endianness is little-endian
+/// \param bits_per_byte: number of bits that make up a byte
 /// \param ns: namespace for type lookups
 /// \return array_exprt holding unpacked elements
-static array_exprt
-unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
+static array_exprt unpack_complex(
+  const exprt &src,
+  bool little_endian,
+  const std::size_t bits_per_byte,
+  const namespacet &ns)
 {
   const complex_typet &complex_type = to_complex_type(src.type());
   const typet &subtype = complex_type.subtype();
 
   auto subtype_bits = pointer_offset_bits(subtype, ns);
   CHECK_RETURN(subtype_bits.has_value());
-  CHECK_RETURN(*subtype_bits % 8 == 0);
+  CHECK_RETURN(*subtype_bits % bits_per_byte == 0);
 
   exprt sub_real = unpack_rec(
     complex_real_exprt{src},
     little_endian,
     mp_integer{0},
-    *subtype_bits / 8,
+    *subtype_bits / bits_per_byte,
+    bits_per_byte,
     ns,
     true);
   exprt::operandst byte_operands = std::move(sub_real.operands());
@@ -797,7 +833,8 @@ unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
     complex_imag_exprt{src},
     little_endian,
     mp_integer{0},
-    *subtype_bits / 8,
+    *subtype_bits / bits_per_byte,
+    bits_per_byte,
     ns,
     true);
   byte_operands.insert(
@@ -806,8 +843,9 @@ unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
     std::make_move_iterator(sub_imag.operands().end()));
 
   const std::size_t size = byte_operands.size();
-  return array_exprt{std::move(byte_operands),
-                     array_typet{bv_typet{8}, from_integer(size, size_type())}};
+  return array_exprt{
+    std::move(byte_operands),
+    array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())}};
 }
 
 /// Rewrite an object into its individual bytes.
@@ -817,6 +855,7 @@ unpack_complex(const exprt &src, bool little_endian, const namespacet &ns)
 ///   nil values
 /// \param max_bytes: if set, use as upper bound of the number of bytes to
 ///   unpack
+/// \param bits_per_byte: number of bits that make up a byte
 /// \param ns: namespace for type lookups
 /// \param unpack_byte_array: if true, return unmodified \p src iff it is an
 //    array of bytes
@@ -826,6 +865,7 @@ static exprt unpack_rec(
   bool little_endian,
   const optionalt<mp_integer> &offset_bytes,
   const optionalt<mp_integer> &max_bytes,
+  const std::size_t bits_per_byte,
   const namespacet &ns,
   bool unpack_byte_array)
 {
@@ -837,7 +877,7 @@ static exprt unpack_rec(
     auto element_bits = pointer_offset_bits(subtype, ns);
     CHECK_RETURN(element_bits.has_value());
 
-    if(!unpack_byte_array && *element_bits == 8)
+    if(!unpack_byte_array && *element_bits == bits_per_byte)
       return src;
 
     const auto constant_size_opt = numeric_cast<mp_integer>(array_type.size());
@@ -848,6 +888,7 @@ static exprt unpack_rec(
       little_endian,
       offset_bytes,
       max_bytes,
+      bits_per_byte,
       ns);
   }
   else if(src.type().id() == ID_vector)
@@ -858,7 +899,7 @@ static exprt unpack_rec(
     auto element_bits = pointer_offset_bits(subtype, ns);
     CHECK_RETURN(element_bits.has_value());
 
-    if(!unpack_byte_array && *element_bits == 8)
+    if(!unpack_byte_array && *element_bits == bits_per_byte)
       return src;
 
     return unpack_array_vector(
@@ -868,15 +909,17 @@ static exprt unpack_rec(
       little_endian,
       offset_bytes,
       max_bytes,
+      bits_per_byte,
       ns);
   }
   else if(src.type().id() == ID_complex)
   {
-    return unpack_complex(src, little_endian, ns);
+    return unpack_complex(src, little_endian, bits_per_byte, ns);
   }
   else if(src.type().id() == ID_struct || src.type().id() == ID_struct_tag)
   {
-    return unpack_struct(src, little_endian, offset_bytes, max_bytes, ns);
+    return unpack_struct(
+      src, little_endian, offset_bytes, max_bytes, bits_per_byte, ns);
   }
   else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
   {
@@ -889,7 +932,13 @@ static exprt unpack_rec(
       member_exprt member{
         src, widest_member->first.get_name(), widest_member->first.type()};
       return unpack_rec(
-        member, little_endian, offset_bytes, widest_member->second, ns, true);
+        member,
+        little_endian,
+        offset_bytes,
+        widest_member->second,
+        bits_per_byte,
+        ns,
+        true);
     }
   }
   else if(src.type().id() == ID_pointer)
@@ -899,6 +948,7 @@ static exprt unpack_rec(
       little_endian,
       offset_bytes,
       max_bytes,
+      bits_per_byte,
       ns,
       unpack_byte_array);
   }
@@ -909,6 +959,7 @@ static exprt unpack_rec(
       little_endian,
       offset_bytes,
       max_bytes,
+      bits_per_byte,
       ns,
       unpack_byte_array);
   }
@@ -919,6 +970,7 @@ static exprt unpack_rec(
       little_endian,
       offset_bytes,
       max_bytes,
+      bits_per_byte,
       ns,
       unpack_byte_array);
   }
@@ -935,7 +987,7 @@ static exprt unpack_rec(
 
     if(max_bytes.has_value())
     {
-      const auto max_bits = *max_bytes * 8;
+      const auto max_bits = *max_bytes * bits_per_byte;
       if(little_endian)
       {
         last_bit = std::min(last_bit, max_bits);
@@ -948,15 +1000,15 @@ static exprt unpack_rec(
 
     auto const src_as_bitvector = typecast_exprt::conditional_cast(
       src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
-    auto const byte_type = bv_typet{8};
+    auto const byte_type = bv_typet{bits_per_byte};
     exprt::operandst byte_operands;
-    for(; bit_offset < last_bit; bit_offset += 8)
+    for(; bit_offset < last_bit; bit_offset += bits_per_byte)
     {
       PRECONDITION(
         pointer_offset_bits(src_as_bitvector.type(), ns).has_value());
       extractbits_exprt extractbits(
         src_as_bitvector,
-        from_integer(bit_offset + 7, c_index_type()),
+        from_integer(bit_offset + bits_per_byte - 1, c_index_type()),
         from_integer(bit_offset, c_index_type()),
         byte_type);
 
@@ -972,11 +1024,11 @@ static exprt unpack_rec(
     const std::size_t size = byte_operands.size();
     return array_exprt(
       std::move(byte_operands),
-      array_typet{bv_typet{8}, from_integer(size, size_type())});
+      array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())});
   }
 
   return array_exprt(
-    {}, array_typet{bv_typet{8}, from_integer(0, size_type())});
+    {}, array_typet{bv_typet{bits_per_byte}, from_integer(0, size_type())});
 }
 
 /// Rewrite a byte extraction of an array/vector-typed result to byte extraction
@@ -1010,7 +1062,9 @@ static exprt lower_byte_extract_array_vector(
     {
       plus_exprt new_offset(
         unpacked.offset(),
-        from_integer(i * element_bits / 8, unpacked.offset().type()));
+        from_integer(
+          i * element_bits / src.get_bits_per_byte(),
+          unpacked.offset().type()));
 
       byte_extract_exprt tmp(unpacked);
       tmp.type() = subtype;
@@ -1045,7 +1099,9 @@ static exprt lower_byte_extract_array_vector(
     typecast_exprt::conditional_cast(
       mult_exprt{
         array_comprehension_index,
-        from_integer(element_bits / 8, array_comprehension_index.type())},
+        from_integer(
+          element_bits / src.get_bits_per_byte(),
+          array_comprehension_index.type())},
       unpacked.offset().type())};
 
   byte_extract_exprt body(unpacked);
@@ -1074,7 +1130,7 @@ static optionalt<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 % 8 != 0)
+  if(!subtype_bits.has_value() || *subtype_bits % src.get_bits_per_byte() != 0)
     return {};
 
   // offset remains unchanged
@@ -1083,7 +1139,8 @@ static optionalt<exprt> lower_byte_extract_complex(
 
   const plus_exprt new_offset{
     unpacked.offset(),
-    from_integer(*subtype_bits / 8, unpacked.offset().type())};
+    from_integer(
+      *subtype_bits / src.get_bits_per_byte(), unpacked.offset().type())};
   byte_extract_exprt imag{unpacked};
   imag.type() = subtype;
   imag.offset() = simplify_expr(new_offset, ns);
@@ -1168,10 +1225,15 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
 
   byte_extract_exprt unpacked(src);
   unpacked.op() = unpack_rec(
-    src.op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
+    src.op(),
+    little_endian,
+    lower_bound_int_opt,
+    upper_bound_int_opt,
+    src.get_bits_per_byte(),
+    ns);
   CHECK_RETURN(
     to_bitvector_type(to_type_with_subtype(unpacked.op().type()).subtype())
-      .get_width() == 8);
+      .get_width() == src.get_bits_per_byte());
 
   if(src.type().id() == ID_array || src.type().id() == ID_vector)
   {
@@ -1181,7 +1243,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     // subtype size that does not fit byte boundaries; currently we fall back to
     // stitching together consecutive elements down below
     auto element_bits = pointer_offset_bits(subtype, ns);
-    if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
+    if(
+      element_bits.has_value() && *element_bits >= 1 &&
+      *element_bits % src.get_bits_per_byte() == 0)
     {
       return lower_byte_extract_array_vector(
         src, unpacked, subtype, *element_bits, ns);
@@ -1210,7 +1274,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 == 0 ||
-        *component_bits % 8 != 0)
+        *component_bits % src.get_bits_per_byte() != 0)
       {
         failed=true;
         break;
@@ -1270,7 +1334,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 == 8,
+    subtype_bits.has_value() && *subtype_bits == src.get_bits_per_byte(),
     "offset bits are byte aligned");
 
   auto size_bits = pointer_offset_bits(unpacked.type(), ns);
@@ -1284,7 +1348,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     size_bits = op0_bits;
   }
 
-  mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
+  mp_integer num_bytes =
+    (*size_bits) / src.get_bits_per_byte() +
+    (((*size_bits) % src.get_bits_per_byte() == 0) ? 0 : 1);
 
   // get 'width'-many bytes, and concatenate
   const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
@@ -1324,7 +1390,8 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   else // width_bytes>=2
   {
     concatenation_exprt concatenation(
-      std::move(op), adjust_width(*subtype, width_bytes * 8));
+      std::move(op),
+      adjust_width(*subtype, width_bytes * src.get_bits_per_byte()));
 
     endianness_mapt map(concatenation.type(), little_endian, ns);
     return bv_to_expr(concatenation, src.type(), map, ns);
@@ -1514,7 +1581,11 @@ static exprt lower_byte_update_array_vector_unbounded(
                                       from_integer(1, first_index.type())}}}};
   exprt update_value = lower_byte_extract(
     byte_extract_exprt{
-      extract_opcode, value_as_byte_array, std::move(offset_expr), subtype},
+      extract_opcode,
+      value_as_byte_array,
+      std::move(offset_expr),
+      src.get_bits_per_byte(),
+      subtype},
     ns);
 
   // The number of target array/vector elements being replaced, not including
@@ -1555,12 +1626,15 @@ static exprt lower_byte_update_array_vector_unbounded(
       src.id(),
       index_exprt{src.op(), last_index},
       from_integer(0, src.offset().type()),
-      byte_extract_exprt{extract_opcode,
-                         value_as_byte_array,
-                         mult_exprt{typecast_exprt::conditional_cast(
-                                      last_index, subtype_size.type()),
-                                    subtype_size},
-                         array_typet{bv_typet{8}, tail_size}}},
+      byte_extract_exprt{
+        extract_opcode,
+        value_as_byte_array,
+        mult_exprt{
+          typecast_exprt::conditional_cast(last_index, subtype_size.type()),
+          subtype_size},
+        src.get_bits_per_byte(),
+        array_typet{bv_typet{src.get_bits_per_byte()}, tail_size}},
+      src.get_bits_per_byte()},
     ns);
 
   if_exprt array_comprehension_body{
@@ -1653,10 +1727,13 @@ static exprt lower_byte_update_array_vector_non_const(
       src.id(),
       index_exprt{src.op(), first_index},
       update_offset,
-      byte_extract_exprt{extract_opcode,
-                         value_as_byte_array,
-                         from_integer(0, src.offset().type()),
-                         array_typet{bv_typet{8}, initial_bytes}}},
+      byte_extract_exprt{
+        extract_opcode,
+        value_as_byte_array,
+        from_integer(0, src.offset().type()),
+        src.get_bits_per_byte(),
+        array_typet{bv_typet{src.get_bits_per_byte()}, initial_bytes}},
+      src.get_bits_per_byte()},
     ns);
 
   if(value_as_byte_array.id() != ID_array)
@@ -1709,10 +1786,13 @@ static exprt lower_byte_update_array_vector_non_const(
         src.id(),
         index_exprt{src.op(), where},
         from_integer(0, src.offset().type()),
-        byte_extract_exprt{extract_opcode,
-                           value_as_byte_array,
-                           std::move(offset_expr),
-                           array_typet{bv_typet{8}, subtype_size}}},
+        byte_extract_exprt{
+          extract_opcode,
+          value_as_byte_array,
+          std::move(offset_expr),
+          src.get_bits_per_byte(),
+          array_typet{bv_typet{src.get_bits_per_byte()}, subtype_size}},
+        src.get_bits_per_byte()},
       ns);
 
     result.add_to_operands(std::move(where), std::move(element));
@@ -1736,7 +1816,11 @@ static exprt lower_byte_update_array_vector_non_const(
           extract_opcode,
           value_as_byte_array,
           from_integer(offset, src.offset().type()),
-          array_typet{bv_typet{8}, from_integer(tail_size, size_type())}}},
+          src.get_bits_per_byte(),
+          array_typet{
+            bv_typet{src.get_bits_per_byte()},
+            from_integer(tail_size, size_type())}},
+        src.get_bits_per_byte()},
       ns);
 
     result.add_to_operands(std::move(where), std::move(element));
@@ -1773,7 +1857,8 @@ static exprt lower_byte_update_array_vector(
   // fall back to bytewise updates in all non-constant or dubious cases
   if(
     !size.is_constant() || !src.offset().is_constant() ||
-    !subtype_bits.has_value() || *subtype_bits == 0 || *subtype_bits % 8 != 0 ||
+    !subtype_bits.has_value() || *subtype_bits == 0 ||
+    *subtype_bits % src.get_bits_per_byte() != 0 ||
     non_const_update_bound.has_value() || value_as_byte_array.id() != ID_array)
   {
     return lower_byte_update_array_vector_non_const(
@@ -1790,17 +1875,23 @@ static exprt lower_byte_update_array_vector(
 
   std::size_t i = 0;
   // copy the prefix not affected by the update
-  for(; i < num_elements && (i + 1) * *subtype_bits <= offset_bytes * 8; ++i)
+  for(; i < num_elements &&
+        (i + 1) * *subtype_bits <= offset_bytes * src.get_bits_per_byte();
+      ++i)
+  {
     elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())});
+  }
 
   // the modified elements
   for(; i < num_elements &&
         i * *subtype_bits <
-          (offset_bytes + value_as_byte_array.operands().size()) * 8;
+          (offset_bytes + value_as_byte_array.operands().size()) *
+            src.get_bits_per_byte();
       ++i)
   {
-    mp_integer update_offset = offset_bytes - i * (*subtype_bits / 8);
-    mp_integer update_elements = *subtype_bits / 8;
+    mp_integer update_offset =
+      offset_bytes - i * (*subtype_bits / src.get_bits_per_byte());
+    mp_integer update_elements = *subtype_bits / src.get_bits_per_byte();
     exprt::operandst::const_iterator first =
       value_as_byte_array.operands().begin();
     exprt::operandst::const_iterator end = value_as_byte_array.operands().end();
@@ -1830,7 +1921,10 @@ static exprt lower_byte_update_array_vector(
       from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()),
       array_exprt{
         std::move(update_values),
-        array_typet{bv_typet{8}, from_integer(update_size, size_type())}}};
+        array_typet{
+          bv_typet{src.get_bits_per_byte()},
+          from_integer(update_size, size_type())}},
+      src.get_bits_per_byte()};
     elements.push_back(lower_byte_operators(bu, ns));
   }
 
@@ -1879,8 +1973,10 @@ static exprt lower_byte_update_struct(
     // compute the update offset relative to this struct member - will be
     // negative if we are already in the middle of the update or beyond it
     exprt offset = simplify_expr(
-      minus_exprt{src.offset(),
-                  from_integer(member_offset_bits / 8, src.offset().type())},
+      minus_exprt{
+        src.offset(),
+        from_integer(
+          member_offset_bits / src.get_bits_per_byte(), src.offset().type())},
       ns);
     auto offset_bytes = numeric_cast<mp_integer>(offset);
     // we don't need to update anything when
@@ -1890,7 +1986,7 @@ static exprt lower_byte_update_struct(
     // offset
     if(
       offset_bytes.has_value() &&
-      (*offset_bytes * 8 >= *element_width ||
+      (*offset_bytes * src.get_bits_per_byte() >= *element_width ||
        (value_as_byte_array.id() == ID_array && *offset_bytes < 0 &&
         -*offset_bytes >= value_as_byte_array.operands().size())))
     {
@@ -1911,7 +2007,8 @@ static exprt lower_byte_update_struct(
         extract_opcode,
         src.op(),
         from_integer(0, src.offset().type()),
-        array_typet{bv_typet{8}, src_size_opt.value()}};
+        src.get_bits_per_byte(),
+        array_typet{bv_typet{src.get_bits_per_byte()}, src_size_opt.value()}};
 
       byte_update_exprt bu = src;
       bu.set_op(lower_byte_extract(byte_extract_expr, ns));
@@ -1923,6 +2020,7 @@ static exprt lower_byte_update_struct(
           lower_byte_update(
             bu, value_as_byte_array, non_const_update_bound, ns),
           from_integer(0, src.offset().type()),
+          src.get_bits_per_byte(),
           src.type()},
         ns);
     }
@@ -1931,7 +2029,8 @@ static exprt lower_byte_update_struct(
     // value. If the size of the update is unknown, then we need to leave some
     // of this work to a back-end solver via the non_const_update_bound branch
     // below.
-    mp_integer update_elements = (*element_width + 7) / 8;
+    mp_integer update_elements =
+      (*element_width + src.get_bits_per_byte() - 1) / src.get_bits_per_byte();
     std::size_t first = 0;
     if(*offset_bytes < 0)
     {
@@ -1956,16 +2055,17 @@ static exprt lower_byte_update_struct(
     std::size_t end = first + numeric_cast_v<std::size_t>(update_elements);
     if(value_as_byte_array.id() == ID_array)
       end = std::min(end, value_as_byte_array.operands().size());
-    exprt::operandst update_values =
-      instantiate_byte_array(value_as_byte_array, first, end, ns);
+    exprt::operandst update_values = instantiate_byte_array(
+      value_as_byte_array, first, end, src.get_bits_per_byte(), ns);
     const std::size_t update_size = update_values.size();
 
     // With an upper bound on the size of the update established, construct the
     // actual update expression. If the exact size of the update is unknown,
     // make the size expression conditional.
     exprt update_size_expr = from_integer(update_size, size_type());
-    array_exprt update_expr{std::move(update_values),
-                            array_typet{bv_typet{8}, update_size_expr}};
+    array_exprt update_expr{
+      std::move(update_values),
+      array_typet{bv_typet{src.get_bits_per_byte()}, update_size_expr}};
     optionalt<exprt> member_update_bound;
     if(non_const_update_bound.has_value())
     {
@@ -1995,7 +2095,7 @@ static exprt lower_byte_update_struct(
     // We have established the bytes to use for the update, but now need to
     // account for sub-byte members.
     const std::size_t shift =
-      numeric_cast_v<std::size_t>(member_offset_bits % 8);
+      numeric_cast_v<std::size_t>(member_offset_bits % src.get_bits_per_byte());
     const std::size_t element_bits_int =
       numeric_cast_v<std::size_t>(*element_width);
 
@@ -2013,7 +2113,12 @@ static exprt lower_byte_update_struct(
     }
 
     // Finally construct the updated member.
-    byte_update_exprt bu{src.id(), std::move(member), offset, update_expr};
+    byte_update_exprt bu{
+      src.id(),
+      std::move(member),
+      offset,
+      update_expr,
+      src.get_bits_per_byte()};
     exprt updated_element =
       lower_byte_update(bu, update_expr, member_update_bound, ns);
 
@@ -2094,9 +2199,9 @@ static exprt lower_byte_update(
     auto element_width = pointer_offset_bits(*subtype, ns);
     CHECK_RETURN(element_width.has_value());
     CHECK_RETURN(*element_width > 0);
-    CHECK_RETURN(*element_width % 8 == 0);
+    CHECK_RETURN(*element_width % src.get_bits_per_byte() == 0);
 
-    if(*element_width == 8)
+    if(*element_width == src.get_bits_per_byte())
     {
       if(value_as_byte_array.id() != ID_array)
       {
@@ -2155,11 +2260,16 @@ static exprt lower_byte_update(
       update_bytes = value_as_byte_array.operands();
     else
     {
-      update_bytes =
-        instantiate_byte_array(value_as_byte_array, 0, (type_bits + 7) / 8, ns);
+      update_bytes = instantiate_byte_array(
+        value_as_byte_array,
+        0,
+        (type_bits + src.get_bits_per_byte() - 1) / src.get_bits_per_byte(),
+        src.get_bits_per_byte(),
+        ns);
     }
 
-    const std::size_t update_size_bits = update_bytes.size() * 8;
+    const std::size_t update_size_bits =
+      update_bytes.size() * src.get_bits_per_byte();
     const std::size_t bit_width = std::max(type_bits, update_size_bits);
 
     const bool is_little_endian = src.id() == ID_byte_update_little_endian;
@@ -2186,6 +2296,7 @@ static exprt lower_byte_update(
         src.id() == ID_byte_update_little_endian,
         mp_integer{0},
         mp_integer{update_bytes.size()},
+        src.get_bits_per_byte(),
         ns);
       CHECK_RETURN(src_as_bytes.id() == ID_array);
       CHECK_RETURN(src_as_bytes.operands().size() == update_bytes.size());
@@ -2213,14 +2324,16 @@ static exprt lower_byte_update(
     }
 
     const typet &offset_type = src.offset().type();
-    mult_exprt offset_times_eight{src.offset(), from_integer(8, offset_type)};
+    mult_exprt offset_in_bits{
+      src.offset(), from_integer(src.get_bits_per_byte(), offset_type)};
 
     const binary_predicate_exprt offset_ge_zero{
-      offset_times_eight, ID_ge, from_integer(0, offset_type)};
+      offset_in_bits, ID_ge, from_integer(0, offset_type)};
 
-    if_exprt mask_shifted{offset_ge_zero,
-                          shl_exprt{mask, offset_times_eight},
-                          lshr_exprt{mask, offset_times_eight}};
+    if_exprt mask_shifted{
+      offset_ge_zero,
+      shl_exprt{mask, offset_in_bits},
+      lshr_exprt{mask, offset_in_bits}};
     if(!is_little_endian)
       mask_shifted.true_case().swap(mask_shifted.false_case());
 
@@ -2249,9 +2362,10 @@ static exprt lower_byte_update(
       zero_extended = value;
 
     // shift the value
-    if_exprt value_shifted{offset_ge_zero,
-                           shl_exprt{zero_extended, offset_times_eight},
-                           lshr_exprt{zero_extended, offset_times_eight}};
+    if_exprt value_shifted{
+      offset_ge_zero,
+      shl_exprt{zero_extended, offset_in_bits},
+      lshr_exprt{zero_extended, offset_in_bits}};
     if(!is_little_endian)
       value_shifted.true_case().swap(value_shifted.false_case());
 
@@ -2314,6 +2428,7 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
   const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
                                     ? ID_byte_extract_little_endian
                                     : ID_byte_extract_big_endian;
+  const std::size_t bits_per_byte = src.get_bits_per_byte();
 
   if(!update_size_expr_opt.value().is_constant())
     non_const_update_bound = *update_size_expr_opt;
@@ -2327,7 +2442,7 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
       update_bits.has_value(), "constant size-of should imply fixed bit width");
     const size_t update_bits_int = numeric_cast_v<size_t>(*update_bits);
 
-    if(update_bits_int % 8 != 0)
+    if(update_bits_int % bits_per_byte != 0)
     {
       DATA_INVARIANT(
         can_cast_type<bitvector_typet>(update_value.type()),
@@ -2338,13 +2453,14 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
         simplify_expr(
           plus_exprt{
             src.offset(),
-            from_integer(update_bits_int / 8, src.offset().type())},
+            from_integer(update_bits_int / bits_per_byte, src.offset().type())},
           ns),
-        bv_typet{8}};
+        src.get_bits_per_byte(),
+        bv_typet{bits_per_byte}};
       const exprt overlapping_byte =
         lower_byte_extract(overlapping_byte_extract, ns);
 
-      size_t n_extra_bits = 8 - update_bits_int % 8;
+      size_t n_extra_bits = bits_per_byte - update_bits_int % bits_per_byte;
       extractbits_exprt extra_bits{
         overlapping_byte, n_extra_bits - 1, 0, bv_typet{n_extra_bits}};
 
@@ -2356,8 +2472,8 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
     }
     else
     {
-      update_size_expr_opt =
-        from_integer(update_bits_int / 8, update_size_expr_opt->type());
+      update_size_expr_opt = from_integer(
+        update_bits_int / bits_per_byte, update_size_expr_opt->type());
     }
   }
 
@@ -2365,7 +2481,8 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
     extract_opcode,
     update_value,
     from_integer(0, src.offset().type()),
-    array_typet{bv_typet{8}, *update_size_expr_opt}};
+    src.get_bits_per_byte(),
+    array_typet{bv_typet{bits_per_byte}, *update_size_expr_opt}};
 
   const exprt value_as_byte_array = lower_byte_extract(byte_extract_expr, ns);
 
diff --git a/src/util/byte_operators.cpp b/src/util/byte_operators.cpp
index a5d14030835..863e15d8ab3 100644
--- a/src/util/byte_operators.cpp
+++ b/src/util/byte_operators.cpp
@@ -47,11 +47,13 @@ static irep_idt byte_update_id()
 byte_extract_exprt
 make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
 {
-  return byte_extract_exprt{byte_extract_id(), _op, _offset, _type};
+  return byte_extract_exprt{
+    byte_extract_id(), _op, _offset, config.ansi_c.char_width, _type};
 }
 
 byte_update_exprt
 make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
 {
-  return byte_update_exprt{byte_update_id(), _op, _offset, _value};
+  return byte_update_exprt{
+    byte_update_id(), _op, _offset, _value, config.ansi_c.char_width};
 }
diff --git a/src/util/byte_operators.h b/src/util/byte_operators.h
index e7e99c89818..8a81da60ff0 100644
--- a/src/util/byte_operators.h
+++ b/src/util/byte_operators.h
@@ -32,12 +32,15 @@ class byte_extract_exprt : public binary_exprt
     irep_idt _id,
     const exprt &_op,
     const exprt &_offset,
+    std::size_t bits_per_byte,
     const typet &_type)
     : binary_exprt(_op, _id, _offset, _type)
   {
     INVARIANT(
       _id == ID_byte_extract_little_endian || _id == ID_byte_extract_big_endian,
       "byte_extract_exprt: Invalid ID");
+
+    set_bits_per_byte(bits_per_byte);
   }
 
   exprt &op() { return op0(); }
@@ -45,6 +48,16 @@ class byte_extract_exprt : public binary_exprt
 
   const exprt &op() const { return op0(); }
   const exprt &offset() const { return op1(); }
+
+  std::size_t get_bits_per_byte() const
+  {
+    return get_size_t(ID_bits_per_byte);
+  }
+
+  void set_bits_per_byte(std::size_t bits_per_byte)
+  {
+    set_size_t(ID_bits_per_byte, bits_per_byte);
+  }
 };
 
 template <>
@@ -81,12 +94,15 @@ class byte_update_exprt : public ternary_exprt
     irep_idt _id,
     const exprt &_op,
     const exprt &_offset,
-    const exprt &_value)
+    const exprt &_value,
+    std::size_t bits_per_byte)
     : ternary_exprt(_id, _op, _offset, _value, _op.type())
   {
     INVARIANT(
       _id == ID_byte_update_little_endian || _id == ID_byte_update_big_endian,
       "byte_update_exprt: Invalid ID");
+
+    set_bits_per_byte(bits_per_byte);
   }
 
   void set_op(exprt e)
@@ -105,6 +121,16 @@ class byte_update_exprt : public ternary_exprt
   const exprt &op() const { return op0(); }
   const exprt &offset() const { return op1(); }
   const exprt &value() const { return op2(); }
+
+  std::size_t get_bits_per_byte() const
+  {
+    return get_size_t(ID_bits_per_byte);
+  }
+
+  void set_bits_per_byte(std::size_t bits_per_byte)
+  {
+    set_size_t(ID_bits_per_byte, bits_per_byte);
+  }
 };
 
 template <>
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index d91cb73e809..664f01ecec3 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1725,12 +1725,15 @@ 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 * 8 + *el_size)
+    while(mp_integer(const_bits.size()) <
+          *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 * 8),
+      numeric_cast_v<std::size_t>(*offset * expr.get_bits_per_byte()),
       numeric_cast_v<std::size_t>(*el_size));
 
     auto tmp = bits2expr(
@@ -1742,7 +1745,8 @@ 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 * 8) % (*el_size) == 0 &&
+    expr.op().id() == ID_array_of &&
+    (*offset * expr.get_bits_per_byte()) % (*el_size) == 0 &&
     *el_size <=
       pointer_offset_bits(to_array_of_expr(expr.op()).what().type(), ns))
   {
@@ -1777,12 +1781,13 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
     },
     ns);
   if(
-    bits.has_value() && mp_integer(bits->size()) >= *el_size + *offset * 8 &&
+    bits.has_value() &&
+    mp_integer(bits->size()) >= *el_size + *offset * expr.get_bits_per_byte() &&
     !struct_has_flexible_array_member)
   {
     std::string bits_cut = std::string(
       bits.value(),
-      numeric_cast_v<std::size_t>(*offset * 8),
+      numeric_cast_v<std::size_t>(*offset * expr.get_bits_per_byte()),
       numeric_cast_v<std::size_t>(*el_size));
 
     auto tmp = bits2expr(
@@ -1933,10 +1938,12 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
     root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
   {
     byte_extract_exprt be(
-      expr.id()==ID_byte_update_little_endian ?
-        ID_byte_extract_little_endian :
-        ID_byte_extract_big_endian,
-      value, offset, expr.type());
+      expr.id() == ID_byte_update_little_endian ? ID_byte_extract_little_endian
+                                                : ID_byte_extract_big_endian,
+      value,
+      offset,
+      expr.get_bits_per_byte(),
+      expr.type());
 
     return changed(simplify_byte_extract(be));
   }
@@ -1959,7 +1966,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
       if(val_bits.has_value())
       {
         root_bits->replace(
-          numeric_cast_v<std::size_t>(*offset_int * 8),
+          numeric_cast_v<std::size_t>(*offset_int * expr.get_bits_per_byte()),
           numeric_cast_v<std::size_t>(*val_size),
           *val_bits);
 
@@ -2095,13 +2102,15 @@ 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) % 8 != 0)
+      if(
+        !m_size_bits.has_value() || *m_size_bits == 0 ||
+        (*m_size_bits) % expr.get_bits_per_byte() != 0)
       {
         result_expr.make_nil();
         break;
       }
 
-      mp_integer m_size_bytes = (*m_size_bits) / 8;
+      mp_integer m_size_bytes = (*m_size_bits) / expr.get_bits_per_byte();
 
       // is that member part of the update?
       if(*m_offset + m_size_bytes <= *offset_int)
@@ -2131,7 +2140,8 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
           ID_byte_update_little_endian,
           member_exprt(root, component.get_name(), component.type()),
           from_integer(*offset_int - *m_offset, offset.type()),
-          value);
+          value,
+          expr.get_bits_per_byte());
 
         to_with_expr(result_expr).new_value().swap(v);
       }
@@ -2149,6 +2159,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
           ID_byte_extract_little_endian,
           value,
           from_integer(*m_offset - *offset_int, offset.type()),
+          expr.get_bits_per_byte(),
           component.type());
 
         to_with_expr(result_expr).new_value().swap(v);
@@ -2166,8 +2177,10 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
     auto el_size =
       pointer_offset_bits(to_type_with_subtype(op_type).subtype(), ns);
 
-    if(!el_size.has_value() || *el_size == 0 ||
-       (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
+    if(
+      !el_size.has_value() || *el_size == 0 ||
+      (*el_size) % expr.get_bits_per_byte() != 0 ||
+      (*val_size) % expr.get_bits_per_byte() != 0)
     {
       return unchanged(expr);
     }
@@ -2177,29 +2190,34 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
     mp_integer m_offset_bits=0, val_offset=0;
     Forall_operands(it, result)
     {
-      if(*offset_int * 8 + (*val_size) <= m_offset_bits)
+      if(*offset_int * expr.get_bits_per_byte() + (*val_size) <= m_offset_bits)
         break;
 
-      if(*offset_int * 8 < m_offset_bits + *el_size)
+      if(*offset_int * expr.get_bits_per_byte() < m_offset_bits + *el_size)
       {
-        mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - *offset_int;
+        mp_integer bytes_req =
+          (m_offset_bits + *el_size) / expr.get_bits_per_byte() - *offset_int;
         bytes_req-=val_offset;
-        if(val_offset + bytes_req > (*val_size) / 8)
-          bytes_req = (*val_size) / 8 - 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;
 
         byte_extract_exprt new_val(
           ID_byte_extract_little_endian,
           value,
           from_integer(val_offset, offset.type()),
+          expr.get_bits_per_byte(),
           array_typet(
-            unsignedbv_typet(8), from_integer(bytes_req, offset.type())));
+            unsignedbv_typet(expr.get_bits_per_byte()),
+            from_integer(bytes_req, offset.type())));
 
         *it = byte_update_exprt(
           expr.id(),
           *it,
           from_integer(
-            *offset_int + val_offset - m_offset_bits / 8, offset.type()),
-          new_val);
+            *offset_int + val_offset - m_offset_bits / expr.get_bits_per_byte(),
+            offset.type()),
+          new_val,
+          expr.get_bits_per_byte());
 
         *it = simplify_rec(*it); // recursive call
 
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 3e88dc6e838..d500ee158e0 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -152,7 +152,11 @@ simplify_exprt::simplify_member(const member_exprt &expr)
         simplify_plus(plus_exprt(struct_offset, member_offset));
 
       byte_extract_exprt result(
-        op.id(), byte_extract_expr.op(), final_offset, expr.type());
+        op.id(),
+        byte_extract_expr.op(),
+        final_offset,
+        byte_extract_expr.get_bits_per_byte(),
+        expr.type());
 
       return changed(simplify_byte_extract(result)); // recursive call
     }
diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp
index 8d37f036282..dbf81fbdf3f 100644
--- a/unit/solvers/lowering/byte_operators.cpp
+++ b/unit/solvers/lowering/byte_operators.cpp
@@ -55,11 +55,13 @@ TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
     REQUIRE(bit_string2.has_value());
     REQUIRE(*bit_string == *bit_string2);
 
-    const byte_extract_exprt be1{little_endian ? ID_byte_extract_little_endian
-                                               : ID_byte_extract_big_endian,
-                                 sixteen_bits,
-                                 from_integer(0, c_index_type()),
-                                 bit_array_type};
+    const byte_extract_exprt be1{
+      little_endian ? ID_byte_extract_little_endian
+                    : ID_byte_extract_big_endian,
+      sixteen_bits,
+      from_integer(0, c_index_type()),
+      config.ansi_c.char_width,
+      bit_array_type};
     const exprt lower_be1 = lower_byte_extract(be1, ns);
     REQUIRE(lower_be1 == *array_of_bits);
   }
@@ -80,11 +82,13 @@ TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
     REQUIRE(bit_string2.has_value());
     REQUIRE(*bit_string == *bit_string2);
 
-    const byte_extract_exprt be1{little_endian ? ID_byte_extract_little_endian
-                                               : ID_byte_extract_big_endian,
-                                 sixteen_bits,
-                                 from_integer(0, c_index_type()),
-                                 bit_array_type};
+    const byte_extract_exprt be1{
+      little_endian ? ID_byte_extract_little_endian
+                    : ID_byte_extract_big_endian,
+      sixteen_bits,
+      from_integer(0, c_index_type()),
+      config.ansi_c.char_width,
+      bit_array_type};
     const exprt lower_be1 = lower_byte_extract(be1, ns);
     REQUIRE(lower_be1 == *array_of_bits);
   }
@@ -107,7 +111,8 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       ID_byte_extract_little_endian,
       deadbeef,
       from_integer(1, c_index_type()),
-      signedbv_typet(8));
+      config.ansi_c.char_width,
+      signedbv_typet(config.ansi_c.char_width));
 
     THEN("byte_extract lowering yields the expected value")
     {
@@ -136,6 +141,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       ID_byte_extract_little_endian,
       deadbeef,
       from_integer(1, c_index_type()),
+      config.ansi_c.char_width,
       struct_typet(
         {{"unbounded_array",
           array_typet(
@@ -164,6 +170,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       ID_byte_extract_little_endian,
       deadbeef,
       from_integer(1, c_index_type()),
+      config.ansi_c.char_width,
       union_typet(
         {{"unbounded_array",
           array_typet(
@@ -192,6 +199,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       ID_byte_extract_little_endian,
       deadbeef,
       from_integer(1, c_index_type()),
+      config.ansi_c.char_width,
       union_typet{});
 
     THEN("byte_extract lowering does not raise an exception")
@@ -217,6 +225,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       ID_byte_extract_little_endian,
       s,
       from_integer(1, c_index_type()),
+      config.ansi_c.char_width,
       unsignedbv_typet(16));
 
     THEN("byte_extract lowering yields the expected value")
@@ -332,7 +341,11 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
             REQUIRE(r.has_value());
 
             const byte_extract_exprt be(
-              endianness, *s, from_integer(2, c_index_type()), t2);
+              endianness,
+              *s,
+              from_integer(2, c_index_type()),
+              config.ansi_c.char_width,
+              t2);
 
             const exprt lower_be = lower_byte_extract(be, ns);
             const exprt lower_be_s = simplify_expr(lower_be, ns);
@@ -366,7 +379,8 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
       ID_byte_update_little_endian,
       deadbeef,
       from_integer(1, c_index_type()),
-      from_integer(0x42, unsignedbv_typet(8)));
+      from_integer(0x42, unsignedbv_typet(8)),
+      config.ansi_c.char_width);
 
     THEN("byte_update lowering yields the expected value")
     {
@@ -486,7 +500,11 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
             REQUIRE(r.has_value());
 
             const byte_update_exprt bu(
-              endianness, *s, from_integer(2, c_index_type()), *u);
+              endianness,
+              *s,
+              from_integer(2, c_index_type()),
+              *u,
+              config.ansi_c.char_width);
 
             const exprt lower_bu = lower_byte_operators(bu, ns);
             const exprt lower_bu_s = simplify_expr(lower_bu, ns);
diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp
index 1b4e58fc15f..3272a837480 100644
--- a/unit/util/expr_cast/expr_cast.cpp
+++ b/unit/util/expr_cast/expr_cast.cpp
@@ -147,6 +147,7 @@ SCENARIO("expr_dynamic_cast",
       ID_byte_extract_little_endian,
       symbol_exprt(typet()),
       constant_exprt("0", typet()),
+      1, // arbitrary integer
       typet());
     THEN("try_expr_dynamic_cast<byte_extract_expr> returns non-empty")
     {
@@ -159,6 +160,7 @@ SCENARIO("expr_dynamic_cast",
       ID_byte_extract_big_endian,
       symbol_exprt(typet()),
       constant_exprt("0", typet()),
+      1, // arbitrary integer
       typet());
     THEN("try_expr_dynamic_cast<byte_extract_expr> returns non-empty")
     {
@@ -183,6 +185,7 @@ SCENARIO("can_cast_expr", "[core][utils][expr_cast][can_cast_expr]")
       ID_byte_extract_little_endian,
       symbol_exprt(typet()),
       constant_exprt("0", typet()),
+      1, // arbitrary integer
       typet());
     THEN("can_expr_expr<byte_extract_expr> returns true")
     {
@@ -195,6 +198,7 @@ SCENARIO("can_cast_expr", "[core][utils][expr_cast][can_cast_expr]")
       ID_byte_extract_big_endian,
       symbol_exprt(typet()),
       constant_exprt("0", typet()),
+      1, // arbitrary integer
       typet());
     THEN("can_expr_expr<byte_extract_expr> returns true")
     {