You are right that the compiler does not do the right thing because when merging 2 routines it keeps the body of the selected version as is included its contracts but the contracts as seen in the parents not the descendants because the code is not replicated.

However, although not formalized yet, it is most likely that the compiler will now reject joining of 2 routines if one of them is kept as is, it will now force you to redefine the body of the routine so that you have a chance to provide an implementation that will satisfy any of the merged preconditions and of course ensures all merged postconditions.

When this is implemented, we will close this bug report. In the meantime, make the redefinition manually when you do such a merge.