Fixing issues #410 and #338

[marcoeilers]

When inside a package statement, we have to always call the continuation, we cannot use shortcuts that just return Success(). If we do that, Silicon still continues verification after the package block, but it will not know that it has to continue with the heap from the infeasible branch.

Thus, this PR:

• adds a new state entry which marks whether we are currently inside a package block (exhaleExt does not work for this because it's temporarily set to false e.g. when evaluating pure assertions)
• changes the three places in the code that return Success() when in an infeasible branch s.t. verification continues, possibly with an unknown value if we're reading a field that we don't have permission to

[ArquintL]

Looks good to me; although, I must admit that I don't fully grasp the necessity of optimalSnapshotSort

[marcoeilers]

Looks good to me; although, I must admit that I don't fully grasp the necessity of optimalSnapshotSort

Depending on what is in a predicate, its snapshot has a different sort (e.g. a predicate containing only a permission to an int field will have type int; if it contains multiple values, it'll be type snap). The fix needs us to continue verification when we're in an infeasible state when reading a resource we don't have any chunk of; to do that, we need to return a fresh value of the expected sort.