aag 2394 49 43 1 2302
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 773
102 869
104 969
106 1065
108 1165
110 1261
112 1361
114 1457
116 1557
118 1653
120 1753
122 1849
124 1949
126 2045
128 2145
130 2241
132 2341
134 2437
136 2537
138 2633
140 2733
142 2829
144 2929
146 3025
148 3125
150 3221
152 3321
154 3417
156 3517
158 3613
160 3713
162 3809
164 3909
166 4005
168 4105
170 4201
172 4301
174 4397
176 4497

... [truncated 31.0 kB]

a[4][6]<0>
l35 a[5][0]<0>
l36 a[5][1]<0>
l37 a[5][2]<0>
l38 a[5][3]<0>
l39 a[5][4]<0>
l40 a[5][5]<0>
l41 a[5][6]<0>
l42 init_latch<0>
o0 err<0>
c
#!SYNTCOMP
SOLVED_BY : 2/11 [SYNTCOMP2016-RealSeq], 3/6 [SYNTCOMP2016-RealPar], 2/10 [SYNTCOMP2017-RealSeq], 3/6 [SYNTCOMP2017-RealPar], 0/6 [SYNTCOMP2017-SyntSeq], 1/4 [SYNTCOMP2017-SyntPar]
SOLVED_IN : 1.092 [SYNTCOMP2016-RealSeq], 1.31228 [SYNTCOMP2016-RealPar], 1.112 [SYNTCOMP2017-RealSeq], 1.30351 [SYNTCOMP2017-RealPar]
STATUS : realizable
REF_SIZE : 2330
#.