Does not regonize heap dependent function as trigger

[sakehl]

I'm unsure if this is a bug or just a misunderstanding on my part.

But when writing a trigger, with heap dependent function, it does not seem to work.

Changing the trigger on line 8 towards hide0(x0,n, j) does work.

File

method main1(tid: Int, n: Int, x0: Array, x1: Array)
  requires 10 < n
  requires alen(x0) == n
  requires (forall i: Int ::
    {hide0(x0, n, i)}
    0 <= i && i < n ==> acc(hide0(x0, n, i), write) )
  requires (forall j: Int ::
          { get0(x0, n, j) }
          0 <= j && j < n ==>
          get0(x0, n, j) == 0)
{ 
  assert get0(x0, n, 0) == 0
}

///////////////////////////

domain Array  {

  function array_loc(a: Array, i: Int): Ref 

  function alen(a: Array): Int 

  function loc_inv_1(loc: Ref): Array 

  function loc_inv_2(loc: Ref): Int 

  axiom {
    (forall a: Array, i: Int ::
      { array_loc(a, i) }
      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
  }

  axiom {
    (forall a: Array :: { alen(a) } alen(a) >= 0)
  }
}

field int: Int

predicate hide0(x: Array, n: Int, i: Int) {
  n > 0 && i >= 0 && i < n && alen(x) == n &&
  acc(aloc(x, i).int, write)
}

// @opaque()
function get0(x: Array, n: Int, i: Int): Int
  requires 0 <= i && i < n
  requires acc(hide0(x, n, i), write)
  ensures result == unfolding acc(hide0(x,n, i), write) in aloc(x, i).int
{
  unfolding acc(hide0(x, n, i), write) in aloc(x, i).int
}

predicate hide1(x: Array, n: Int, i: Int) { 
  n > 0 && i >= 0 && i < n && alen(x) == n && 
  acc(aloc(x, i).int, write)
}

//@opaque()
function get1(x: Array, n: Int, i: Int): Int
  requires 0 <= i && i < n
  requires acc(hide1(x, n, i), wildcard)
  ensures result == unfolding acc(hide1(x,n, i), wildcard) in aloc(x, i).int
{
  unfolding acc(hide1(x, n, i), wildcard) in aloc(x, i).int
}


function aloc(a: Array, i: Int): Ref
  requires 0 <= i
  requires i < alen(a)
  decreases 
  ensures loc_inv_1(result) == a
  ensures loc_inv_2(result) == i
{
  array_loc(a, i)
}

[sakehl]

Additionally, when asserting the actual forall, this is the only thing I got working:

assert (forall j: Int ::
          { hide0(x0, n, j) } { get0(x0, n, j)}
          0 <= j && j < n ==>
          get0(x0, n, j) == 0)

[marcoeilers]

It's not a misunderstanding, this is supposed to work.
There are some known cases where heap-dependent functions as triggers can lead to problems, but this one really shouldn't as far as I can tell. I'll look into it.