Prover died on simple program

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

class KillProver {
  method ProverShouldntDie() returns (k: nat)
    modifies set o: object {:trigger true} :: o
  {
    k := 0;
  }
}

Command to run and resulting output

Paste in VSCode

What happened?

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

Windows

[stefan-aws]

This seems to be caused by the trigger. If I run the program without verifying it, I get this boogie translation error: Error: trigger must mention all quantified variables, but does not mention: o#0. Introducing a constant predicate fixes the issue:

predicate T(o: object) {
  true
}

class KillProver {
  method ProverShouldntDie() returns (k: nat)
    modifies set o: object {:trigger T(o)} :: o
  {
    k := 0;
  }
}

[keyboardDrummer]

This is an error reporting issue. The message Error: trigger must mention all quantified variables, but does not mention: o#0 comes from Boogie but is emitted is a non-standard way, which causes it to be completely ignored by Dafny server, while on the CLI it is printed but otherwise ignored, allowing verification to continue (even though there is an error), leading to additional bad looking error output from the solver.