Separately translated triggers not recorded in FunctionRecorder

[marcoeilers]

For quantifiers that have user-provided triggers that do not occur inside the quantifier body and are therefore translated separately, any information recorded in the FunctionRecorder about those trigger expressions is discarded afterwards. As a result, the following program results in a warning Could not resolve expression idx(s, i) (test.vpr@3.24--3.33) during the axiomatisation of function amm. This typically happens if the expression is on an infeasible path, i.e. is dead code. The unresolved expression will be replaced by a fresh symbol, i.e. an arbitrary value. (but it does verify).

function amm(s: Seq[Int]): Bool
{
    forall i: Int :: { idx(s, i)}  i >= 0 && i < |s| ==> idx2(s, i) > 0
}

function umm(s: Seq[Int]): Int
  requires amm(s)
  requires |s| > 0
  ensures result > 0
{ idx(s, 0) }


function idx(s: Seq[Int], i: Int): Int
  //requires i >= 0
  //requires i < |s|
{
  i >= 0 && i < |s| ? s[i] : 0
}

function idx2(s: Seq[Int], i: Int): Int
  requires i >= 0
  requires i < |s|
{
  i >= 0 && i < |s| ? s[i] : 0
}