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