1 sort bitvec 8
2 input 1 @inp2
3 sort bitvec 1
4 input 3 @inp4
5 ite 1 4 -2 -2
6 eq 3 -2 5
7 constraint 6