1 sort bitvec 2 2 zero 1 3 input 1 @inp3 4 const 1 10 5 add 1 -3 4 6 sort bitvec 1 7 eq 6 -2 5 8 constraint -7