8 domain: '{ S_0[k] : exists (e0 = [(507 - k)/256]: k >= 0 and k <= 255 and 256e0
9 >= 252 - k and 256e0 <= 261 - k) }'
10 schedule: '{ S_0[k] -> [0, o1] : exists (e0 = [(-k + o1)/256]: 256e0 = -k + o1 and
11 o1 >= 252 and k <= 255 and k >= 0 and o1 <= 261) }'
17 relation: '{ S_0[k] -> a[] }'
21 relation: '{ S_0[k] -> [5] }'