1 sort bitvec 8 2 input 1 @inp2 3 sort bitvec 3 4 one 3 5 uext 1 4 5 6 srl 1 2 5 7 sort bitvec 1 8 slice 7 6 7 7 9 constraint 8