1 sort bitvec 1
2 input 1 @inp2
3 input 1 @inp3
4 eq 1 2 -3
5 constraint 4
6 zero 1
7 eq 1 6 -3
8 constraint 7
9 ult 1 2 -3
10 eq 1 -3 6
11 and 1 9 10
12 constraint 11