12 domain: '{ S_0[k] : k >= 252 }'
13 schedule: '{ S_0[k] -> [0, k] }'
19 relation: '{ S_0[k] -> a[] }'
20 index: '{ S_0[k] -> a[] }'
21 reference: __pet_ref_0
25 relation: '{ S_0[k] -> [o0] : exists (e0 = floor((-k + o0)/256): 256e0 = -k
26 + o0 and o0 <= 255 and o0 >= 0) }'
27 index: '{ S_0[k] -> [(k - 256*floor((k)/256))] }'
28 reference: __pet_ref_1