Opaque blocks with nested functions in ensures clause

[clid]

Dafny version

4.11

Code to produce this issue

class A {
  var b_obj : B

  constructor B() { b_obj := new B; }

  method main() returns (res : int)
    ensures res == 1
  {
    opaque
      modifies {}
      ensures res == b_obj.b_contract()
      // ensures res == b_obj.b_contract_ext()    // With this formula verification succeeds.
    {
      res := b_obj.b_method();
      // assert res == b_obj.b_contract();    // With this assertion verification succeeds.
    }
    return res;
  }
}

class B
{
  function b_contract() : int
  {
    b_contract_ext()
  }

  function b_contract_ext() : int
  {
    1
  }

  method b_method() returns (o : int)
    ensures o == b_contract_ext()
    //ensures o == b_contract()    // With this contract verification succeeds.
  {
    return 1;
  }
}

Command to run and resulting output

dafny verify test.dfy 
test.dfy(11,18): Error: ensures might not hold
   |
11 |       ensures res == b_obj.b_contract()
   |                   ^^

Dafny program verifier finished with 2 verified, 1 error

What happened?

There seems to be an issue with reasoning with nested functions when proving ensures clauses of opaque blocks, as shown by the attached code which fails to verify. I have added some commented lines which would make the verification succeed, but should not be necessary. Also, if instead replacing the opaque block with a similarly defined method call or loop there are no problems verifying the code, and these cases should behave similarly to an opaque block.

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

Linux, Windows