11 domain: '{ S_0[k] : exists (e0 = floor((-6 + k)/256): k >= 0 and k <= 255 and 256e0
12 <= -252 + k and 256e0 >= -261 + k) }'
13 schedule: '{ S_0[k] -> [0, o1] : exists (e0 = floor((-k + o1)/256): 256e0 = -k +
14 o1 and o1 >= 252 and o1 <= 261 and k >= 0 and k <= 255) }'
20 relation: '{ S_0[k] -> a[] }'
21 index: '{ S_0[k] -> a[] }'
22 reference: __pet_ref_0
26 relation: '{ S_0[k] -> [5] }'
27 index: '{ S_0[k] -> [(5)] }'
28 reference: __pet_ref_1