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[] }'
24 relation: '{ S_0[k] -> [5] }'
28 domain: '{ S_1[k] : exists (e0 = [(-2 + k)/256]: k >= 2 and k <= 255 and 256e0 <=
29 -252 + k and 256e0 >= -257 + k); S_1[0] }'
30 schedule: '{ S_1[k] -> [0, o1, 2] : exists (e0 = [(k - o1)/256]: 256e0 = k - o1
31 and o1 >= 252 and o1 <= 257 and k >= 0 and k <= 255) }'
37 relation: '{ S_1[k] -> a[] }'
41 relation: '{ S_1[k] -> [6] }'