1 sort bitvec 8 2 input 1 @inp2 3 const 1 11111111 4 add 1 2 -2 5 sort bitvec 1 6 eq 5 3 4 7 constraint 6