PR# 19939 Post-condition monitoring partially disabled with multiple inheritance

When a the post-condition of a method f of a class A is refined in two subclasses B and C, and then repeatedly inherited in a class D, the post-condition of f in D is the conjunction of all the post-condition of all the parent of D for f.
This is confirmed by the flatview of D in EiffelStudio.
However, the Eiffel compiler failed to do that unless f is explicitly redefined in D.
If either C.f is undefined in D or C.f is renamed in D and B.f is selected in D, then the post-conditions monitored in the final program for f in D are only those from B and A, not from C.

The project in attachment demonstrates the problem using undefinition.
The same issue is obtained when replacing, in D, the undefinition of f by a rename/select.

More detailed explanations have been given on the user group :
https://groups.google.com/g/eiffel-users/c/5Lp5DqdYwsg

Compile and run the project in attachment.
The first d.f call in the test program should yield a post-condition exception (from C).
It does not. The other calls, in comments, show that post-conditions from the B path are however taken into account.

Thank you for your report, we will look into this issue.

Attachments for problem report #19939