Let binding a quantified variable prevents Viper from inferring triggers

[tillarnold]

In Prusti we have encountered a case where our generated code does not verify due to us storing a variable from a quantifier in a temporary variable. While it is possible for us to address this issue in our own code, for example by postprocessing our generated viper code, we were wondering if it would be desirable for this kind of code to complete verification in viper itself.

This minimized example below shows the issue. As it is written here the verificaion will fail. However if f_get(alias) is replaced with f_get(qvar) then verification completes.

method main() {
    assume forall qvar: Int ::
      let alias == (qvar) in
        f_get(alias) == f_clamp() //replace alias with qvar here, then in verifies
    assert f_get(10) == 0
}

function f_get(idx: Int): Int


function f_clamp(): Int
  ensures result == 0

[marcoeilers]

Fixed in #753 and viperproject/silicon#771.