Environment
- Kani 0.67.0 (cargo plugin), bundle-provided CBMC 6.8.0 (
cbmc-6.8.0, 64-bit x86_64 linux)
- rustc nightly-2025-11-21 (Kani's pinned toolchain)
- ubuntu-24.04 GitHub-hosted runner (16 GB RAM); reproduced on two independent fresh VMs
- Invocation:
cargo kani --harness <name> --default-unwind 24
What happens
A #[kani::proof] harness over a u128 integer-sqrt edge-case check (the harness computes reference values via u128::pow) crashes CBMC with exit status 136 (SIGFPE) early in Bounded Model Checking, right after the unwinding messages for u128::pow:
Starting Bounded Model Checking
Unwinding loop _RNvMs8_NtCs...4core3numo3pow... iteration 1 file .../library/core/src/num/uint_macros.rs line 3347 column 17 function core::num::<impl u128>::pow thread 0
...
Unwinding loop _RNvMs8_NtCs...4core3numo3pow... iteration 6 file .../library/core/src/num/uint_macros.rs line 3347 column 17 function core::num::<impl u128>::pow thread 0
CBMC failed with status 136
VERIFICATION:- FAILED
- Deterministic: reproduced 2/2 on independent fresh VMs, ~22-28 s into the run both times.
- It does not look like memory pressure: it happens seconds in, during symex/unwinding, and other harnesses in the same job run for their full budgets. (A separate, memory-related failure mode is reported independently.)
- Note on surfacing: Kani reports this as
VERIFICATION:- FAILED, which initially mislabeled the crash as a counterexample in our CI triage. A distinct marker for CBMC abnormal exits would help downstream tooling.
Repro status
The codebase is private. Harness shape: #[kani::proof], run with --default-unwind 24, asserting properties of an integer sqrt at u128::MAX and neighbors, computing reference values with u128::pow. Happy to provide full logs and the exact harness source privately, and to work on a minimized standalone reproducer if useful for triage.
Environment
cbmc-6.8.0, 64-bit x86_64 linux)cargo kani --harness <name> --default-unwind 24What happens
A
#[kani::proof]harness over a u128 integer-sqrt edge-case check (the harness computes reference values viau128::pow) crashes CBMC with exit status 136 (SIGFPE) early in Bounded Model Checking, right after the unwinding messages foru128::pow:VERIFICATION:- FAILED, which initially mislabeled the crash as a counterexample in our CI triage. A distinct marker for CBMC abnormal exits would help downstream tooling.Repro status
The codebase is private. Harness shape:
#[kani::proof], run with--default-unwind 24, asserting properties of an integer sqrt atu128::MAXand neighbors, computing reference values withu128::pow. Happy to provide full logs and the exact harness source privately, and to work on a minimized standalone reproducer if useful for triage.