Opaque blocks allow proving false

[RustanLeino]

Dafny version

4.9.1

Code to produce this issue

method Main() {
  var c: object;
  opaque
    ensures fresh(c)
  {
    c := new object;
  }
  assert false;
}

Command to run and resulting output

% dafny verify test.dfy

Dafny program verifier finished with 1 verified, 0 errors

What happened?

The assert false; is proved, despite the fact that it is reachable.

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

Mac