Incompleteness when exhaling a QP whose permission expression depends on the quantified variable inside a package statement

[marcoeilers]

@jcp19 found this one.

The following example does not verify but should:

field f: Int

method m(xs: Set[Ref], ys: Set[Ref])
{
  inhale forall r: Ref :: r in xs ==> acc(r.f, r in ys ? 1/2 : none)

  package true --* true {
    assert forall r: Ref :: r in xs ==> acc(r.f, r in ys ? 1/2 : none)
  }
}