Old on a local variable affects triggering

[vakaras]

The following example fails to verify:

domain Snap$Array {
  function read(arr: Snap$Array, idx: Int): Int
}

function snap(self: Ref): Snap$Array
  requires acc(Array(self), write)

predicate Array(self: Ref)

method m_foo()
{
  var array: Ref
  inhale acc(Array(array), write)
  inhale (forall i: Int :: { read(snap(array), i) }
    0 <= i && i < 10 ==> read(snap(array), i) == 42)
  label l8
  exhale acc(Array(array), write)
  inhale acc(Array(array), write)
  assert array == old[l8](array)
  inhale forall i: Int ::
    { read(snap(array), i) } // using *only* this trigger fails verification
    // { read(snap(old[l8](array)), i) } // it's this trigger that makes verification succeed
    0 <= i && i < 10  ==> read(snap(array), i) == old[l8](read(snap(array), i))
  assert (forall i: Int :: { read(snap(array), i) }
    0 <= i && i < 10 ==> read(snap(array), i) == 42)
}

Replacing trigger read(snap(array), i) with read(snap(old[l8](array)), i) makes the example to verify even though Silicon clearly knowns that array == old[l8](array).

@mschwerhoff Any clue what is happening here?

The example was found and reduced by Pointerbender.

[mschwerhoff]

Potentially related issues: #362, #371

[marcoeilers]

Resolved by PR #710.