Boogie

Enable marking if commands as {:allow_split} or not (#970)

### Changes
- Introduce the attribute `{:allow_split}` that can be placed on
`IfCmd`. When using `{:isolate "paths"}` only, branches with
`{:allow_split}` will trigger splitting of the VC.

### Testing
- Updated existing tests so they exercise the presence and absence of
`{:allow_split}`
- Added a test that combines `{:vcs_split_on_every_assert}` and explicit
returns.