Surprising invalid counterexample when using if true

[TomSMaier]

Dafny version

4.9.0

Code to produce this issue

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

method F(m: int)
{
  var y := 0;
  if true {
    y := 1;
  }
  var u := m - y;
  assert 0 < m;
}

method F1(m: int)
{
  var y := 0;
  y := 1;
  var u := m - y;
  assert 0 < m;
}

Command to run and resulting output

$ dafny verify --extract-counterexample input.dfy
input.dfy(10,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 0 == m && 0 == y;
 input.dfy(5,12):
 assume 0 == m && 0 == y;
 input.dfy(7,10):
 assume 0 == m && 1 == y;
 input.dfy(9,16):
 assume 0 == m && 0 == u && 1 == y;
 
   |
10 |   assert 0 < m;
   |          ^^^^^

input.dfy(18,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(14,0): initial state:
 assume 0 == m;
 input.dfy(15,12):
 assume 0 == m && 0 == y;
 input.dfy(16,8):
 assume 0 == m && 1 == y;
 input.dfy(17,16):
 assume 0 == m && 1 == y && -1 == u;
 
   |
18 |   assert 0 < m;
   |          ^^^^^


Dafny program verifier finished with 0 verified, 2 errors

What happened?

In both methods, assert m < 0 does not hold.
In method F, the counterexample is invalid: it should be -1 == u instead of 0 == u.
When removing if true, the counterexample becomes valid, as seen in the output for F1.

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

Linux, Mac