#pragma CIVL ACSL
$input int M;
$assume(0 < M);
$input int N;
$assume(0 < N);
$input float A[M][N], B[M][N];

int main() {
  double C[M][N];
  //@ loop assigns C[0..M-1][0..N-1];
  //@ focus I | C[I][0..N-1];
  for (int i = 0; i < M; i++) {
    //@ loop assigns C[i][0..N-1];
    //@ focus J | C[i][J];
    for (int j = 0; j < N; j++) {
      C[i][j] = A[i][j]+B[i][j];
    }
  }
  
  //@ focus I J;
  $assert($forall(int i:0..M-1;int j:0..N-1) C[i][j] == A[i][j]+B[i][j]);
}