1 sort bitvec 8
2 input 1 x
3 input 1 y
4 sort bitvec 3
5 one 4
6 one 1
7 sort bitvec 1
8 slt 7 2 3
9 uext 1 5 5
10 sra 1 2 9
11 uext 1 5 5
12 sra 1 3 11
13 and 1 -2 3
14 and 1 13 6
15 sub 1 10 12
16 sub 1 15 14
17 slice 7 16 7 7
18 eq 7 8 17
19 ult 7 2 3
20 uext 1 5 5
21 srl 1 2 20
22 uext 1 5 5
23 srl 1 3 22
24 sub 1 21 23
25 sub 1 24 14
26 slice 7 25 7 7
27 eq 7 19 26
28 or 7 -18 -27
29 constraint 28