Termination Plugin: Generates ill-formed Viper code for input with let expressions

[Felalolf]

For the following Viper code

function bad_bda1d7d_F(): Bool
  requires decreases
{
  (let a_V1 == (1) in a_V1 >= 1) && (let b_V2 == (0) in b_V2 >= 0)
}

the beforeVerify method of TerminationPlugin generates the following Viper method:

// decreases 
method bad_bda1d7d_F_termination_proof()
{
  var a_V1: Int
  inhale a_V1 == 1
  if ((let a_V1 ==
    (1) in
    a_V1 >= 1)) {
    var b_V2: Int
    inhale b_V2 == 0
  }
}

The code is ill-formed since a_V1 is both declared as a variable and used in the let binding. The error does not happen without the second let (e.g. without a second conjunct or if the second conjunct is not a let expression).

My guess is that the handling of short circuiting is incorrect because it uses the original Viper code as the condition instead of a transformed version.

[Felalolf]

This code was generated by Gobra. I will write a fully Viper client producing the error later. For now, I just wanted to document the error so that it is not forgotten.

[marcoeilers]

Apparently the generated code was not ill-formed at all. The issue was that the pretty-printer did not correctly pretty-print some scopes that were required to make it well-defined (see issue #697). That issue was fixed a while ago, which also fixes this issue. The Fix in PR #715 was not required (and actually incorrect) when the actual scopes are taken into account.