source: CIVL/examples/mpi/abstract_array.cvl

#include <mpi.h>

int main(void) {
  int nproc, rank;
  MPI_Init(NULL, NULL);
  MPI_Comm_size(MPI_COMM_WORLD, &nproc);
  MPI_Comm_rank(MPI_COMM_WORLD, &rank);
  int a[] = (int[3])$lambda(int i) rank;
  $assert(nproc >= 2);
  if (rank == 0)
    MPI_Send(a, 3, MPI_INT, 1, 0, MPI_COMM_WORLD);
  else {
    MPI_Recv(a, 3, MPI_INT, 0, 0, MPI_COMM_WORLD, MPI_STATUS_IGNORE);
    $assert($forall (int i:0 .. 2) a[i] == 0);
  }
  MPI_Finalize();
}