$input int N=5;
int m[N][N];

int main(){
  int k;

  $havoc(&m);
  $assume($forall (int i, j | 0<=i && i<N && 0<=j && j<N) m[i][j]>0);
  for(int i=0; i<N; i++)
    for(int j=0; j<N; j++)
      k=1/m[i][j];
}