Issue with variable renaming in macro expansion

[marcoeilers]

Found by Paul Eibensteiner, the following program should verify, but Viper complains about an undeclared identifier 'var_m2', even though that variable is visible at the call site.

define m1(res) {
  res := var_m2
}

define m2(res) {
  var var_m2: Int

  var v0_1: Int
  {
    m1(v0_1)
  }

  res := var_m2
}

method caller() returns (value: Int)
{
  var res: Int
  {
    m2(res)
  }
  var value2: Int
  {
    m2(res)
  }
  value := res
}

[marcoeilers]

Fixed in PR #804