Revert isolation (#966)

No cache (#964)

### Changes
- Enable not using a verification result cache, using the new class
`EmptyVerificationResultCache`

### Testing
- Manually tried out using EmptyVerificationResultCache in Dafny, which
reduces memory pressure

Release 3.3.1 (#962)

Introduce `{:isolate}` and `{:isolate "paths"}` attributes for assert…

… and return commands (#952)

### Changes
- Introduce the `{:isolate}` attribute on AssertCmd and `ReturnCmd`
- Introduce the `{:isolate "paths"}` attribute on AssertCmd and
`ReturnCmd`
- Introduce new tokens that allow precisely describing where a
particular Split comes from.
- Fix a bug that caused too many VCs to be created when using
`/vcsSplitOnEveryAssert` together with focus
- Fix incorrect token bug for VCs originating from focus.

### Testing
- Created a folder `Test/implementationDivision` that has tests for
`{:isolate}`, `{:isolate "paths"}`, `{:focus}` and `{:split_here}`

---------

Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>

Replace AddAssignedVariables with AddAssignedIdentifiers (#945)

Replace AddAssignedVariables with AddAssignedIdentifiers, because the
latter can already be computed before resolution, which is useful for
Dafny.

Optimize blocks (#919)

### Changes

1. Perform block coalescing for each split
2. Add a post-split simplification that removes empty blocks with at
most one outgoing or incoming edge

### Testing
- Updated the test `AssumeFalseSplit.bpl` to take into account
simplification (2)

[Civl] Add support for skip async calls (#923)

Co-authored-by: Shaz Qadeer <shaz@meta.com>

[Civl] Added explicit gates to atomic actions (#911)

This PR allows gates of atomic actions to be explicitly specified. The
convention is as follows:

var {:layer 0,1} x: int;

yield invariant YieldInv();
invariant ...

atomic action Foo()
requires x > 0; // gate (must be sufficient to prove absence of failures
in atomic action)
requires call YieldInv(); // precondition used only in special
circumstances
{
   assert x != 0;
}

---------

Co-authored-by: Shaz Qadeer <shaz@meta.com>

[Civl] Added explicit gates to atomic actions (#911)

This PR allows gates of atomic actions to be explicitly specified. The
convention is as follows:

var {:layer 0,1} x: int;

yield invariant YieldInv();
invariant ...

atomic action Foo()
requires x > 0; // gate (must be sufficient to prove absence of failures
in atomic action)
requires call YieldInv(); // precondition used only in special
circumstances
{
   assert x != 0;
}

---------

Co-authored-by: Shaz Qadeer <shaz@meta.com>

Refactoring related to #891 (#898)

Process comments from #891