Proof for Unreachability requires assert false

[TomSMaier]

Dafny version

4.10.0

Code to produce this issue

// dafny verify input.dfy

method A(q: int)
  requires 0 * q >= q
  requires q * q == q - q + 1716004 // equivalent to `requires false`

method F1(m: int) {
  A(m);
  A(0); // fails
}

method F2(m: int) {
  A(m);
  assert false; // passes
  A(0);
}

Command to run and resulting output

$ dafny verify input.dfy
input.dfy(8,3): Error: a precondition for this call could not be proved
  |
8 |   A(m);
  |   ^^^^^

input.dfy(4,17): Related location: this is the precondition that could not be proved
  |
4 |   requires 0 * q >= q
  |            ^^^^^^^^^^

input.dfy(8,3): Error: a precondition for this call could not be proved
  |
8 |   A(m);
  |   ^^^^^

input.dfy(5,17): Related location: this is the precondition that could not be proved
  |
5 |   requires q * q == q - q + 1716004 // equivalent to `requires false`
  |            ^^^^^^^^^^^^^^^^^^^^^^^^

input.dfy(9,3): Error: a precondition for this call could not be proved
  |
9 |   A(0);
  |   ^^^^^

input.dfy(5,17): Related location: this is the precondition that could not be proved
  |
5 |   requires q * q == q - q + 1716004 // equivalent to `requires false`
  |            ^^^^^^^^^^^^^^^^^^^^^^^^

input.dfy(13,3): Error: a precondition for this call could not be proved
   |
13 |   A(m);
   |   ^^^^^

input.dfy(4,17): Related location: this is the precondition that could not be proved
  |
4 |   requires 0 * q >= q
  |            ^^^^^^^^^^

input.dfy(13,3): Error: a precondition for this call could not be proved
   |
13 |   A(m);
   |   ^^^^^

input.dfy(5,17): Related location: this is the precondition that could not be proved
  |
5 |   requires q * q == q - q + 1716004 // equivalent to `requires false`
  |            ^^^^^^^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 0 verified, 5 errors

What happened?

Because the preconditions of method A are unsatisfiable, all statements after A(m) are unreachable.

In F1, dafny does not detects this.
In F2, with an extra assert false;, dafny correctly identifies that the other statements are not reachable.

It is surprising that the statement assert false; is the missing link for this proof.

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

Linux, Mac