Name clash between Dafny-level and tactic-level

[ggrov]

Consider a method

method m(x : int)
requires x > 10
ensurer x > 10
{
tac();
}

using a tactic:

tactic tac()
{
tactic var x := 5;
tactic var p := tactic.ensures;
assert p[0];
}

Here, x is both a variable in the code and in the tactic. Following the semantics this is allowed and the tactic-level version will override the Dafny level meaning the (incorrect) assertion
assert 5 > 10;
will be generated. The two other options are

1. Have a disjoint name space between Dafny level (i.e. tactic.vars) and tactic-level. This will be too restrictive.
2. (preferable) rename the tactic variable when necessary before interpreting it (this needs to be hidden from users)

Case 2 will in our case mean that before applying the tactic we do the following

tactic tac()
{
tactic var xx := 5;
tactic var p := tactic.ensures;
assert p[0];
}

meaning no more clashes.