[melver]

A memcpy with a symbolic size into an array of non-byte elements could leave
the destination unchanged:

uint32_t src[4], d[4];
size_t n; // symbolic, e.g. n == 4 || n == 8
memcpy(d, src, n);
assert(d[0] == src[0]); // fails

The memcpy model turns this into byte_update(d, 0, src_n), where src_n is
an unsigned char[n]. Because that size is not constant, byte-operator
lowering has to encode the update with a symbolic bound, and it got this wrong
in two independent ways. Every back-end uses this lowering, so the default SAT
back-end, SMT2 solvers (Z3, CVC5), and --arrays-uf-always were all affected.

1. Updates spanning several elements
   (lower_byte_update_array_vector_unbounded): when the update ended exactly
   at an element boundary, the last updated element was treated as untouched.
   For n == 4, d did not change at all. When the update ended partway
   into a later element, that element's partial update ignored the update
   offset and used the wrong bytes. All elements after the first now use the
   same formula, which removes the last-element special case and is a net
   reduction in code.

2. Updates starting partway into an element (bit-vector case of
   lower_byte_update): update bytes past the symbolic bound were replaced by
   the element's original byte i, when update byte i actually lands at
   byte offset + i. For memcpy((uint8_t *)d + 1, src, 1), bytes 2 and 3 of
   d[0] became copies of bytes 1 and 2. This also affected byte updates of
   struct members and unions.

Assisted-by: Antigravity

---

• Each commit message has a non-empty body, explaining why the change was made.
• 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/ (bug fix only)
• 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). (no performance claims)
• 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.