Flaky behavior for memcpy and struct arrays.

[gtrepta]

CBMC version: 5.80.0
Operating system: Ubuntu Focal

main.c:

#include <assert.h>
#include <string.h>

#define SIZE 1

struct s {
  char a1[1];
  unsigned int a2_len;
  char a2[SIZE];
};

void main() {
  struct s s1;
  char buf[SIZE];

  __CPROVER_assume(s1.a2_len <= SIZE);
  memcpy(buf, s1.a2, s1.a2_len);
  assert(memcmp(buf, s1.a2, s1.a2_len)==0);
}

Exact command line resulting in the issue

cbmc --unwind <SIZE+1> main.c

What behaviour did you expect

A successful verification for the memcmp assertion, regardless of the value of SIZE or how the struct members are declared.

What happened instead

The assertions fails. But, for certain values of SIZE (ie. 4), the assertion passes. Or, with the a1 field omitted from the struct declaration, the assertion also passes.

[tautschnig]

Thank you for your bug report. This looks like a bug in our byte-operator flattening. Investigating.