Boogie

v3.5.4

Refactor

Boogie

Avoid adding duplicate coverage IDs (#1019)

Previously, if a program element happened to already be labeled with the
label that's auto-generated for another element, Boogie would fail when
adding an already-existing key to the coverage tracking map.

Boogie

Add `/warnVacuousProofs` option (#1016)

This option enables `/trackVerificationCoverage` and automatically warns
if it detects vacuous proofs. This is intended for the less-common case
where a front end doesn't add IDs to program elements and then
post-process the results.

Boogie

v3.5.1

Release version 3.5.1

Boogie

Export hidden functions (#989)

Export hidden functions, used by
https://github.com/dafny-lang/dafny/pull/5929

Boogie

v3.4.2

Provide more flexibility in configuring which return statements get s…

Boogie

Improve short names for splits (#976)

### Changes
Improve short names for splits

### Testing
Updated tests

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.

Boogie

v3.3.3

Revert isolation (#966)

Boogie

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