1 sort bitvec 32
2 input 1 @inp2
3 sort bitvec 5
4 constd 3 2
5 constd 3 3
6 constd 3 29
7 constd 1 8
8 sdiv 1 2 7
9 uext 1 4 27
10 sra 1 2 9
11 uext 1 6 27
12 srl 1 10 11
13 add 1 2 12
14 uext 1 5 27
15 sra 1 13 14
16 sort bitvec 1
17 eq 16 8 15
18 constraint -17