Reference non-aliasing only assertable after a fold, but not before

[mschwerhoff]

field f: Int

predicate p(x: Ref) {
  acc(x.f) && x.f >= 3
}

method foo(x: Ref, y: Ref)
  requires p(x) && p(y)
  requires unfolding p(y) in y.f == 7 // Needed (but explainable)
{
  unfold p(x)
  x.f := 4 // Needed for final assertion
  assert x != y // Fails
  fold p(x)
  assert x != y // Holds (also without line 13)
}

My hunch is an incompleteness related to heap snapshots.