1 sort bitvec 32
2 input 1 x
3 input 1 y
4 sort bitvec 1
5 slice 4 2 31 31
6 slice 4 3 31 31
7 sort bitvec 31
8 slice 7 2 30 0
9 slice 7 3 30 0
10 ult 4 8 9
11 and 4 5 -6
12 and 4 -5 6
13 and 4 -11 -12
14 and 4 10 13
15 or 4 14 11
16 slt 4 2 3
17 and 4 -15 16
18 constraint 17