Parser and pretty-printer do not preserve scopes

[marcoeilers]

The Viper language allows users to write blocks (enclosed by curly braces) inside of methods to create local scopes.
For example, the following program creates a scope after the conditional:

method main1(b: Bool)
{
    if (b) {
        var x: Int
        x := 45
        assert x > 34
    } 
    {
      var x: Int
      x := 45
      assert x > 34
    }
}

There are two issues with this:

1. Viper's parser flattens nested scopes into their surrounding scope (unless they are contained directly by conditional or loop statements). As a result, in the AST constructed from this program, the method body is a Seqn that contains a conditional, an assignment, and an assert statement, instead of containing a conditional and a nested Seqn. This, in turn, leads to a consistency error claiming that there is a duplicate identifier x. The error does not occur if the AST is not flattened. (See discussion in issue Flatten macro expansions #279 regarding this problem; the flattening that is performed was supposed to happen only for expanded macro bodies.)
2. Even if the AST is constructed correctly with a Seqn inside a Seqn (e.g., by a frontend), Viper's pretty-printer does not emit curly braces around the inner Seqn. Thus, if the program is pretty-printed, the inner scope vanishes, and the program turns from one without duplicate identifiers into one with duplicate identifiers inside the conditional.

[marcoeilers]

This was fixed in PR #704.