1extern char __VERIFIER_nondet_char(void);
2extern int __VERIFIER_nondet_int(void);
3extern long __VERIFIER_nondet_long(void);
4extern void *__VERIFIER_nondet_pointer(void);
5extern int __VERIFIER_nondet_int();
6
7int main() {
8 int s__state ;
9 int s__hit = __VERIFIER_nondet_int() ;
10 int s__verify_mode = __VERIFIER_nondet_int() ;
11 int s__session__peer = __VERIFIER_nondet_int() ;
12 unsigned long s__s3__tmp__new_cipher__algorithms = __VERIFIER_nondet_long() ;
13 int buf ;
14 int cb ;
15 int blastFlag ;
16 int tmp___1;
17
18 s__state = 8466;
19 blastFlag = 0;
20
21 while (1) {
22 if (s__state <= 8512 && blastFlag > 2) { goto ERROR; }
23 {
24 {
25 {
26 {
27 {
28 if (s__state == 8466) {
29 goto switch_1_8466;
30 } else {
31 if (s__state == 8496) {
32 goto switch_1_8496;
33 } else {
34 {
35 if (s__state == 8512) {
36 goto switch_1_8512;
37 } else {
38 {
39 if (s__state == 8528) {
40 goto switch_1_8528;
41 } else {
42 {
43 if (s__state == 8544) {
44 goto switch_1_8544;
45 } else {
46 {
47 if (s__state == 8560) {
48 goto switch_1_8560;
49 } else {
50 {
51 if (s__state == 8576) {
52 goto switch_1_8576;
53 } else {
54 {
55 if (s__state == 8592) {
56 goto switch_1_8592;
57 } else {
58 {
59 if (s__state == 8608) {
60 goto switch_1_8608;
61 } else {
62 {
63 if (s__state == 8640) {
64 goto switch_1_8640;
65 } else {
66 {
67 if (s__state == 8656) {
68 goto switch_1_8656;
69 } else {
70 {
71 if (s__state == 8672) {
72 goto switch_1_8672;
73 } else {
74 goto end;
75
76 switch_1_8466:
77 if (blastFlag == 0) {
78 blastFlag = 1;
79 }
80 s__state = 8496;
81 goto switch_1_break;
82
83 switch_1_8496:
84 if (blastFlag == 1) {
85 blastFlag = 2;
86 }
87 if (s__hit) {
88 s__state = 8656;
89 } else {
90 s__state = 8512;
91 }
92 goto switch_1_break;
93
94 switch_1_8512:
95 s__state = 8528;
96 goto switch_1_break;
97
98 switch_1_8528:
99 s__state = 8544;
100 goto switch_1_break;
101
102 switch_1_8544:
103 if (s__verify_mode + 1) {
104 if (s__session__peer != 0) {
105 if (s__verify_mode + 4) {
106 s__state = 8560;
107 } else {
108 goto _L___2;
109 }
110 } else {
111 _L___2:
112 if (s__s3__tmp__new_cipher__algorithms + 256UL) {
113 if (s__verify_mode + 2) {
114 goto _L___1;
115 } else {
116 s__state = 8560;
117 }
118 } else {
119 _L___1:
120 s__state = 8576;
121 }
122 }
123 } else {
124 s__state = 8560;
125 }
126 goto switch_1_break;
127
128 switch_1_8560:
129 s__state = 8576;
130 goto switch_1_break;
131
132 switch_1_8576:
133 tmp___1 = __VERIFIER_nondet_int();
134 if (tmp___1 == 2) {
135 s__state = 8466;
136 } else {
137 s__state = 8592;
138 }
139 goto switch_1_break;
140
141 switch_1_8592:
142 s__state = 8608;
143 goto switch_1_break;
144
145 switch_1_8608:
146 s__state = 8640;
147 goto switch_1_break;
148
149 switch_1_8640:
150 if (blastFlag == 3) {
151 blastFlag = 4;
152 }
153 if (s__hit) {
154 goto end;
155 } else {
156 s__state = 8656;
157 }
158 goto switch_1_break;
159
160 switch_1_8656:
161 if (blastFlag == 2) {
162 blastFlag = 3;
163 }
164 s__state = 8672;
165 goto switch_1_break;
166
167 switch_1_8672:
168 if (blastFlag == 4) {
169 blastFlag = 5;
170 } else {
171 if (blastFlag == 5) {
172 goto ERROR;
173 }
174 }
175 if (s__hit) {
176 s__state = 8640;
177 } else {
178 goto end;
179 }
180 goto switch_1_break;
181
182 }
183 }
184 }
185 }
186 }
187 }
188 }
189 }
190 }
191 }
192 }
193 }
194 }
195 }
196 }
197 }
198 }
199 }
200 }
201 }
202 }
203 }
204 }
205 }
206 }
207 }
208 }
209 switch_1_break: ;
210 }
211
212 end:
213 return (-1);
214 ERROR:
215 return (-1);
216}