$input int n;
$assume(n > 0);

typedef struct {
  int x;
  float y;
} simple_t;

typedef struct {
  int x;
  float y;
  simple_t t;
  union {
    simple_t t;
    int x;
  } u;
  int ts[10];
} complex_t;


int main() {
  complex_t s3[n] = (complex_t[n])$lambda(int i) (complex_t){.t.y = .9, {.x = 42}};

  $assert($forall (int i : 0 .. n-1) s3[i].x == 0 && s3[i].y == 0 &&
	                             s3[i].t.x == 0 && s3[i].t.y == 0.9 &&
	                             s3[i].u.x == 42 && s3[i].u.t.x == 0); //s3[i].u.t is undefined
}