This will allow one to be able to be able to do permission definendess checks in a different state than the standard evaluation state.

…permission checks

The setDefState field in DefinednessState is now mutable such that when unfolding one can change the definedness state (assuming there is a separate definedness state). An alternative would be to keep the same definedness state during an unfolding statement but to then explicitly reset this state via a Boogie statement at the end of an unfolding. Since Boogie performs constant propagation the resulting VC should essentially be the same for both approaches. The currently implemented approach is more in-line with the way encoding is currently handled, where new states are constructed instead of reusing previous states.

…nedness check)

o special treatment for permission introspection since permission introspection within unfoldings still needs to be explored properly

…inside a package statement

…nedness state. As a result, we can remove the predicate in this state (but do not check whether it is there, because in this mode well-definedness is assumed; analogous to inhale).

…ements

… exhale

this check should not be required, but I add it as a sanity check

…state if the exhale is non-empty