1 sort bitvec 23
2 input 1 @inp2
3 sort bitvec 34
4 uext 3 2 11
5 sort bitvec 10
6 input 5 @inp6
7 uext 3 6 24
8 mul 3 4 7
9 constd 3 4294967297
10 sort bitvec 1
11 eq 10 8 9
12 constraint 11