Fragility issue when inherited trait function used in inherited contract

[erniecohen]

Dafny version

4.7.0

Code to produce this issue

module Ma {
trait {:termination false} A { 
    ghost predicate has(d:int,b:bool) decreases this
    ghost predicate p(d:int) { forall b :: has(d,b) }
    function top():(d:int) ensures p(d)
}  
} module Mb { import opened Ma  // commenting this out breaks rank() and def of r below
datatype C extends A = C(a:A) {
    ghost predicate has(d:int,b:bool) decreases this { a.has(d,b) }    
    function top():(r:int) decreases this ensures p(r) {
        var ad := this as A;  // this shouldn't be needed
        var r := a.top();
        assert p(r) by {
            forall b ensures ad.has(r,b) { 
                assert has(r,b);
            }
        }
        r
}}}

Command to run and resulting output

See comments in the code for issues:
1) Getting the use of the definition of `p` requires explicitly casting to A
2) Removing the module break breaks the termination proofs of a.top() and a.has().

What happened?

Commenting out the hint (or the module break) breaks verification.

What type of operating system are you experiencing the problem on?

Mac