1 sort bitvec 17
2 input 1 @inp2
3 sort bitvec 34
4 uext 3 2 17
5 input 1 @inp5
6 uext 3 5 17
7 mul 3 4 6
8 constd 3 4294967295
9 sort bitvec 1
10 eq 9 7 8
11 constraint 10