11 domain: '{ S_0[k] : k >= 0 and k <= 255 }'
12 schedule: '{ S_0[k] -> [0, o1] : exists (e0 = [(-k + o1)/256]: 256e0 = -k + o1 and
13 o1 >= 252 and k >= 0 and k <= 255) }'
19 relation: '{ S_0[k] -> a[] }'
20 reference: __pet_ref_0
24 relation: '{ S_0[k] -> [5] }'
25 reference: __pet_ref_1