1extern int __VERIFIER_nondet_int();
2int main()
3{
4 int p1 = __VERIFIER_nondet_int();
5 int lk1;
6
7 int p2 = __VERIFIER_nondet_int();
8 int lk2;
9
10 int p3 = __VERIFIER_nondet_int();
11 int lk3;
12
13 int p4 = __VERIFIER_nondet_int();
14 int lk4;
15
16 int p5 = __VERIFIER_nondet_int();
17 int lk5;
18
19 int p6 = __VERIFIER_nondet_int();
20 int lk6;
21
22 int p7 = __VERIFIER_nondet_int();
23 int lk7;
24
25
26 int cond;
27
28 while(1) {
29 cond = __VERIFIER_nondet_int();
30 if (cond == 0) {
31 goto out;
32 } else {}
33 lk1 = 0;
34
35 lk2 = 0;
36
37 lk3 = 0;
38
39 lk4 = 0;
40
41 lk5 = 0;
42
43 lk6 = 0;
44
45 lk7 = 0;
46
47
48
49 if (p1 != 0) {
50 lk1 = 1;
51 } else {}
52
53 if (p2 != 0) {
54 lk2 = 1;
55 } else {}
56
57 if (p3 != 0) {
58 lk3 = 1;
59 } else {}
60
61 if (p4 != 0) {
62 lk4 = 1;
63 } else {}
64
65 if (p5 != 0) {
66 lk5 = 1;
67 } else {}
68
69 if (p6 != 0) {
70 lk6 = 1;
71 } else {}
72
73 if (p7 != 0) {
74 lk7 = 1;
75 } else {}
76
77
78
79 if (p1 != 0) {
80 if (lk1 != 1) goto ERROR;
81 lk1 = 0;
82 } else {}
83
84 if (p2 != 0) {
85 if (lk2 != 1) goto ERROR;
86 lk2 = 0;
87 } else {}
88
89 if (p3 != 0) {
90 if (lk3 != 1) goto ERROR;
91 lk3 = 0;
92 } else {}
93
94 if (p4 != 0) {
95 if (lk4 != 1) goto ERROR;
96 lk4 = 0;
97 } else {}
98
99 if (p5 != 0) {
100 if (lk5 != 1) goto ERROR;
101 lk5 = 0;
102 } else {}
103
104 if (p6 != 0) {
105 if (lk6 != 1) goto ERROR;
106 lk6 = 0;
107 } else {}
108
109 if (p7 != 0) {
110 if (lk7 != 1) goto ERROR;
111 lk7 = 0;
112 } else {}
113
114 }
115 out:
116 return 0;
117 ERROR:
118 return 0;
119}
120