aag 992 60 56 1 876
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 2
124 4
126 6
128 8
130 10
132 12
134 14
136 16
138 18
140 20
142 22
144 24
146 26
148 28
150 30
152 32
154 34
156 36
158 38
160 40
162 42
164 44
166 46
168 48
170 50
172 52
174 54
176 56
178 58
180 60
182 62
184 64
186 66
188 68
190 70
192 72
194 74
196 76
198 78
200 80
202 82
204 84
206 86
208 88
2

... [truncated 12.5 kB]

15]
l32 nextv_x2[0]
l33 nextv_x2[1]
l34 nextv_x2[2]
l35 nextv_x2[3]
l36 nextv_x2[4]
l37 nextv_x2[5]
l38 nextv_x2[6]
l39 nextv_x2[7]
l40 nextv_x2[8]
l41 nextv_x2[9]
l42 nextv_x2[10]
l43 nextv_x2[11]
l44 nextv_x2[12]
l45 nextv_x2[13]
l46 nextv_x2[14]
l47 nextv_x2[15]
l48 nexta_Q_a1
l49 nexta_R_a1
l50 nexta_S_a1
l51 nexta_Q_a2
l52 nexta_R_a2
l53 nexta_S_a2
l54 dve_initialized
l55 dve_valid
c
#!SYNTCOMP
STATUS : realizable
SOLVED_BY : 3/3 [2016-pre-classification]
SOLVED_IN : 0.164 [2016-pre-classification]
#.