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