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
23 int cond;
24
25 while(1) {
26 cond = __VERIFIER_nondet_int();
27 if (cond == 0) {
28 goto out;
29 } else {}
30 lk1 = 0;
31
32 lk2 = 0;
33
34 lk3 = 0;
35
36 lk4 = 0;
37
38 lk5 = 0;
39
40 lk6 = 0;
41
42
43
44 if (p1 != 0) {
45 lk1 = 1;
46 } else {}
47
48 if (p2 != 0) {
49 lk2 = 1;
50 } else {}
51
52 if (p3 != 0) {
53 lk3 = 1;
54 } else {}
55
56 if (p4 != 0) {
57 lk4 = 1;
58 } else {}
59
60 if (p5 != 0) {
61 lk5 = 1;
62 } else {}
63
64 if (p6 != 0) {
65 lk6 = 1;
66 } else {}
67
68
69
70 if (p1 != 0) {
71 if (lk1 != 1) goto ERROR;
72 lk1 = 0;
73 } else {}
74
75 if (p2 != 0) {
76 if (lk2 != 1) goto ERROR;
77 lk2 = 0;
78 } else {}
79
80 if (p3 != 0) {
81 if (lk3 != 1) goto ERROR;
82 lk3 = 0;
83 } else {}
84
85 if (p4 != 0) {
86 if (lk4 != 1) goto ERROR;
87 lk4 = 0;
88 } else {}
89
90 if (p5 != 0) {
91 if (lk5 != 1) goto ERROR;
92 lk5 = 0;
93 } else {}
94
95 if (p6 != 0) {
96 if (lk6 != 1) goto ERROR;
97 lk6 = 0;
98 } else {}
99
100 }
101 out:
102 return 0;
103 ERROR:
104 return 0;
105}
106