1 sort bitvec 16
2 input 1 @inp2
3 input 1 @inp3
4 sort bitvec 32
5 uext 4 2 16
6 uext 4 3 16
7 udiv 4 5 6
8 urem 4 5 6
9 udiv 1 2 3
10 urem 1 2 3
11 slice 1 7 15 0
12 slice 1 8 15 0
13 sort bitvec 1
14 eq 13 9 11
15 eq 13 10 12
16 and 13 14 15
17 constraint -16