clean up postcondition framedness check

[gauravpartha]

The method postcondition is checked to be properly framed in a fresh state as follows:

inhale precondition
PostMask := Mask;
PostHeap := Heap;
havoc PostHeap;
PostMask := ZeroMask
 if(*) {
   check postcondition framed in (PostHeap, PostMask)
   assume false;
}
translate main body of method
exhale postcondition

The initial assignments to PostMask and PostHeap are superfluous. Moreover, the post state setup is only relevant inside the then-branch of the non-deterministic if statement. This PR makes this explicit by changing the encoding to:

inhale precondition
 if(*) {
   havoc PostHeap;
   PostMask := ZeroMask;
   check postcondition framed in (PostHeap, PostMask)
   assume false;
}
translate main body of method
exhale postcondition