1 sort bitvec 1
2 zero 1
3 sort bitvec 31
4 input 3 @inp4
5 sort bitvec 32
6 concat 5 2 4
7 sort bitvec 30
8 input 7 @inp8
9 sort bitvec 2
10 ones 9
11 concat 5 8 10
12 udiv 5 6 11
13 slice 1 12 31 31
14 constraint 13