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 int p8 = __VERIFIER_nondet_int();
26 int lk8;
27
28 int p9 = __VERIFIER_nondet_int();
29 int lk9;
30
31
32 int cond;
33
34 while(1) {
35 cond = __VERIFIER_nondet_int();
36 if (cond == 0) {
37 goto out;
38 } else {}
39 lk1 = 0;
40
41 lk2 = 0;
42
43 lk3 = 0;
44
45 lk4 = 0;
46
47 lk5 = 0;
48
49 lk6 = 0;
50
51 lk7 = 0;
52
53 lk8 = 0;
54
55 lk9 = 0;
56
57
58
59 if (p1 != 0) {
60 lk1 = 1;
61 } else {}
62
63 if (p2 != 0) {
64 lk2 = 1;
65 } else {}
66
67 if (p3 != 0) {
68 lk3 = 1;
69 } else {}
70
71 if (p4 != 0) {
72 lk4 = 1;
73 } else {}
74
75 if (p5 != 0) {
76 lk5 = 1;
77 } else {}
78
79 if (p6 != 0) {
80 lk6 = 1;
81 } else {}
82
83 if (p7 != 0) {
84 lk7 = 1;
85 } else {}
86
87 if (p8 != 0) {
88 lk8 = 1;
89 } else {}
90
91 if (p9 != 0) {
92 lk9 = 1;
93 } else {}
94
95
96
97 if (p1 != 0) {
98 if (lk1 != 1) goto ERROR;
99 lk1 = 0;
100 } else {}
101
102 if (p2 != 0) {
103 if (lk2 != 1) goto ERROR;
104 lk2 = 0;
105 } else {}
106
107 if (p3 != 0) {
108 if (lk3 != 1) goto ERROR;
109 lk3 = 0;
110 } else {}
111
112 if (p4 != 0) {
113 if (lk4 != 1) goto ERROR;
114 lk4 = 0;
115 } else {}
116
117 if (p5 != 0) {
118 if (lk5 != 1) goto ERROR;
119 lk5 = 0;
120 } else {}
121
122 if (p6 != 0) {
123 if (lk6 != 1) goto ERROR;
124 lk6 = 0;
125 } else {}
126
127 if (p7 != 0) {
128 if (lk7 != 1) goto ERROR;
129 lk7 = 0;
130 } else {}
131
132 if (p8 != 0) {
133 if (lk8 != 1) goto ERROR;
134 lk8 = 0;
135 } else {}
136
137 if (p9 != 0) {
138 if (lk9 != 1) goto ERROR;
139 lk9 = 0;
140 } else {}
141
142 }
143 out:
144 return 0;
145 ERROR:
146 return 0;
147}
148