Trivial assertion violation in Dafny

Question

Why does Dafny claim this simple assertion is possibly violated?

var b := new int[2];
b[0],b[1] := 1, -2;
assert exists k | 0 <= k < b.Length :: (b[k] == 1 || b[k] == -1);

Answer 1

This has to do with the way Dafny handles existential quantifiers. It will (almost) never "guess" a value for you. Instead, Dafny uses syntactic heuristics (called "triggers") to try certain values from the context.

In your assertion, the trigger is b[k], which means that Dafny will only try values of k such that the expression b[k] is mentioned explicitly.

Thus, one way to fix the assertion is to explicitly mention the correct value for k, by adding the assertion

assert b[0] == 1;

or even

assert b[0] == 1 || b[0] == -1

---

This is somewhat related to this question.

For more on triggers see this answer.