João Pereira

This is related to a more general problem in Gobra where we often forgot to check for redeclarations, e.g., https://github.com/viperproject/gobra/issues/484

Before merging this, I would also like to run it with verifiedSCION

I believe it makes sense to merge these changes before I start looking at enabling the consistency checks. I am now running tests locally on the verified scion repository. @ArquintL...

@ArquintL should we close this PR? Right now, it seems unlikely that it will be merged. Regarding the changes to the encoding, if you think it is worth keeping, maybe...

As a workaround, selective importing of a package's contents was disabled for now

Update: there is a prototype solution on branch `fix-selective-import`

PR #619 provides a middle a good compromising solution to this issue. In particular, this solution does not desugar any private member, which should make the size of the translations...

If the overhead is actually high, we could try to use some sort of copy-on-write mechanism

> How important is this? If I am not missing something, this should be quite easy to implement. This is definitely not urgent, but there were was at least a...

Please don't merge it yet, it is currently causing some incompletenesses in VerifiedSCION