1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7extern unsigned int __VERIFIER_nondet_uint();
8extern int __VERIFIER_nondet_int();
9
10int main()
11{
12 unsigned int N_LIN=__VERIFIER_nondet_uint();
13 unsigned int N_COL=__VERIFIER_nondet_uint();
14 unsigned int j,k;
15 int matriz[N_COL][N_LIN], maior;
16
17 maior = __VERIFIER_nondet_int();
18 for(j=0;j<N_COL;j++)
19 for(k=0;k<N_LIN;k++)
20 {
21 matriz[j][k] = __VERIFIER_nondet_int();
22
23 if(matriz[j][k]>maior)
24 maior = matriz[j][k];
25 }
26
27 for(j=0;j<N_COL;j++)
28 for(k=0;k<N_LIN;k++)
29 __VERIFIER_assert(matriz[j][k]<maior);
30}