Recording possible triggers from inside let-expressions properly

[marcoeilers]

When recording possible triggers while evaluating a quantifier body, this PR changes Silicon so that it records a version of the expression that has the let-bound variable replaced with its body. This is necessary because otherwise, possible triggers from inside let-expressions are essentially unavailable as triggers, since the let-bound variable is not available in the trigger itself, and without it, the expressions don't match syntactically.

[fpoli]

Is the subscription exponential in the number of AST nodes in the worst case (e.g. a let variable used more than once and defined in the body of another let, used and defined in the body of another let, and so on)? I'm asking because we considered using this encoding stile in Prusti at some point (we currently don't) as a way to avoid generating an expression with a worst-case size exponential in the number of Rust statements.

[marcoeilers]

Is the subscription exponential in the number of AST nodes in the worst case (e.g. a let variable used more than once and defined in the body of another let, used and defined in the body of another let, and so on)? I'm asking because we considered using this encoding stile in Prusti at some point (we currently don't) as a way to avoid generating an expression with a worst-case size exponential in the number of Rust statements.

I guess it would be, yes.
It would only be a problem if you have large expressions inside quantifier bodies though.
I thought that there were different places in Viper that deal with let-expressions by inlining them, but I can't actually find any, so maybe that's not actually true.