Undo revert 966 and add fixes

[keyboardDrummer]

Note: review per commit and skip the first one, since that's an unrevert, so the code was previously reviewed approved and merged.

Changes

• Undo revert Revert isolation #966, which was reverted because it caused unintended Dafny changes
• Change the isolation of returns, so that each ensures clause gets its own VC when {:vcs_split_on_every_assert} is used, so we get #returns * #ensures additional VCs from return statements.
• Change the isolation of returns, so that only explicit return statement are given their own VC branch

Testing

• Added a CLI test that tests the above two changes
• I have checked that updating Dafny to this latest Boogie version only causes expected failures in Dafny tests that can easily be repaired.

[MikaelMayer]

Is it possible that this token could nest another nested token? If that is the case, I would prefer to see a parameter bool ImplicitJump
inside TokenWrapper which should then be a record, to avoid what we experienced in Dafny with unexpected piles of token wrappers that are hard to unfold properly, especially when the order should not matter.
You can then have an extension method method WithImplicit(this IToken token) that, if the token is already wrapped, copy it while setting the implicit flag, and otherwise wrap it with a wrapped token accordingly

[keyboardDrummer]

Great callout. I've changed the check from originalReturn.tok is ImplicitJump to originalReturn.tok is not Token so that any wrapping, which I think indicates it's generated code, will prevent a separate VC from being generated.

I find it hard to say what implementation is the most maintainable here, without having more cases of token wrapping to reason with, so I hope we can leave it at this and stay vigilant.

[robin-aws]

Just reviewed the last two commits, trusted the previous review of the un-revert