1 sort bitvec 8 2 input 1 @inp2 3 constd 1 1 4 udiv 1 2 2 5 sort bitvec 1 6 eq 5 3 4 7 constraint 6