Heap dependent function triggering

[JonasAlaif]

The following program verifies when it shouldn't. This is due to a matching loop that gets introduced. In general, the way Viper generates the triggers for definitional axioms is kinda strange. This is an issue both in Silicon and in Carbon.

predicate OhHi() { true }

function mark(): Bool
{
  true
}

function make_your_own_matching_loop(n: Int): Bool
  requires OhHi()
{
    n <= 0 ? true : (unfolding OhHi() in mark()) && make_your_own_matching_loop(n - 1)
}

method main()
{
  fold OhHi()
  var f: Bool := make_your_own_matching_loop(49)
  assert f
}