diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 9e60faf8047..36cf7a18854 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -793,7 +793,29 @@ std::optional 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{