[melver]

Consider a store that straddles two members of a packed struct:

#pragma pack(push, 1)
struct S
{
  uint32_t a; // bytes 0..3
  uint64_t c; // bytes 4..11
  uint32_t d; // bytes 12..15
};
#pragma pack(pop)

struct S s;
*(uint64_t *)((char *)&s + 8) = v; // bytes 8..15

The simplifier splits the resulting byte_update of s into per-member updates:

s.c = byte_update(s.c, 4, v); // v's bytes 0..3 -> c's bytes 4..7
s.d = byte_extract(v, 4);     // v's bytes 4..7 -> d

The simplifier passes all 8 bytes of v as the update value, but only 4 of them fit in c from offset 4 onwards; v's remaining 4 bytes extend past the end of c. Such updates are well-formed: lower_byte_update applies the overlapping part, as does the variable-offset encoding in convert_byte_update for non-negative offsets. The constant-offset encoding, however, treated any update that did not fit entirely within the updated object as out of bounds and discarded all of it. Bytes 8..11 of s thus kept their old value, while bytes 12..15 were updated, on both little- and big-endian configurations. The SMT2 back-end, which lowers byte operators, was not affected.

Make the constant-offset encoding update only the bits that lie within the updated object. This also handles negative constant offsets.

Assisted-by: Antigravity

---

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.