11 domain: '{ S_0[k] : exists (e0 = [(-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 = [(k - o1)/256]: 256e0 = k - o1
14 and o1 >= 252 and o1 <= 257 and k >= 0 and k <= 255) }'
20 relation: '{ S_0[k] -> a[] }'
21 reference: __pet_ref_0
25 relation: '{ S_0[k] -> [5] }'
26 reference: __pet_ref_1
30 domain: '{ S_1[k] : exists (e0 = [(-2 + k)/256]: k >= 2 and k <= 255 and 256e0 <=
31 -252 + k and 256e0 >= -257 + k); S_1[0] }'
32 schedule: '{ S_1[k] -> [0, o1, 2] : exists (e0 = [(k - o1)/256]: 256e0 = k - o1
33 and o1 >= 252 and o1 <= 257 and k >= 0 and k <= 255) }'
39 relation: '{ S_1[k] -> a[] }'
40 reference: __pet_ref_2
44 relation: '{ S_1[k] -> [6] }'
45 reference: __pet_ref_3