#include <stdlib.h>

typedef struct M {
  int f;
} *B;

int main() {
  int n = 2;
  B x[2];
  for (int i = 0; i < n; i++) {
    x[i] = (B)malloc(sizeof(struct M));
    x[i]->f = 4;
  }
  $assert($forall(int i : 0 .. n - 1) x[i]->f == 4);
  $for(int i: 0 .. n-1)
    free(x[i]);
}