1 sort bitvec 16
2 input 1 @inp2
3 input 1 @inp3
4 sort bitvec 32
5 concat 4 2 3
6 constd 4 103
7 sort bitvec 1
8 eq 7 5 6
9 slice 1 6 31 16
10 slice 1 6 15 0
11 eq 7 2 9
12 eq 7 3 10
13 and 7 11 12
14 eq 7 8 13
15 constraint -14