1extern void __VERIFIER_assume(int);
2void __VERIFIER_assert(int cond) {
3 if (!(cond)) {
4 ERROR: goto ERROR;
5 }
6 return;
7}
8
9
10
11extern char __VERIFIER_nondet_char();
12
13main()
14{
15 char string_A[5], string_B[5];
16 int i, j, nc_A, nc_B, found=0;
17
18
19 for(i=0; i<5; i++)
20 string_A[i]=__VERIFIER_nondet_char();
21 __VERIFIER_assume(string_A[5 -1]=='\0');
22
23 for(i=0; i<5; i++)
24 string_B[i]=__VERIFIER_nondet_char();
25 __VERIFIER_assume(string_B[5 -1]=='\0');
26
27 nc_A = 0;
28 while(string_A[nc_A]!='\0')
29 nc_A++;
30
31 nc_B = 0;
32 while(string_B[nc_B]!='\0')
33 nc_B++;
34
35 __VERIFIER_assume(nc_B >= nc_A);
36
37
38 i=j=0;
39 while((i<nc_A) && (j<nc_B))
40 {
41 if(string_A[i] == string_B[j])
42 {
43 i++;
44 j++;
45 }
46 else
47 {
48 i = i-j+1;
49 j = 0;
50 }
51 }
52
53 found = (j>nc_B-1)<<i;
54
55 __VERIFIER_assert(found == 0 || found == 1);
56
57}