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 ult 5 7 8
10 eq 5 6 9
11 slice 5 2 31 31
12 slice 5 3 31 31
13 ult 5 2 3
14 xor 5 13 11
15 xor 5 14 12
16 eq 5 6 15
17 sub 1 2 4
18 sub 1 3 4
19 slt 5 17 18
20 eq 5 13 19
21 xor 5 6 11
22 xor 5 21 12
23 eq 5 13 22
24 or 5 -10 -16
25 or 5 -20 -23
26 or 5 24 25
27 constraint 26