aag 3528 96 93 1 3339
2
4
6
8
10
12
14
16
18
20
22
24
26
28
30
32
34
36
38
40
42
44
46
48
50
52
54
56
58
60
62
64
66
68
70
72
74
76
78
80
82
84
86
88
90
92
94
96
98
100
102
104
106
108
110
112
114
116
118
120
122
124
126
128
130
132
134
136
138
140
142
144
146
148
150
152
154
156
158
160
162
164
166
168
170
172
174
176
178
180
182
184
186
188
190
192
194 2
196 4
198 6
200 8
202 10
204 12
206 14
208 16
210 18
212 20
214 22
216 24
218 26
220 28
222 30
224 32
226 34
228 36
230 38
232 40
234 42
236 44
238 46
24

... [truncated 50.2 kB]

]
l68 nextv_a_8[4]
l69 nextv_a_8[5]
l70 nextv_a_8[6]
l71 nextv_a_8[7]
l72 nextv_x[0]
l73 nextv_x[1]
l74 nextv_x[2]
l75 nextv_x[3]
l76 nextv_x[4]
l77 nextv_x[5]
l78 nextv_x[6]
l79 nextv_x[7]
l80 nextv_y[0]
l81 nextv_y[1]
l82 nextv_y[2]
l83 nextv_y[3]
l84 nextv_y[4]
l85 nextv_y[5]
l86 nextv_y[6]
l87 nextv_y[7]
l88 nexta_q
l89 nexta_not_done
l90 nexta_done
l91 dve_initialized
l92 dve_valid
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2016-pre-classification]
SOLVED_IN : 1.288 [2016-pre-classification]
#.