Counterexample variable appears before is declaration

[TomSMaier]

Dafny version

4.9.0

Code to produce this issue

// dafny verify --extract-counterexample input.dfy

method F(y: int) ensures y != 2
{
  var x := 1;
  assert y != 2;
  var h := y;
  if * {
    h := h + h;
  }
  h := h + h;
}

Command to run and resulting output

$ dafny verify --extract-counterexample input.dfy
input.dfy(6,9): Error: assertion might not hold
 Related counterexample:
 WARNING: the following counterexample may be inconsistent or invalid. See dafny.org/dafny/DafnyRef/DafnyRef#sec-counterexamples
 input.dfy(4,0): initial state:
 assume 2 == y && 0 == h;
 input.dfy(5,12):
 assume 2 == y && 1 == x && 0 == h;
 
  |
6 |   assert y != 2;
  |          ^^^^^^


Dafny program verifier finished with 0 verified, 1 error

What happened?

In this function, the assertion assert y != 2 on line 4 does not hold. Its counterexample says that 0 == h at line 2, which is before h is declared at line 5.

Surprisingly, if the method is simplified in any way (remove more statements, simplify expressions, remove ensures, remove if *, ...), the issue disappears and 0 == h is not reported any more at line 2.

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

Linux, Mac