Getting invariant to pass requires repeating a subexpression of it

[keyboardDrummer]

In the following code there is a loop invariant invariant a.get(0).getA() == 1. To get it to pass we have to write var initialValue := a.get(0).getA(), assigning a subexpression of the invariant to a variable, in the body of the loop. This shouldn't be necessary.

class GhostArray<T> {
  @Axiom
  ghost static method create(size: int) returns (r: GhostArray<T>)
    ensures r.size() == size && fresh(r)

  ghost function size(): nat

  ghost function get(index: nat): T
    reads this

  @Axiom
  ghost method sett(index: nat, value: T)
    modifies this
    ensures get(index) == value && forall i: nat :: i != index ==> old(get(i)) == get(i)
}

ghost method nullablePointArrayOfSize10()
{
  var a: GhostArray<Point?> := GhostArray<Point?>.create(10);
  var point1: Point := new Point(0, 0);
  var pointZero: Point := new Point(1, 2);
  a.sett(0, pointZero);
  {
    var i: int := 1;
    while i < a.size()
      invariant a.get(0) != null
      invariant a.get(0).getA() == 1
      modifies a
    {
      // uncommenting the next line causes this to pass
      // var initialValue := a.get(0).getA();
      a.sett(i, point1);
      i := i + 1;
    }
  }
}

class Point {
  ghost var a: int
  ghost var b: int

  @Axiom
  ghost constructor(a_: int, b_: int)
    ensures this.a == a_
    ensures this.b == b_

  ghost function getA(): (result?: int)
    reads this
  {
    a
  }
}