Byte update with a symbolic size skips the last element when the size is a multiple of the element size (unsound)

[bardiharborow]

CBMC version: 6.11.0 (cbmc-6.11.0)
Operating system: macOS 26.3, arm64
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: both assertions pass
What happened instead: both assertions fail

#include <stdint.h>
#include <string.h>

int main()
{
  unsigned n;
  __CPROVER_assume(n == 4 || n == 8);
  uint32_t src[2] = {0x11111111u, 0x22222222u};
  uint32_t dst[2] = {0, 0};
  memcpy(dst, src, n);
  __CPROVER_assert(dst[0] == 0x11111111u, "dst[0] fully copied");
  __CPROVER_assert(n != 8 || dst[1] == 0x22222222u, "dst[1] fully copied");
}

[main.assertion.1] line 13 dst[0] fully copied: FAILURE
[main.assertion.2] line 14 dst[1] fully copied: FAILURE
VERIFICATION FAILED

The copy writes n bytes, which fill exactly one or two elements of dst. CBMC finds a trace in which the element that holds the last copied byte keeps its old value, for both values of n. The result is unsound.

Which cases are affected

The copy size must be symbolic, the destination must be an array of multi-byte elements, and the copy must end exactly on an element boundary. memcpy, memmove, memset and __CPROVER_array_replace are all affected. With __CPROVER_assume(n == 8) alone the result is correct, because symex propagates n as a constant and the lowering takes a different path.

Cause

Symex produces a byte_update whose value has a non-constant size. The lowering goes to lower_byte_update_array_vector_unbounded, which builds an array comprehension. It computes the last updated element as

• updated_elements = (bound + subtype_size - 1) / subtype_size (L1717), which rounds up, and
• last_index = first_index + updated_elements - 1 (L1725).

So last_index already denotes the element that holds the last written byte. The upper bound of the comprehension (L1742) is nevertheless

index >= (tail_size == 0 ? last_index : last_index + 1)

where tail_size = (bound - initial_bytes) mod subtype_size is the number of bytes written into the last element beyond a full element. When the copy ends on an element boundary, tail_size is 0 and the range of unchanged elements starts at last_index itself. That element is therefore never updated. With n == 4 this is element 0, with n == 8 it is element 1.

The condition should simply be index > last_index, because last_index already accounts for a partial last element.