Rewrite byte_extract from multi-dimensional array

As a follow-up to 78839a9: add support for rewriting
multiple-of-element size access to arrays when working with
multi-dimensional arrays.

Author: tautschnig

src/util/pointer_offset_size.cpp

@@ -793,7 +793,29 @@ std::optional<exprt> get_subexpression_at_offset(
       const exprt &other_factor =
         offset_mult.op0().is_constant() ? offset_mult.op1() : offset_mult.op0();
 
-      if(const_factor % (*elem_size_bits / config.ansi_c.char_width) != 0)
+      const mp_integer elem_size_bytes =
+        *elem_size_bits / config.ansi_c.char_width;
+      if(
+        array_type->element_type().id() == ID_array &&
+        const_factor < elem_size_bytes && elem_size_bytes % const_factor == 0)
+      {
+        const mp_integer index_divider = elem_size_bytes / const_factor;
+        exprt index = div_exprt{
+          other_factor, from_integer(index_divider, other_factor.type())};
+        exprt remaining_offset = mult_exprt{
+          mod_exprt{
+            other_factor, from_integer(index_divider, other_factor.type())},
+          from_integer(const_factor, other_factor.type())};
+
+        return get_subexpression_at_offset(
+          index_exprt{
+            expr,
+            typecast_exprt::conditional_cast(index, array_type->index_type())},
+          remaining_offset,
+          target_type,
+          ns);
+      }
+      else if(const_factor % elem_size_bytes != 0)
         return {};
 
       exprt index = mult_exprt{