Malformed triggers

[RustanLeino]

The following Dafny program has a old in a less-than-commendable, but legal, position:

predicate P(x: int)

lemma L()
  ensures forall y :: P(old(y))

Alas, the program causes Dafny to generate malformed Boogie code, because of the trigger Dafny generates for the quantifier.

% dafny test.dfy
test.dfy(5,28): Error: a matching pattern must be more than just a variable by itself: y#1
test.dfy(5,28): Error: a matching pattern must be more than just a variable by itself: y#1
2 name resolution errors detected in test__module.bpl

Additional trigger information:

Selected triggers: {old(y)}
Rejected triggers: {P(old(y))} (more specific than {old(y)})