On the OBDD complexity of the most significant bit of integer multiplication