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