12 domain: '{ S_0[k] : k >= 252 and k <= 257 }'
13 schedule: '{ S_0[k] -> [0, k, 0] }'
21 index: '{ S_0[k] -> a[] }'
22 reference: __pet_ref_0
28 domain: '{ S_1[k] : exists (e0 = floor((-1 + k)/256): k >= 252 and k <= 257 and
29 256e0 >= -256 + k and 256e0 <= -2 + k) }'
30 schedule: '{ S_1[k] -> [0, k, 2] }'
38 index: '{ S_1[k] -> a[] }'
39 reference: __pet_ref_1