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 blastFlag ;
11 int tmp___1;
12
13 s__state = 8466;
14 blastFlag = 0;
15
16 while (1) {
17 if (s__state <= 8512 && blastFlag > 2) { goto ERROR; }
18 {
19 {
20 {
21 {
22 {
23 if (s__state == 8466) {
24 goto switch_1_8466;
25 } else {
26 {
27 {
28 if (s__state == 8512) {
29 goto switch_1_8512;
30 } else {
31 {
32 {
33 {
34 {
35 {
36 {
37 {
38 {
39 {
40 {
41 {
42 {
43 {
44 if (s__state == 8640) {
45 goto switch_1_8640;
46 } else {
47 {
48 if (s__state == 8656) {
49 goto switch_1_8656;
50 } else {
51 {
52 {
53 goto end;
54
55 switch_1_8466:
56 if (blastFlag == 0) {
57 blastFlag = 2;
58 }
59 if (s__hit) {
60 s__state = 8656;
61 } else {
62 s__state = 8512;
63 }
64 goto switch_1_break;
65
66 switch_1_8512:
67 tmp___1 = __VERIFIER_nondet_int();
68 if (tmp___1) {
69 s__state = 8466;
70 } else {
71 s__state = 8640;
72 }
73 goto switch_1_break;
74
75 switch_1_8640:
76 if (blastFlag == 3) {
77 blastFlag = 4;
78 }
79 if (s__hit) {
80 goto end;
81 } else {
82 s__state = 8656;
83 }
84 goto switch_1_break;
85
86 switch_1_8656:
87 if (blastFlag == 2) {
88 blastFlag = 3;
89 }
90
91 if (blastFlag == 4) {
92 blastFlag = 5;
93 } else {
94 if (blastFlag == 5) {
95 goto ERROR;
96 }
97 }
98 if (s__hit) {
99 s__state = 8640;
100 } else {
101 goto end;
102 }
103 goto switch_1_break;
104
105 }
106 }
107 }
108 }
109 }
110 }
111 }
112 }
113 }
114 }
115 }
116 }
117 }
118 }
119 }
120 }
121 }
122 }
123 }
124 }
125 }
126 }
127 }
128 }
129 }
130 }
131 }
132 switch_1_break: ;
133 }
134
135 end:
136 return (-1);
137 ERROR:
138 return (-1);
139}