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