source: CIVL/examples/languageFeatures/bundleTest2_nonconc.cvl

#include <bundle.cvh>

$input int M, N, L, I;
$assume( 10 < M && 10 < N && 10 < L && 0 <= I && I < 10);

$input int X[M][N];
$input int Y[N][M];
$input int Z[L][M][N];

int x[M][N];
int y[N][M];
int z[L][M][N];
int zz[L][N][M];
int w[M][L][N];

int main() {
  int dat = 6;
  $bundle bun = $bundle_pack(&dat, sizeof(int));

  $bundle_unpack(bun, &w[1][2][3]);
  $assert(w[1][2][3] == dat);

  bun = $bundle_pack(X, sizeof(int) * M * N);
  // [M][N] in [M][L][N] from [0][0][0]
  $bundle_unpack(bun, w);
  $assert(
          w[ 0 ][ 0 ][ 0 ] == 
          X[ 0 ][ 0 ]
          );
  $assert(
          w[0][1][1] == X[1][1] && w[0][0][1] == X[0][1] && w[0][2][2] == X[2][2]
          );

    /*
      SALR bug, following will crash ... 
      $assert($forall (int i : 0 .. (M*N)-1)
      w[ i / (N*L) ][ (i % (N*L)) / N ][ ((i % (N*L))) % N ] == 
      X[ i / N ][ i % N ]
      );
    */
  $bundle_unpack(bun, x);
  $assert($forall (int i : 0 .. M-1) ($forall (int j : 0 .. N-1) 
                                      x[i][j] == X[i][j]
                                      ));
  // [M][N] -> [N][M]
  $bundle_unpack(bun, y);
  $assert($forall (int i : 0 .. N-1) ($forall (int j : 0 .. M-1) 
                                      y[i][j] == X[(i*M + j) / N][(i*M + j) % N]
                                      ));

  $bundle_unpack(bun, z);
  $assert($forall (int i : 0 .. M-1) ($forall (int j : 0 .. N-1) 
                                      z[0][i][j] == X[i][j]
                                      ));

  $bundle_unpack(bun, z[I]);
  $assert($forall (int i : 0 .. M-1) ($forall (int j : 0 .. N-1) 
                                      z[I][i][j] == X[i][j]
                                      ));

  // [M][N] -> [N][M]
  $bundle_unpack(bun, zz[I]);
  $assert($forall (int i : 0 .. N-1) ($forall (int j : 0 .. M-1) 
                                      zz[I][i][j] == X[(i*M + j) / N][(i*M + j) % N]
                                      ));

  bun = $bundle_pack(Z[I][0], sizeof(int) * N * I);

  // slice (&Z[I][0][0], I * N * sizeof_int) -> x[0][0]
  $bundle_unpack(bun, x);
  $assert($forall (int i : 0 .. (I-1))
          ($forall (int j : 0 .. (N-1)) x[i][j] == Z[I][i][j])
           );

  bun = $bundle_pack(Z[0][0], sizeof(int) * I);
  $bundle_unpack(bun, x);
  $assert($forall (int i : 0 .. (I-1))
          x[0][i] == Z[0][0][i]);
}