Skip to content

Commit 7774e1c

Browse files
committed
Do not unnecessarily restrict byte update lowering of arrays
Arrays of arrays of non-constant size (as found in regression/cbmc/Multi_Dimensional_Array6) can still be lowered by the more general lowering code, although doing so is expensive.
1 parent 25a7b36 commit 7774e1c

File tree

1 file changed

+1
-5
lines changed

1 file changed

+1
-5
lines changed

src/solvers/lowering/byte_operators.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2057,11 +2057,7 @@ static exprt lower_byte_update(
20572057
subtype = to_array_type(src.type()).subtype();
20582058

20592059
auto element_width = pointer_offset_bits(*subtype, ns);
2060-
CHECK_RETURN(element_width.has_value());
2061-
CHECK_RETURN(*element_width > 0);
2062-
CHECK_RETURN(*element_width % 8 == 0);
2063-
2064-
if(*element_width == 8)
2060+
if(element_width.has_value() && *element_width == 8)
20652061
{
20662062
if(value_as_byte_array.id() != ID_array)
20672063
{

0 commit comments

Comments
 (0)