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