Add --isolate-paths option

[keyboardDrummer]

Add an --isolate-paths option that can be set globally or at the verifiable symbol level (method/function/..)

When this option is set, at least one VC is generated per path.

We should enable Dafny developers to code in a way that allows a many to one relation for paths and assertions. This way, using --isolate-assertions would, when already using --isolate-paths, not introduce additional VCs. Using --isolate-assertions is important for guidance type features like #5261

Enable the many to one relation should be helped by:

• Isolating implicit assertions is part of that: Isolate all implicit assertions #5689
• We could also add a 'check' statement, this is like an assert nested in an opaque block.

The cost of using --isolate-paths can be reduced using opaque blocks: #5687

When combined with --isolate-assertions, this may produce a lot of VCs, so that's not recommended.

It's OK if this option can not be combined with {:split_here} and {:focus}