6 extent: '{ __pet_test_0[k] : k >= 252 and k <= 261 }'
7 value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }'
17 domain: '{ [S_0[k] -> [0]] : (exists (e0 = floor((k)/256): 256e0 = k and k >= 252
18 and k <= 261)) or (exists (e0 = floor((257 - k)/256): k >= 252 and k <= 261 and
19 256e0 >= 2 - k and 256e0 <= 255 - k)) }'
20 schedule: '{ S_0[k] -> [0, k, 0] }'
26 relation: '{ S_0[k] -> a[] }'
27 index: '{ S_0[k] -> a[] }'
28 reference: __pet_ref_1
35 relation: '{ S_0[k] -> __pet_test_0[-1 + k] : k >= 253 }'
36 index: '{ S_0[k] -> __pet_test_0[((-1 + k) : k >= 253)] }'
37 reference: __pet_ref_0
41 domain: '{ [S_1[k] -> [0]] : k >= 252 and k <= 261 }'
42 schedule: '{ S_1[k] -> [0, k, 1, 0] }'
48 relation: '{ S_1[k] -> __pet_test_0[k] }'
49 index: '{ S_1[k] -> __pet_test_0[(k)] }'
50 reference: __pet_ref_3
57 relation: '{ S_1[k] -> __pet_test_0[-1 + k] : k >= 253 }'
58 index: '{ S_1[k] -> __pet_test_0[((-1 + k) : k >= 253)] }'
59 reference: __pet_ref_2
63 domain: '{ [S_2[k] -> [0]] : k >= 252 and k <= 261 }'
64 schedule: '{ S_2[k] -> [0, k, 2] }'
70 relation: '{ S_2[k] -> a[] }'
71 index: '{ S_2[k] -> a[] }'
72 reference: __pet_ref_5
76 relation: '{ S_2[k] -> [o0] : exists (e0 = floor((-k + o0)/256): 256e0 = -k
77 + o0 and o0 >= 0 and o0 <= 255) }'
78 index: '{ S_2[k] -> [(k - 256*floor((k)/256))] }'
79 reference: __pet_ref_6
84 relation: '{ S_2[k] -> __pet_test_0[k] }'
85 index: '{ S_2[k] -> __pet_test_0[(k)] }'
86 reference: __pet_ref_4
91 extension: '{ __pet_test_0[k] -> __pet_test_0[k''] : k'' <= k and k'' >= 252 and