fix: BigFloat rounding overflow handling in FromRational (#1043)

### Summary
This PR fixes a bug where `FromRational` didn't handle the case where
IEEE 754 rounding causes the significand to grow from n bits to n+1
bits.

### Bug Fixed
When converting rationals to floating-point, if the significand after
shifting was all 1s and needed to round up, it would overflow to a value
with one extra bit (e.g., 53 bits of 1s → 54 bits). `FromRational`
wasn't adjusting for this case, leading to incorrect results. For
example, `2.220446049250313e-16` was incorrectly rounding to 2^(-53)
instead of 2^(-52).

### Changes
- Enhanced `ApplyShiftWithRounding` to return an `overflow` flag
indicating when rounding increases bit length
- Updated `FromRational` to check the overflow flag and adjust the
significand/exponent accordingly
- Updated all other callers of `ApplyShiftWithRounding` to handle the
new return value
- Added test coverage for the rounding overflow scenario

### Testing
All existing tests pass. Added `TestFromRationalRoundingOverflow` to
specifically test this bug.

Refactor

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.

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.

Release version 3.5.1

Export hidden functions (#989)

Export hidden functions, used by
dafny-lang/dafny#5929

Provide more flexibility in configuring which return statements get s…

…eparate VCs with isolate_assertions (#979)

### Changes
Enable isolate_assertions to include explicit return statement in Daf…ny
programs

Improve short names for splits (#976)

### Changes
Improve short names for splits

### Testing
Updated tests

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.

Revert isolation (#966)