1 sort bitvec 32
2 input 1 @inp2
3 sort bitvec 29
4 zero 3
5 sort bitvec 2
6 input 5 @inp6
7 sort bitvec 1
8 one 7
9 sort bitvec 31
10 concat 9 4 6
11 concat 1 10 8
12 urem 1 2 11
13 slice 3 12 31 3
14 eq 7 13 4
15 constraint -14