[prover] fixed_point64::round false positive after Z3 update

[wrwg]

Summary

fixed_point64::round verification produces a spurious counterexample ~3/5 runs. The Boogie encoding is correct — a standalone functional test (tests/sources/functional/fixed_point_round.move) verifies successfully every time.

Analysis

• The round function calls opaque floor() and ceil(). The counterexample claims floor() returns 2 for value = 2^64 + 1, but spec_floor gives 1.
• Generated Boogie is identical between main and the PR branch (only file paths and GlobalId suffixes differ). The spec functions are {:inline}, the assumes are correct.
• The same Boogie input (md5sum identical across runs) produces different Z3 results — sometimes passes, sometimes fails. This is pure Z3 non-determinism.
• ceil() already had pragma verify_duration_estimate = 1000 (effectively disabling verification) due to similar instability, suggesting these fixed-point functions are borderline for Z3.
• This likely regressed with the recent Z3 version update.

Reproduction

# Fails ~3/5 runs:
cargo test -p aptos-framework --test move_prover_tests -- move_aptos_stdlib_prover_tests

# Standalone test always passes:
cargo test -p move-prover -- fixed_point_round

Workaround

pragma verify = false on round with a TODO pointing to this issue. Correctness is covered by the standalone functional test.