Open MikaelMayer opened 3 weeks ago
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;
}
}
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.
Dafny version
latest-nightly
Code to produce this issue
Command to run and resulting output
What happened?
What type of operating system are you experiencing the problem on?
Windows