Unexpected failure with array_copy/array_equals

[remi-delmas-3000]

The assertion in this program fails unexpectedly, but passes with size = N for many different concrete N

#include <stdlib.h>
#include <assert.h>
size_t nondet_size_t();
int main() {
  size_t size = nondet_size_t();
  if (0 < size && size <= __CPROVER_max_malloc_size) {
    char *a = malloc(size);
    char *b = malloc(size);
    __CPROVER_array_copy(a, b);
    assert(__CPROVER_array_equal(a, b));
  }
}

CBMC version: 5.95.1
Operating system: Ubuntu 20.04, macOS 14.3
Exact command line resulting in the issue: cbmc array_copy.c
What behaviour did you expect: SUCCESS for assert(__CPROVER_array_equal(a, b));
What happened instead: FAILURE for assert(__CPROVER_array_equal(a, b));

[tautschnig]

The problem is caused by use creating a fresh object-size symbol for each allocation of dynamic size. So these are two arrays of size symex_dynamic::dynamic_object_size!0#1 and symex_dynamic::dynamic_object_size$0!0#1, respectively. Looks like we need to fix how we build those object sizes.