Information following from field access receiver not known when checking for permission

[marcoeilers]

The following program verifies in Carbon but not in Silicon (with or without MCE):

field f: Int

function flag(): Bool

function assuming(b: Bool, r: Ref): Ref
  ensures b
  ensures result == r

method m(r: Ref)
{
  inhale flag() ==> acc(r.f)
  var tmp : Int
  tmp := assuming(flag(), r).f
}

The issue seems to be that the knowledge that flag() is true, which follows from the field access receiver expression, is apparently not known when checking for the field permission. If the expression is moved to a separate statement, the program verifies:

method m2(r: Ref)
{
  inhale flag() ==> acc(r.f)
  var tmp : Int
  var r2: Ref
  r2 := assuming(flag(), r)
  tmp := r2.f
}

[marcoeilers]

These also fail:

method m2(r: Ref)
{
  inhale acc(r.f, flag() ? write : none)
  var tmp : Int
  tmp := assuming(flag(), r).f
}

method m3(r: Ref)
{
  inhale acc(r.f, flag() ? write : none)
  exhale acc(assuming(flag(), r).f)
}

method m4(r: Ref)
{
  inhale flag() ==> acc(r.f)
  exhale acc(assuming(flag(), r).f)
}