1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7char __VERIFIER_nondet_char();
8unsigned int __VERIFIER_nondet_uint();
9
10int main() {
11 int MAX = __VERIFIER_nondet_uint();
12 char str1[MAX], str2[MAX];
13 int cont, i, j;
14 cont = 0;
15
16 for (i=0; i<MAX; i++) {
17 str1[i]=__VERIFIER_nondet_char();
18 }
19 str1[MAX-1]= '\0';
20
21 j = 0;
22
23 for (i = MAX - 1; i >= 0; i--) {
24 str2[j] = str1[0];
25 j++;
26 }
27
28 j = MAX-1;
29 for (i=0; i<MAX; i++) {
30 __VERIFIER_assert(str1[i] == str2[j]);
31 j--;
32 }
33}