9 domain: '{ S_0[k] : exists (e0 = [(507 - k)/256]: k >= 0 and k <= 255 and 256e0
10 <= 257 - k and 256e0 >= 252 - k) }'
11 schedule: '{ S_0[k] -> [0, o1, 0] : exists (e0 = [(k - o1)/256]: 256e0 = k - o1
12 and o1 >= 252 and k <= 255 and k >= 0 and o1 <= 257) }'
18 relation: '{ S_0[k] -> a[] }'
22 relation: '{ S_0[k] -> [5] }'
26 domain: '{ S_1[k] : k <= 255 and k >= 252; S_1[0] }'
27 schedule: '{ S_1[k] -> [0, o1, 2] : exists (e0 = [(k - o1)/256]: 256e0 = k - o1
28 and o1 >= 252 and k <= 255 and k >= 0 and o1 <= 257) }'
34 relation: '{ S_1[k] -> a[] }'
38 relation: '{ S_1[k] -> [6] }'