Atomic assignments now pogged as a whole

This fixes an issue with generating state invariant obligations
for atomic assignments (reported for Symphony).
Iterate through entire ctxt stack when popping.