otherwise, WP->SP adds impossible try-with clauses, and sp_expr
fails when it encounter an unreachable catching clause. Rather
than harden up sp_expr, we prefer to avoid adding dead code,
and so we filter out the context before switching the VCgen.

We also forbid to switch from SP to WP when the code under
the tag has non-empty outcome set. Merely providing an empty
postcondition is wrong, since we do not perform an appropriate
havoc.