1extern int __VERIFIER_nondet_int(void);
2void __VERIFIER_assert(int cond) {
3 if (!(cond)) {
4 ERROR: goto ERROR;
5 }
6 return;
7}
8extern unsigned int __VERIFIER_nondet_uint();
9
10int main()
11{
12 unsigned int M = __VERIFIER_nondet_uint();
13 int A[M], B[M], C[M];
14 unsigned int i;
15
16 for(i=0;i<M;i++)
17 A[i] = __VERIFIER_nondet_int();
18
19 for(i=0;i<M;i++)
20 B[i] = __VERIFIER_nondet_int();
21
22 for(i=0;i<M;i++)
23 C[i]=A[i]+B[i];
24
25 for(i=0;i<M;i++)
26 __VERIFIER_assert(C[i]==A[i]+B[i]);
27}