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