Boogie

Allow `/prune:0` to disable pruning (#848)

Add a `/noprune` flag to turn off pruning. It's off by default, but this
can be convenient if a) it's turned on earlier on the command line, or
b) Boogie is being used from another system like Dafny.

I would have made it `/prune:{1,0}`, but it's harder to make that
backward compatible with the current behavior.

Boogie

Verification task per split (#841)

Dependent Dafny PR: https://github.com/dafny-lang/dafny/pull/5031

### Changes
- Change the API `executionEngine.GetImplementationTasks` to
`executionEngine.GetVerificationTasks`, which returns a task for each
statically defined assertion batch. When using the split on every assert
option, this will return a verification task for each assertion.

### Testing
- Added test SplitOnEveryAssertion

---------

Co-authored-by: Aaron Tomb <[email protected]>

Boogie

v3.0.10

Update Version to 3.0.10 (#837)

Boogie

Don't create trivial labeled assumptions (#823)

Previously, `{:id ...}` attributes were copied from `assert` statements
to `assume` statements unconditionally, even when subsumption was
disabled. This led to `{:id ...}` attributes on `assume true`
statements, which will never be necessary for a proof, so there's no
reason to track them.

Boogie

Fix crashes with verification coverage + counterexamples (#817)

Previously, running Boogie with `/trackVerificationCoverage` and
`/enhancedErrorMessages:1` (or anything that leads to counterexample
parsing) would lead to crashes when verification failed. This fixes that
issue.

Boogie

More thorough checks for exceeding resource limit (#812)

Sometimes Z3 doesn't tell us that it exceeded its resource limit. So, if
it returns "unknown", with an unknown reason, and the reported resource
count exceeds the provided limit, report that it ran out of resources.

Fixes #803.

Addresses dafny-lang/dafny#4804

Boogie

v3.0.6

Bump version number

Boogie

Allow task scheduler parameter to ExecutionEngine (#794)

This allows the creator of an `ExecutionEngine` to pass in a
`CustomStackSizePoolTaskScheduler` so that the scheduler can be shared
between different instantiations of an execution engine. We normally
want only one scheduler per machine, but sometimes want multiple
execution engines.

Boogie

v3.0.4

Update version to 3.0.4 (#783)

Boogie

v3.0.3

Fix silly concurrency bug (#778)