source: CIVL/examples/svcomp17/Problem01_label15_false-unreach-call.c@ 1aaefd4

main test-branch
Last change on this file since 1aaefd4 was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago

Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 21.3 KB
Line 
1int calculate_output(int);
2extern void __VERIFIER_error(void);
3extern int __VERIFIER_nondet_int(void);
4extern void exit(int);
5
6 // inputs
7 int a= 1;
8 int d= 4;
9 int e= 5;
10 int f= 6;
11 int c= 3;
12 int b= 2;
13
14 // outputs
15 int u = 21;
16 int v = 22;
17 int w = 23;
18 int x = 24;
19 int y = 25;
20 int z = 26;
21
22 int a17 = 1;
23 int a7 = 0;
24 int a20 = 1;
25 int a8 = 15;
26 int a12 = 8;
27 int a16 = 5;
28 int a21 = 1;
29
30 int calculate_output(int input) {
31 if((((a8==15)&&(((((a21==1)&&(((a16==5)||(a16==6))&&(input==1)))&&(a20==1))&&(a17==1))&&!(a7==1)))&&(a12==8))){
32 a16 = 5;
33 a20 = 0;
34 return 24;
35 } else if((((((((input==5)&&((((a16==6)&&(a17==1))||(!(a17==1)&&(a16==4)))||(!(a17==1)&&(a16==5))))&&(a20==1))&&(a12==8))&&(a7==1))&&!(a21==1))&&(a8==13))){
36 a20 = 0;
37 a16 = 6;
38 a17 = 0;
39 a8 = 15;
40 a7 = 0;
41 a21 = 1;
42 return 26;
43 } else if(((!(a7==1)&&((((a16==6)&&((a21==1)&&((a17==1)&&(input==3))))&&!(a20==1))&&(a8==15)))&&(a12==8))){
44 a20 = 1;
45 a16 = 4;
46 a7 = 1;
47 a8 = 13;
48 return -1;
49 } else if(((a17==1)&&((!(a7==1)&&(((a21==1)&&((((a16==5)||(a16==6))&&(input==6))&&(a20==1)))&&(a8==15)))&&(a12==8)))){
50 a8 = 13;
51 a7 = 1;
52 a16 = 4;
53 return -1;
54 } else if((((input==3)&&((((a16==6)&&((!(a20==1)&&(!(a7==1)&&!(a17==1)))&&(a8==15)))&&(a21==1))||((((a8==13)&&((a20==1)&&((a17==1)&&(a7==1))))&&(a16==4))&&!(a21==1))))&&(a12==8))){
55 a7 = 0;
56 a20 = 1;
57 a21 = 1;
58 a16 = 4;
59 a17 = 1;
60 a8 = 13;
61 return -1;
62 } else if((((a17==1)&&(((a21==1)&&((!(a7==1)&&((input==4)&&(a8==15)))&&!(a20==1)))&&(a12==8)))&&(a16==6))){
63 a17 = 0;
64 return 26;
65 } else if((((a12==8)&&(((a21==1)&&((((input==5)&&!(a7==1))&&(a8==15))&&(a16==5)))&&!(a20==1)))&&!(a17==1))){
66 a7 = 1;
67 a16 = 4;
68 a8 = 13;
69 a20 = 1;
70 a17 = 1;
71 return -1;
72 } else if(((a12==8)&&((input==1)&&(((a21==1)&&(((a8==15)&&((!(a17==1)&&!(a7==1))&&!(a20==1)))&&(a16==6)))||(!(a21==1)&&((a16==4)&&((a8==13)&&(((a17==1)&&(a7==1))&&(a20==1))))))))){
73 a7 = 1;
74 a17 = 1;
75 a21 = 0;
76 a20 = 1;
77 a8 = 13;
78 a16 = 5;
79 return 26;
80 } else if(((((!(a17==1)&&(!(a7==1)&&((a21==1)&&((a8==15)&&(input==4)))))&&!(a20==1))&&(a12==8))&&(a16==4))){
81 a17 = 1;
82 a16 = 5;
83 return 21;
84 } else if(((((((a16==6)&&((!(a20==1)&&(!(a17==1)&&!(a7==1)))&&(a8==15)))&&(a21==1))||(((a16==4)&&(((a20==1)&&((a17==1)&&(a7==1)))&&(a8==13)))&&!(a21==1)))&&(input==2))&&(a12==8))){
85 a7 = 0;
86 a20 = 1;
87 a8 = 14;
88 a16 = 4;
89 a21 = 1;
90 a17 = 0;
91 return -1;
92 } else if(((a8==13)&&(!(a21==1)&&((((input==3)&&((((a20==1)&&!(a17==1))&&(a16==6))||((!(a20==1)&&(a17==1))&&(a16==4))))&&(a12==8))&&(a7==1))))){
93 a16 = 4;
94 a17 = 1;
95 a20 = 1;
96 return 26;
97 } else if(((((a21==1)&&((a12==8)&&((input==1)&&(((!(a20==1)&&(a17==1))&&(a16==4))||(((a16==5)&&(!(a17==1)&&(a20==1)))||((a16==6)&&(!(a17==1)&&(a20==1))))))))&&!(a7==1))&&(a8==15))){
98 a16 = 6;
99 a20 = 1;
100 a17 = 0;
101 return 24;
102 } else if((((a16==5)&&(((a7==1)&&((!(a21==1)&&((a12==8)&&(input==3)))&&(a8==13)))&&(a17==1)))&&(a20==1))){
103 a20 = 0;
104 a8 = 15;
105 a17 = 0;
106 a21 = 1;
107 return -1;
108 } else if(((a17==1)&&(((a8==15)&&(((a12==8)&&((!(a7==1)&&(input==5))&&(a21==1)))&&!(a20==1)))&&(a16==5)))){
109 a20 = 1;
110 a8 = 13;
111 a7 = 1;
112 a16 = 4;
113 return -1;
114 } else if((!(a7==1)&&(((((a21==1)&&(((a8==15)&&(input==5))&&!(a17==1)))&&(a12==8))&&(a20==1))&&(a16==4)))){
115 a8 = 13;
116 a17 = 1;
117 a7 = 1;
118 return -1;
119 } else if(((!(a21==1)&&(((a12==8)&&((((a16==6)&&((a20==1)&&!(a17==1)))||((!(a20==1)&&(a17==1))&&(a16==4)))&&(input==1)))&&(a8==13)))&&(a7==1))){
120 a16 = 6;
121 a20 = 1;
122 a17 = 0;
123 return -1;
124 } else if(((a17==1)&&(!(a7==1)&&(((a21==1)&&(((a12==8)&&((input==5)&&((a16==5)||(a16==6))))&&(a20==1)))&&(a8==15))))){
125 a7 = 1;
126 a16 = 4;
127 a8 = 13;
128 return -1;
129 } else if((((a12==8)&&(!(a21==1)&&((a7==1)&&((a8==13)&&((input==6)&&((((a16==6)&&(a17==1))||((a16==4)&&!(a17==1)))||((a16==5)&&!(a17==1))))))))&&(a20==1))){
130 a8 = 15;
131 a17 = 0;
132 a21 = 1;
133 a20 = 0;
134 a16 = 4;
135 return -1;
136 } else if((((a16==5)&&((((a8==15)&&((!(a7==1)&&(input==2))&&(a21==1)))&&(a12==8))&&!(a20==1)))&&!(a17==1))){
137 a16 = 4;
138 a17 = 1;
139 return 24;
140 } else if((!(a20==1)&&((a21==1)&&((a16==4)&&((a8==15)&&(((a12==8)&&((input==2)&&!(a7==1)))&&!(a17==1))))))){
141 a17 = 1;
142 a16 = 5;
143 return 21;
144 } else if((((a21==1)&&(!(a7==1)&&((!(a20==1)&&(!(a17==1)&&((a12==8)&&(input==6))))&&(a16==4))))&&(a8==15))){
145 a20 = 1;
146 a16 = 6;
147 return 22;
148 } else if(((a17==1)&&((((((a12==8)&&((input==4)&&(a8==13)))&&(a20==1))&&!(a21==1))&&(a16==5))&&(a7==1)))){
149 a16 = 4;
150 a17 = 0;
151 return 25;
152 } else if(((((a8==13)&&((a12==8)&&((((((a16==6)&&(a17==1))||(!(a17==1)&&(a16==4)))||(!(a17==1)&&(a16==5)))&&(input==1))&&!(a21==1))))&&(a20==1))&&(a7==1))){
153 a8 = 15;
154 a16 = 6;
155 a21 = 1;
156 a20 = 0;
157 a7 = 0;
158 a17 = 1;
159 return -1;
160 } else if(((a8==13)&&(!(a21==1)&&((((((!(a17==1)&&(a20==1))&&(a16==6))||((a16==4)&&((a17==1)&&!(a20==1))))&&(input==5))&&(a7==1))&&(a12==8))))){
161 a17 = 1;
162 a20 = 0;
163 a16 = 4;
164 return 25;
165 } else if(((!(a21==1)&&((((((a16==6)&&((a20==1)&&!(a17==1)))||(((a17==1)&&!(a20==1))&&(a16==4)))&&(input==4))&&(a7==1))&&(a12==8)))&&(a8==13))){
166 a8 = 15;
167 a21 = 1;
168 a20 = 0;
169 a7 = 0;
170 a16 = 6;
171 a17 = 0;
172 return 26;
173 } else if((((a21==1)&&(!(a7==1)&&((((((a16==5)&&((a20==1)&&!(a17==1)))||((!(a17==1)&&(a20==1))&&(a16==6)))||((a16==4)&&((a17==1)&&!(a20==1))))&&(input==4))&&(a12==8))))&&(a8==15))){
174 a16 = 4;
175 a20 = 0;
176 a17 = 0;
177 return 24;
178 } else if(((((((a16==6)&&((!(a20==1)&&(!(a17==1)&&!(a7==1)))&&(a8==15)))&&(a21==1))||(((a16==4)&&((((a7==1)&&(a17==1))&&(a20==1))&&(a8==13)))&&!(a21==1)))&&(input==4))&&(a12==8))){
179 a17 = 0;
180 a16 = 5;
181 a21 = 1;
182 a8 = 14;
183 a7 = 1;
184 a20 = 1;
185 return -1;
186 } else if((!(a17==1)&&(((a12==8)&&(!(a20==1)&&(((a8==15)&&((a21==1)&&(input==4)))&&!(a7==1))))&&(a16==5)))){
187 a17 = 1;
188 return 24;
189 } else if((((!(a7==1)&&(((input==2)&&((((a16==5)&&((a20==1)&&!(a17==1)))||((a16==6)&&((a20==1)&&!(a17==1))))||((a16==4)&&(!(a20==1)&&(a17==1)))))&&(a8==15)))&&(a12==8))&&(a21==1))){
190 a17 = 0;
191 a16 = 5;
192 a20 = 1;
193 return 25;
194 } else if((!(a20==1)&&(((((((input==6)&&(a16==5))&&(a21==1))&&!(a17==1))&&(a12==8))&&!(a7==1))&&(a8==15)))){
195 a17 = 1;
196 return 24;
197 } else if(((a12==8)&&(((((((a21==1)&&(input==5))&&(a8==15))&&(a17==1))&&!(a7==1))&&!(a20==1))&&(a16==6)))){
198 a20 = 1;
199 a16 = 4;
200 a7 = 1;
201 a8 = 13;
202 return -1;
203 } else if(((((a8==15)&&(!(a7==1)&&((((!(a20==1)&&(a17==1))&&(a16==4))||(((!(a17==1)&&(a20==1))&&(a16==5))||((a16==6)&&((a20==1)&&!(a17==1)))))&&(input==6))))&&(a12==8))&&(a21==1))){
204 a20 = 0;
205 a17 = 1;
206 a16 = 4;
207 return 22;
208 } else if(((a8==15)&&((a16==4)&&(!(a20==1)&&((((a21==1)&&(!(a17==1)&&(input==5)))&&!(a7==1))&&(a12==8)))))){
209 a7 = 1;
210 a8 = 13;
211 a17 = 1;
212 a20 = 1;
213 return -1;
214 } else if(((a17==1)&&((a12==8)&&((a8==15)&&(((!(a7==1)&&(((a16==5)||(a16==6))&&(input==2)))&&(a21==1))&&(a20==1)))))){
215 a17 = 0;
216 a16 = 6;
217 return 22;
218 } else if((!(a7==1)&&(((a8==15)&&((!(a17==1)&&((a12==8)&&((input==3)&&(a21==1))))&&(a16==4)))&&(a20==1)))){
219 a17 = 1;
220 a7 = 1;
221 a8 = 13;
222 return -1;
223 } else if(((a16==5)&&((!(a21==1)&&(((a8==13)&&(((input==2)&&(a20==1))&&(a12==8)))&&(a7==1)))&&(a17==1)))){
224 a21 = 1;
225 a8 = 14;
226 a16 = 4;
227 a20 = 0;
228 a7 = 0;
229 a17 = 0;
230 return -1;
231 } else if(((a20==1)&&(((a12==8)&&((a7==1)&&((a8==13)&&(((!(a17==1)&&(a16==5))||(((a17==1)&&(a16==6))||(!(a17==1)&&(a16==4))))&&(input==3)))))&&!(a21==1)))){
232 a8 = 14;
233 a7 = 0;
234 a17 = 1;
235 a21 = 1;
236 a16 = 4;
237 return -1;
238 } else if(((a12==8)&&((a7==1)&&(!(a21==1)&&((a8==13)&&((input==6)&&(((a16==6)&&((a20==1)&&!(a17==1)))||((a16==4)&&((a17==1)&&!(a20==1)))))))))){
239 a20 = 0;
240 a21 = 1;
241 a17 = 0;
242 a8 = 14;
243 a16 = 4;
244 return -1;
245 } else if(((!(a7==1)&&(!(a17==1)&&((((a16==4)&&((a8==15)&&(input==1)))&&(a12==8))&&(a21==1))))&&(a20==1))){
246 a7 = 1;
247 a8 = 13;
248 a17 = 1;
249 return -1;
250 } else if(((a17==1)&&(((a21==1)&&(!(a20==1)&&((a12==8)&&((a8==15)&&(!(a7==1)&&(input==1))))))&&(a16==6)))){
251 a20 = 1;
252 a8 = 13;
253 a7 = 1;
254 a16 = 4;
255 return -1;
256 } else if(((a20==1)&&((a12==8)&&((((a17==1)&&((((a16==5)||(a16==6))&&(input==4))&&(a8==15)))&&(a21==1))&&!(a7==1))))){
257 a16 = 4;
258 a7 = 1;
259 a8 = 13;
260 return -1;
261 } else if(((((a8==13)&&((((!(a21==1)&&(input==6))&&(a20==1))&&(a12==8))&&(a17==1)))&&(a7==1))&&(a16==5))){
262 a16 = 4;
263 a20 = 0;
264 return 25;
265 } else if(((a16==5)&&(((((a12==8)&&(!(a7==1)&&((input==2)&&!(a20==1))))&&(a21==1))&&(a17==1))&&(a8==15)))){
266 a17 = 0;
267 return 24;
268 } else if((((a12==8)&&(((!(a17==1)&&((a21==1)&&((input==4)&&!(a7==1))))&&(a8==15))&&(a20==1)))&&(a16==4))){
269 a20 = 0;
270 a17 = 1;
271 a16 = 6;
272 return 21;
273 } else if(((a7==1)&&((a8==13)&&((a12==8)&&(!(a21==1)&&((input==2)&&((((a20==1)&&!(a17==1))&&(a16==6))||(((a17==1)&&!(a20==1))&&(a16==4))))))))){
274 a16 = 4;
275 a20 = 0;
276 a17 = 1;
277 return -1;
278 } else if((((((((!(a20==1)&&(!(a17==1)&&!(a7==1)))&&(a8==15))&&(a16==6))&&(a21==1))||((((a8==13)&&(((a17==1)&&(a7==1))&&(a20==1)))&&(a16==4))&&!(a21==1)))&&(input==6))&&(a12==8))){
279 a20 = 1;
280 a8 = 13;
281 a16 = 4;
282 a7 = 0;
283 a21 = 1;
284 a17 = 0;
285 return -1;
286 } else if(((!(a7==1)&&(!(a17==1)&&(((((input==3)&&(a21==1))&&(a16==4))&&(a8==15))&&(a12==8))))&&!(a20==1))){
287 a17 = 1;
288 a7 = 1;
289 a8 = 13;
290 a20 = 1;
291 return -1;
292 } else if((((((a12==8)&&(((((a17==1)&&!(a20==1))&&(a16==4))||((((a20==1)&&!(a17==1))&&(a16==5))||((!(a17==1)&&(a20==1))&&(a16==6))))&&(input==3)))&&(a8==15))&&(a21==1))&&!(a7==1))){
293 a16 = 4;
294 a17 = 1;
295 a8 = 13;
296 a20 = 1;
297 a7 = 1;
298 return -1;
299 } else if((((!(a7==1)&&(((input==5)&&((((a16==5)&&(!(a17==1)&&(a20==1)))||((a16==6)&&((a20==1)&&!(a17==1))))||((a16==4)&&(!(a20==1)&&(a17==1)))))&&(a12==8)))&&(a21==1))&&(a8==15))){
300 a16 = 4;
301 a17 = 1;
302 a7 = 1;
303 a20 = 1;
304 a8 = 13;
305 return -1;
306 } else if(((!(a7==1)&&(((a21==1)&&(((a17==1)&&((a12==8)&&(input==2)))&&!(a20==1)))&&(a16==6)))&&(a8==15))){
307 a8 = 13;
308 a20 = 1;
309 a16 = 4;
310 a7 = 1;
311 return -1;
312 } else if(((!(a17==1)&&((a21==1)&&((!(a20==1)&&((a12==8)&&((input==3)&&!(a7==1))))&&(a8==15))))&&(a16==5))){
313 a8 = 13;
314 a16 = 4;
315 return -1;
316 } else if((((a16==5)&&(!(a20==1)&&(((((input==6)&&(a21==1))&&(a17==1))&&!(a7==1))&&(a12==8))))&&(a8==15))){
317 return 24;
318 } else if((!(a7==1)&&((a17==1)&&(((a16==6)&&(!(a20==1)&&(((input==6)&&(a12==8))&&(a21==1))))&&(a8==15))))){
319 a7 = 1;
320 a8 = 13;
321 a20 = 1;
322 a16 = 4;
323 return -1;
324 } else if(((((a21==1)&&((a8==15)&&((a12==8)&&(!(a7==1)&&(!(a17==1)&&(input==2))))))&&(a16==4))&&(a20==1))){
325 a17 = 1;
326 a8 = 13;
327 a7 = 1;
328 return -1;
329 } else if(((a8==15)&&(((a16==4)&&((a12==8)&&((!(a20==1)&&(!(a7==1)&&(input==1)))&&!(a17==1))))&&(a21==1)))){
330 a16 = 6;
331 a20 = 1;
332 return 22;
333 } else if(((a21==1)&&(((a12==8)&&((((a17==1)&&((input==3)&&((a16==5)||(a16==6))))&&!(a7==1))&&(a20==1)))&&(a8==15)))){
334 a17 = 0;
335 a16 = 4;
336 return 21;
337 } else if((!(a21==1)&&((a20==1)&&(((a12==8)&&((a8==13)&&((((a16==5)&&!(a17==1))||(((a17==1)&&(a16==6))||(!(a17==1)&&(a16==4))))&&(input==2))))&&(a7==1))))){
338 a21 = 1;
339 a8 = 15;
340 a17 = 1;
341 a7 = 0;
342 a16 = 6;
343 a20 = 0;
344 return -1;
345 } else if(((a7==1)&&((a12==8)&&((((a20==1)&&(((!(a17==1)&&(a16==5))||(((a17==1)&&(a16==6))||((a16==4)&&!(a17==1))))&&(input==4)))&&(a8==13))&&!(a21==1))))){
346 a8 = 15;
347 a16 = 6;
348 a21 = 1;
349 a7 = 0;
350 a20 = 0;
351 a17 = 0;
352 return 26;
353 } else if(((a21==1)&&((((!(a7==1)&&((a8==15)&&(!(a20==1)&&(input==4))))&&(a17==1))&&(a16==5))&&(a12==8)))){
354 return 24;
355 } else if((((!(a7==1)&&((!(a20==1)&&((a21==1)&&((input==3)&&(a17==1))))&&(a8==15)))&&(a12==8))&&(a16==5))){
356 a20 = 1;
357 a8 = 13;
358 a7 = 1;
359 a16 = 4;
360 return -1;
361 } else if(((((!(a17==1)&&(!(a20==1)&&((a8==15)&&((input==1)&&(a16==5)))))&&(a12==8))&&(a21==1))&&!(a7==1))){
362 return -1;
363 } else if(((((a21==1)&&((a8==15)&&(((a16==5)&&((a12==8)&&(input==1)))&&(a17==1))))&&!(a7==1))&&!(a20==1))){
364 return 21;
365 } else if(((!(a21==1)&&((a20==1)&&((((a8==13)&&((a7==1)&&(input==5)))&&(a17==1))&&(a12==8))))&&(a16==5))){
366 a21 = 1;
367 a7 = 0;
368 a17 = 0;
369 a8 = 14;
370 a20 = 0;
371 return -1;
372 } else if((((!(a7==1)&&((a21==1)&&((((input==6)&&(a20==1))&&(a8==15))&&!(a17==1))))&&(a12==8))&&(a16==4))){
373 a7 = 1;
374 a8 = 13;
375 a17 = 1;
376 return -1;
377 } else if(((((a20==1)&&(((!(a21==1)&&((a7==1)&&(input==1)))&&(a8==13))&&(a17==1)))&&(a12==8))&&(a16==5))){
378 a21 = 1;
379 a16 = 6;
380 a7 = 0;
381 return -1;
382 } else if(((a12==8)&&((input==5)&&((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==15))&&(a16==6))&&(a21==1))||(!(a21==1)&&((a16==4)&&(((a20==1)&&((a7==1)&&(a17==1)))&&(a8==13)))))))){
383 a20 = 0;
384 a21 = 1;
385 a8 = 14;
386 a17 = 0;
387 a16 = 5;
388 a7 = 1;
389 return -1;
390 }
391 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){
392 error_20: exit(0);
393 }
394 if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){
395 error_47: exit(0);
396 }
397 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){
398 error_32: exit(0);
399 }
400 if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){
401 error_37: exit(0);
402 }
403 if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){
404 error_56: exit(0);
405 }
406 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==5))&&(a21==1))){
407 error_33: exit(0);
408 }
409 if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){
410 error_57: exit(0);
411 }
412 if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){
413 error_50: exit(0);
414 }
415 if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){
416 error_35: exit(0);
417 }
418 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){
419 error_15: __VERIFIER_error();
420 }
421 if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){
422 error_38: exit(0);
423 }
424 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){
425 error_21: exit(0);
426 }
427 if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){
428 error_44: exit(0);
429 }
430 if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){
431 error_41: exit(0);
432 }
433 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){
434 error_19: exit(0);
435 }
436 if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){
437 error_40: exit(0);
438 }
439 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==5))&&(a21==1))){
440 error_27: exit(0);
441 }
442 if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){
443 error_59: exit(0);
444 }
445 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){
446 error_2: exit(0);
447 }
448 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){
449 error_1: exit(0);
450 }
451 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==6))&&(a21==1))){
452 error_31: exit(0);
453 }
454 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==6))&&(a21==1))){
455 error_28: exit(0);
456 }
457 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){
458 error_5: exit(0);
459 }
460 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){
461 error_23: exit(0);
462 }
463 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){
464 error_4: exit(0);
465 }
466 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){
467 globalError: exit(0);
468 }
469 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==5))&&(a21==1))){
470 error_24: exit(0);
471 }
472 if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){
473 error_58: exit(0);
474 }
475 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){
476 error_18: exit(0);
477 }
478 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){
479 error_29: exit(0);
480 }
481 if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){
482 error_36: exit(0);
483 }
484 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==4))&&(a21==1))){
485 error_26: exit(0);
486 }
487 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){
488 error_7: exit(0);
489 }
490 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==6))&&(a21==1))){
491 error_34: exit(0);
492 }
493 if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){
494 error_51: exit(0);
495 }
496 if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){
497 error_49: exit(0);
498 }
499 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){
500 error_0: exit(0);
501 }
502 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){
503 error_11: exit(0);
504 }
505 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){
506 error_10: exit(0);
507 }
508 if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){
509 error_55: exit(0);
510 }
511 if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){
512 error_46: exit(0);
513 }
514 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==4))&&(a21==1))){
515 error_8: exit(0);
516 }
517 if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){
518 error_53: exit(0);
519 }
520 if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){
521 error_42: exit(0);
522 }
523 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){
524 error_17: exit(0);
525 }
526 if(((((((!(a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){
527 error_45: exit(0);
528 }
529 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){
530 error_9: exit(0);
531 }
532 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==15))&&(a12==8))&&(a16==6))&&(a21==1))){
533 error_25: exit(0);
534 }
535 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){
536 error_12: exit(0);
537 }
538 if((((((((a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){
539 error_48: exit(0);
540 }
541 if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==5))&&(a21==1))){
542 error_54: exit(0);
543 }
544 if((((((((a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){
545 error_13: exit(0);
546 }
547 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){
548 error_6: exit(0);
549 }
550 if((((((((a17==1)&&(a7==1))&&!(a20==1))&&(a8==15))&&(a12==8))&&(a16==5))&&(a21==1))){
551 error_30: exit(0);
552 }
553 if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){
554 error_52: exit(0);
555 }
556 if(((((((!(a17==1)&&(a7==1))&&!(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){
557 error_22: exit(0);
558 }
559 if((((((((a17==1)&&!(a7==1))&&!(a20==1))&&(a8==13))&&(a12==8))&&(a16==6))&&(a21==1))){
560 error_43: exit(0);
561 }
562 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){
563 error_3: exit(0);
564 }
565 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==6))&&(a21==1))){
566 error_16: exit(0);
567 }
568 if(((((((!(a17==1)&&(a7==1))&&(a20==1))&&(a8==14))&&(a12==8))&&(a16==4))&&(a21==1))){
569 error_14: exit(0);
570 }
571 if(((((((!(a17==1)&&!(a7==1))&&(a20==1))&&(a8==13))&&(a12==8))&&(a16==5))&&(a21==1))){
572 error_39: exit(0);
573 }
574 return -2;
575 }
576
577int main()
578{
579 // default output
580 int output = -1;
581
582 // main i/o-loop
583 while(1)
584 {
585 // read input
586 int input;
587 input = __VERIFIER_nondet_int();
588 if ((input != 1) && (input != 2) && (input != 3) && (input != 4) && (input != 5) && (input != 6)) return -2;
589
590 // operate eca engine
591 output = calculate_output(input);
592
593 }
594}
Note: See TracBrowser for help on using the repository browser.