Opaque blocks prove variable previously assigned

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

method FreshEnsures() {
  var c: int;
  ghost var wasAssigned := assigned(c);
  opaque ensures c == 1 {
    c := 1;
  }
  assert wasAssigned;
}

Command to run and resulting output

dafny verify

What happened?

In a time-traveling verification superpower, Dafny is able to prove that c was assigned before it was assigned.
Fortunately, this knowledge is not ported back to where it should happen but it's unsettling, and I can't rule out that we can prove something unexpected because of that.
I'm working on a fix because for referrers, we need to be able to know that when a variable is declared, it's not assigned yet.

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

Windows