Inhaling a quantified self framing assertions gives insufficient permission error

[dewert99]

The following example gives the error shown as a comment:

domain IArray[T] {

  function aloc(a: IArray[T], i: Int): T

  function len(a: IArray[T]): Int

  function first(r: T): IArray[T]

  function second(r: T): Int

  axiom array_all_diff {
    (forall a: IArray[T], i: Int :: { (aloc(a, i): T) } (first((aloc(a, i): T)): IArray[T]) == a && (second((aloc(a, i): T)): Int) == i)
  }

  axiom length_nonneg {
    (forall a: IArray[T] :: { (len(a): Int) } (len(a): Int) >= 0)
  }
}

field f: Int

method test04_fail(rs1: IArray[Ref], rs2: IArray[Ref])
{
  var k1: Int
  var k2: Int
 // Inhale might fail. There might be insufficient permission to access (aloc(rs1, i1): Ref).f 
  inhale forall i1: Int, i2: Int :: 
  0 <= i1 && (i1 < (len(rs1): Int) && (0 <= i2 && i2 < (len(rs2): Int))) ==> 
  (acc((aloc(rs1, i1): Ref).f, write * write)  && acc((aloc(rs2, i2): Ref).f, write * write) && (aloc(rs1, i1): Ref).f < (aloc(rs2, i2): Ref).f)
}


method self_framing(rs1: IArray[Ref], rs2: IArray[Ref], i1: Int, i2: Int)
requires 0 <= i1 && (i1 < (len(rs1): Int) && (0 <= i2 && i2 < (len(rs2): Int))) ==> 
  (acc((aloc(rs1, i1): Ref).f, write * write)  && acc((aloc(rs2, i2): Ref).f, write * write) && (aloc(rs1, i1): Ref).f < (aloc(rs2, i2): Ref).f)

even though the quantified assertion is self framing as shown by the self_framing method.

I'm guessing this has to do with the way the pure and impure parts of quantified permissions are split up leading to an issue if the pure part doesn't trigger the impure part to get the required permission