esbmc is missing support for the ArrayInitLoopExpr:

Represents a loop initializing the elements of an array.

The need to initialize the elements of an array occurs in a number of contexts:

in the implicit copy/move constructor for a class with an array member
when a lambda-expression captures an array by value
when a decomposition declaration decomposes an array

There are two subexpressions: a common expression (the source array) that is evaluated once up-front, and a per-element initializer that runs once for each array element.

Within the per-element initializer, the common expression may be referenced via an OpaqueValueExpr, and the current index may be obtained via an ArrayInitIndexExpr.

Testcase:

#include <cassert>

struct a
{
  int b[3];
};
int main()
{
  a d{};
  assert(d.b[0] == 0);
  assert(d.b[1] == 0);
  assert(d.b[2] == 0);
  d.b[0] = 1;
  assert(d.b[0] == 1);
  assert(d.b[1] == 0);
  assert(d.b[2] == 0);

  int i = 0;
  a e{d};
  assert(e.b[0] == 1);
  assert(e.b[1] == 0);
  assert(e.b[2] == 0);
  e.b[2] = 20;
  assert(e.b[0] == 1);
  assert(e.b[1] == 0);
  assert(e.b[2] == 20);

  return 0;
}