Havoc scoped variables explicitly

[gauravpartha]

This pull request adds explicit havocs to scoped variables. Previously, havocs were omitted, which is sound because Carbon introduces a unique Boogie variable for each scoped variable and thus the implicit havoc for the variable at the beginning of the program is sufficient. The reason for adding explicit havocs is (1) to make the encoding reflect the Viper program structure more closely, and (2) to allow reusing the same Boogie variable for scoped variables that do not overlap.