Dafny assumes non-termination for a loop it cannot prove termination

[TomSMaier]

Dafny version

4.11.0

Code to produce this issue

// dafny verify input.dfy

method M() {
  var q := true;
  while q {
    q := false;
  }
  assert false;
}

Command to run and resulting output

$ dafny verify input.dfy
input.dfy(5,2): Error: cannot prove termination; try supplying a decreases clause for the loop
  |
5 |   while q {
  |   ^^^^^


Dafny program verifier finished with 0 verified, 1 error

What happened?

In this snippet, the loop is executed exactly once and the execution fails at assert false;. Because the loop lacks a decreases clause, Dafny cannot prove termination for this loop. Dafny then treats the loop as non-terminating and marks the following assert false; as verified.

When providing the the correct decreases clause decreases q, the loop verifies and the assert false is flagged as failing.
I believe the assert false; should be marked as failing in either case, because it is indeed reachable.

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

Mac