1 sort bitvec 32
2 input 1 x
3 input 1 y
4 const 1 10000000000000000000000000000000
5 sort bitvec 1
6 slt 5 2 3
7 add 1 2 4
8 add 1 3 4
9 ulte 5 8 7
10 eq 5 6 -9
11 slte 5 2 3
12 ulte 5 7 8
13 eq 5 11 12
14 sgt 5 2 3
15 eq 5 -12 14
16 sgte 5 2 3
17 eq 5 9 16
18 ult 5 2 3
19 ulte 5 3 2
20 eq 5 18 -19
21 ugt 5 2 3
22 ulte 5 2 3
23 eq 5 21 -22
24 ugte 5 2 3
25 ulte 5 3 2
26 eq 5 24 25
27 or 5 -10 -13
28 or 5 -15 -17
29 or 5 -20 -23
30 or 5 27 28
31 or 5 29 30
32 or 5 31 -26
33 constraint 32