1 sort bitvec 33
2 input 1 @inp2
3 sort bitvec 66
4 uext 3 2 33
5 mul 3 4 4
6 constd 3 18446744073709551617
7 sort bitvec 1
8 eq 7 5 6
9 constraint 8