1 sort bitvec 32
2 input 1 x
3 sort bitvec 5
4 input 3 n
5 constd 3 31
6 consth 1 80000000
7 uext 1 4 27
8 sra 1 2 7
9 add 1 2 6
10 uext 1 4 27
11 srl 1 9 10
12 uext 1 4 27
13 srl 1 6 12
14 sub 1 11 13
15 sort bitvec 1
16 eq 15 8 14
17 uext 1 4 27
18 srl 1 2 17
19 xor 1 18 13
20 sub 1 19 13
21 eq 15 8 20
22 and 1 2 6
23 uext 1 4 27
24 srl 1 22 23
25 uext 1 4 27
26 srl 1 2 25
27 add 1 24 24
28 sub 1 26 27
29 eq 15 8 28
30 uext 1 5 27
31 srl 1 2 30
32 neg 1 31
33 sub 3 5 4
34 uext 1 33 27
35 sll 1 32 34
36 or 1 26 35
37 eq 15 8 36
38 xor 1 2 32
39 uext 1 4 27
40 srl 1 38 39
41 xor 1 40 32
42 eq 15 8 41
43 or 15 -16 -21
44 or 15 -29 -37
45 or 15 43 44
46 or 15 45 -42
47 constraint 46