MCE and possibly other parts of the code define functions not taking all quantified variables into account

[marcoeilers]

The following verifies with MCE:

field f: Int

method foo(x: Ref, y: Ref)
{
  inhale acc(x.f) && x.f == 4 && acc(y.f) && y.f == 5
  
  var myseq: Seq[Ref] := Seq(x, y)

  assert forall r: Ref :: {r in myseq} r in myseq ==> fn(r) > 2

  assert x in myseq
  assert y in myseq
  assert false
}

function fn(x: Ref): Int
  requires acc(x.f, wildcard)
{x.f}

It seems as if s.functionRecorderQuantifiedVariables() contains function arguments and s.quantifiedVariables contains quantified variables if we're inside a quantifier. Lots of places that define functions depending on one of them should probably take both into account. MCE snapshots only use s.functionRecorderQuantifiedVariables(), which is what causes the unsoundness above.

[marcoeilers]

Fixed in #898