BPL Translation Error with sets:

[xtrm0]

In dafny 3.6:
Minimum repro:

function Succ(x: int): int
{
  x + 1
}

function FailingLemma(): nat
{
  var st : set<int> :| forall x | x in st :: Succ(x) > 0;
  0
}

Output:

$ dafny /version
Dafny 3.6.0.40511
$ dafny repro.dfy 
/build/repro.dfy(8,23): Error: trigger must mention all quantified variables, but does not mention: x#3
1 name resolution errors detected in /tmp/repro__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

/tmp/repro__module.bpl(2934,46): Error: trigger must mention all quantified variables, but does not mention: x#3
1 name resolution errors detected in /tmp/repro__module.bpl

[xtrm0]

This is present in every 3.X.Y release

[xtrm0]

Fixed in #2745