1 sort bitvec 1
2 input 1 @inp2
3 sort bitvec 32
4 one 3
5 input 3 @inp5
6 add 3 4 -5
7 ite 3 2 -5 6
8 uext 3 -2 31
9 add 3 -5 8
10 eq 1 7 9
11 ite 3 2 6 -5
12 uext 3 2 31
13 add 3 -5 12
14 eq 1 11 13
15 or 1 -10 -14
16 constraint 15