#pragma CIVL ACSL
typedef double T;
$input int B1, B2, B3, N1, N2, N3;
$assume(1<=N1 && N1<=B1 && 1<=N2 && N2<=B2 && 1<=N3 && N3<=B3);
$input T A[N1][N2], B[N2][N3];
T C[N1][N3];

void mul(T a[][], T b[][], T c[][], int n1, int n2, int n3) {
  /*@ loop assigns c[0..n1-1][0..n3-1];
    @ focus I | c[I][0..n3-1];
    @*/
  for (int i=0; i<n1; i++) {
    /*@ loop assigns c[i][0..n3-1];
      @ focus J | c[i][J];
      @*/
    for (int j=0; j<n3; j++) {
      T sum = (T)0;
      /*@ loop invariant 0 <= k <= n2;
        @ loop invariant sum == \sum(0, k-1, \lambda int t; a[i][t]*b[t][j]);
        @*/
      for (int k=0; k<n2; k++) {
        sum += a[i][k]*b[k][j];
      }
      c[i][j] = sum;
    }
  }
}

int main(void) {
  mul(A, B, C, N1, N2, N3);
  //@ focus I J;
  $assert($forall(int i : 0 .. N1-1; int j : 0 .. N3-1) C[i][j] == $sum(int k: 0..N2-1) A[i][k]*B[k][j]);
}