Skip to content

Commit f513331

Browse files
committed
fixup! Simplify byte_extract(byte_update(...)) without overlap
This fixes a bits/bytes confusing, resulting in missed optimisations of byte_extract(byte_update(...)) nestings when the byte_extract was at an offset higher than the update. Found while debugging model-checking/kani#1958.
1 parent 3302184 commit f513331

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/util/simplify_expr.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -1727,7 +1727,8 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
17271727
const auto update_size = pointer_offset_bits(bu.value().type(), ns);
17281728
if(
17291729
update_size.has_value() &&
1730-
*offset >= *update_offset * bu.get_bits_per_byte() + *update_size)
1730+
*offset * expr.get_bits_per_byte() >=
1731+
*update_offset * bu.get_bits_per_byte() + *update_size)
17311732
{
17321733
auto tmp = expr;
17331734
tmp.op() = bu.op();

0 commit comments

Comments
 (0)