Boogie

Replace AddAssignedVariables with AddAssignedIdentifiers (#945)

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

Boogie

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)

Boogie

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

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

Boogie

[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>

Boogie

Refactoring related to https://github.com/boogie-org/boogie/pull/891 …

…(#898)

Process comments from https://github.com/boogie-org/boogie/pull/891

Boogie

Remove code that causes memory leaks (#888)

### Changes
- Replace two usages of `ConcurrentBag` with `ConcurrentStack`, which
has a much simpler implementation that has no risk of memory leaks.
ConcurrentBag was causing leaks. More information is here:
https://stackoverflow.com/questions/5353164/possible-memoryleak-in-concurrentbag
- Remove cancellation support from AsyncQueue, since the cancellation
token would gain a reference to the item being dequeued, which a caller
might not expect and which causes a memory leak if the cancellation
token is kept alive.
- Add a 'Clear' method to 'AsyncQueue' to allow cancelling all customers
- Fix a surprising memory leak in `CustomStackSizePoolTaskScheduler`
- Enable using an ExecutionEngine with a custom TaskScheduler

### Testing
- Tested with a profiler that the above changes resolve the issue that
each Boogie program created by Dafny was never garbage collected.

Boogie

v3.1.5

Release version 3.1.5

Boogie

Add missing string interpolation (#865)

The fact that we didn't detect this earlier makes it clear that this
functionality wasn't being tested. Unfortunately, it's not immediately
clear to me how to write a test that would exercise the relevant code.

This should fix #863, even though we don't have tests to confirm that.

Boogie

Fix crash on low rlimit (#859)

Z3 has multiple ways of responding that the resource limit has been
exceeded. In some cases it responds with an error message including
"push canceled". This updates Boogie to handle more of the strange side
cases.

Boogie

Reset predecessors before focusing (#856)

There are two calls to `FocusAndSplit` in Boogie. Before one, there was
already a call to `ResetPredecessors`, but not before the other. Now
they both work on an implementation where the `Predecessors` attributes
has been reset.

---------

Co-authored-by: Remy Willems <rwillems@amazon.com>