11 domain: '{ S_0[k] : exists (e0 = floor((-2 + k)/256): k >= 0 and k <= 255 and 256e0
12 <= -252 + k and 256e0 >= -257 + k) }'
13 schedule: '{ S_0[k] -> [0, o1, 0] : exists (e0 = floor((k - o1)/256): 256e0 = k
14 - o1 and o1 >= 252 and o1 <= 257 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
32 domain: '{ S_1[k] : exists (e0 = floor((-2 + k)/256): k >= 2 and k <= 255 and 256e0
33 <= -252 + k and 256e0 >= -257 + k); S_1[0] }'
34 schedule: '{ S_1[k] -> [0, o1, 2] : exists (e0 = floor((k - o1)/256): 256e0 = k
35 - o1 and o1 >= 252 and o1 <= 257 and k >= 0 and k <= 255) }'
41 relation: '{ S_1[k] -> a[] }'
42 index: '{ S_1[k] -> a[] }'
43 reference: __pet_ref_2
47 relation: '{ S_1[k] -> [6] }'
48 index: '{ S_1[k] -> [(6)] }'
49 reference: __pet_ref_3