3 context: '[N] -> { : N <= 2147483647 and N >= -2147483648 }'
6 extent: '[N] -> { __pet_test_0[t] : t >= 0 }'
7 value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
12 extent: '[N] -> { __pet_test_1[t] : N = 0 and t >= 1; __pet_test_1[0] }'
13 value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
18 extent: '[N] -> { __pet_test_2[t] : t >= 0 }'
19 value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
24 extent: '[N] -> { __pet_test_3[t] : t >= 0 }'
25 value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
30 extent: '[N] -> { a[] }'
35 domain: '[N] -> { S_0[t] : N = 0 and t >= 1; S_0[0] }'
36 schedule: '[N] -> { S_0[t] -> [0, t, 0] }'
42 relation: '[N] -> { S_0[t] -> a[] }'
43 index: '[N] -> { S_0[t] -> a[] }'
44 reference: __pet_ref_0
48 relation: '[N] -> { S_0[t] -> [5] }'
49 index: '[N] -> { S_0[t] -> [(5)] }'
50 reference: __pet_ref_1
54 domain: '[N] -> { S_1[t] : N = 0 and t >= 1; S_1[0] : N = 0 }'
55 schedule: '[N] -> { S_1[t] -> [0, t, 2] }'
61 relation: '[N] -> { S_1[t] -> a[] }'
62 index: '[N] -> { S_1[t] -> a[] }'
63 reference: __pet_ref_2
67 relation: '[N] -> { S_1[t] -> [6] }'
68 index: '[N] -> { S_1[t] -> [(6)] }'
69 reference: __pet_ref_3
73 domain: '[N] -> { [S_2[t] -> [0]] : t >= 0 }'
74 schedule: '{ S_2[t] -> [1, t, 0] }'
80 relation: '[N] -> { S_2[t] -> a[] }'
81 index: '[N] -> { S_2[t] -> a[] }'
82 reference: __pet_ref_5
86 relation: '[N] -> { S_2[t] -> [5] }'
87 index: '[N] -> { S_2[t] -> [(5)] }'
88 reference: __pet_ref_6
93 relation: '[N] -> { S_2[t] -> __pet_test_0[-1 + t] : t >= 1 }'
94 index: '[N] -> { S_2[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
95 reference: __pet_ref_4
99 domain: '[N] -> { [S_3[t] -> [0]] : t >= 0 }'
100 schedule: '{ S_3[t] -> [1, t, 1, 0] }'
106 relation: '[N] -> { S_3[t] -> __pet_test_0[t] }'
107 index: '[N] -> { S_3[t] -> __pet_test_0[(t)] }'
108 reference: __pet_ref_8
115 relation: '[N] -> { S_3[t] -> __pet_test_0[-1 + t] : t >= 1 }'
116 index: '[N] -> { S_3[t] -> __pet_test_0[((-1 + t) : t >= 1)] }'
117 reference: __pet_ref_7
121 domain: '[N] -> { [S_4[t] -> [0]] : t >= 0 }'
122 schedule: '{ S_4[t] -> [1, t, 2] }'
128 relation: '[N] -> { S_4[t] -> a[] }'
129 index: '[N] -> { S_4[t] -> a[] }'
130 reference: __pet_ref_10
134 relation: '[N] -> { S_4[t] -> [6] }'
135 index: '[N] -> { S_4[t] -> [(6)] }'
136 reference: __pet_ref_11
141 relation: '[N] -> { S_4[t] -> __pet_test_0[t] }'
142 index: '[N] -> { S_4[t] -> __pet_test_0[(t)] }'
143 reference: __pet_ref_9
147 domain: '[N] -> { [S_5[t] -> [1]] : N = 0 and t >= 1; [S_5[0] -> [1]] }'
148 schedule: '[N] -> { S_5[t] -> [2, t, 0] }'
154 relation: '[N] -> { S_5[t] -> __pet_test_1[t] }'
155 index: '[N] -> { S_5[t] -> __pet_test_1[(t)] }'
156 reference: __pet_ref_13
163 relation: '[N] -> { S_5[t] -> __pet_test_1[-1 + t] : N = 0 and t >= 2; S_5[1]
164 -> __pet_test_1[0] }'
165 index: '[N] -> { S_5[t] -> __pet_test_1[((-1 + t) : t = 1 or (N = 0 and t >= 2))]
167 reference: __pet_ref_12
171 domain: '[N] -> { [S_6[t] -> [1]] : N = 0 and t >= 1; [S_6[0] -> [1]] }'
172 schedule: '[N] -> { S_6[t] -> [2, t, 1, 0] }'
178 relation: '[N] -> { S_6[t] -> a[] }'
179 index: '[N] -> { S_6[t] -> a[] }'
180 reference: __pet_ref_15
184 relation: '[N] -> { S_6[t] -> [5] }'
185 index: '[N] -> { S_6[t] -> [(5)] }'
186 reference: __pet_ref_16
191 relation: '[N] -> { S_6[t] -> __pet_test_1[t] }'
192 index: '[N] -> { S_6[t] -> __pet_test_1[(t)] }'
193 reference: __pet_ref_14
197 domain: '[N] -> { [S_7[t] -> [1]] : N = 0 and t >= 1; [S_7[0] -> [1]] : N = 0 }'
198 schedule: '[N] -> { S_7[t] -> [2, t, 1, 2] }'
204 relation: '[N] -> { S_7[t] -> a[] }'
205 index: '[N] -> { S_7[t] -> a[] }'
206 reference: __pet_ref_18
210 relation: '[N] -> { S_7[t] -> [6] }'
211 index: '[N] -> { S_7[t] -> [(6)] }'
212 reference: __pet_ref_19
217 relation: '[N] -> { S_7[t] -> __pet_test_1[t] }'
218 index: '[N] -> { S_7[t] -> __pet_test_1[(t)] }'
219 reference: __pet_ref_17
223 domain: '[N] -> { [S_8[t] -> [1, 0]] : t >= 0 }'
224 schedule: '{ S_8[t] -> [3, t, 0] }'
230 relation: '[N] -> { S_8[t] -> __pet_test_2[t] }'
231 index: '[N] -> { S_8[t] -> __pet_test_2[(t)] }'
232 reference: __pet_ref_22
239 relation: '[N] -> { S_8[t] -> __pet_test_2[-1 + t] : t >= 1 }'
240 index: '[N] -> { S_8[t] -> __pet_test_2[((-1 + t) : t >= 1)] }'
241 reference: __pet_ref_20
245 relation: '[N] -> { S_8[t] -> __pet_test_3[-1 + t] : t >= 1 }'
246 index: '[N] -> { S_8[t] -> __pet_test_3[((-1 + t) : t >= 1)] }'
247 reference: __pet_ref_21
251 domain: '[N] -> { [S_9[t] -> [1, 0]] : t >= 0 }'
252 schedule: '{ S_9[t] -> [3, t, 1, 0] }'
258 relation: '[N] -> { S_9[t] -> a[] }'
259 index: '[N] -> { S_9[t] -> a[] }'
260 reference: __pet_ref_25
264 relation: '[N] -> { S_9[t] -> [5] }'
265 index: '[N] -> { S_9[t] -> [(5)] }'
266 reference: __pet_ref_26
271 relation: '[N] -> { S_9[t] -> __pet_test_2[t] }'
272 index: '[N] -> { S_9[t] -> __pet_test_2[(t)] }'
273 reference: __pet_ref_23
277 relation: '[N] -> { S_9[t] -> __pet_test_3[-1 + t] : t >= 1 }'
278 index: '[N] -> { S_9[t] -> __pet_test_3[((-1 + t) : t >= 1)] }'
279 reference: __pet_ref_24
283 domain: '[N] -> { [S_10[t] -> [1, 0]] : t >= 0 }'
284 schedule: '{ S_10[t] -> [3, t, 1, 1, 0] }'
290 relation: '[N] -> { S_10[t] -> __pet_test_3[t] }'
291 index: '[N] -> { S_10[t] -> __pet_test_3[(t)] }'
292 reference: __pet_ref_29
299 relation: '[N] -> { S_10[t] -> __pet_test_2[t] }'
300 index: '[N] -> { S_10[t] -> __pet_test_2[(t)] }'
301 reference: __pet_ref_27
305 relation: '[N] -> { S_10[t] -> __pet_test_3[-1 + t] : t >= 1 }'
306 index: '[N] -> { S_10[t] -> __pet_test_3[((-1 + t) : t >= 1)] }'
307 reference: __pet_ref_28
311 domain: '[N] -> { [S_11[t] -> [1, 0]] : t >= 0 }'
312 schedule: '{ S_11[t] -> [3, t, 1, 2] }'
318 relation: '[N] -> { S_11[t] -> a[] }'
319 index: '[N] -> { S_11[t] -> a[] }'
320 reference: __pet_ref_32
324 relation: '[N] -> { S_11[t] -> [6] }'
325 index: '[N] -> { S_11[t] -> [(6)] }'
326 reference: __pet_ref_33
331 relation: '[N] -> { S_11[t] -> __pet_test_2[t] }'
332 index: '[N] -> { S_11[t] -> __pet_test_2[(t)] }'
333 reference: __pet_ref_30
337 relation: '[N] -> { S_11[t] -> __pet_test_3[t] }'
338 index: '[N] -> { S_11[t] -> __pet_test_3[(t)] }'
339 reference: __pet_ref_31
344 extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }'
346 extension: '[N] -> { __pet_test_1[t] -> __pet_test_1[t''] : N = 0 and t'' <= t and
347 t'' >= 1; __pet_test_1[t] -> __pet_test_1[0] : t >= 0 }'
349 extension: '{ __pet_test_3[t] -> __pet_test_3[t''] : t'' <= t and t'' >= 0 }'
351 extension: '{ __pet_test_2[t] -> __pet_test_2[t''] : t'' <= t and t'' >= 0 }'