Environment
- Kani 0.67.0 (cargo plugin), bundle-provided CBMC 6.8.0, built-in CaDiCaL 2.0.0 (
--sat-solver cadical, Kani's default)
- rustc nightly-2025-11-21 (Kani's pinned toolchain)
- ubuntu-24.04 GitHub-hosted runner (16 GB RAM)
- Invocation:
cargo kani --harness <name> --default-unwind 24, run inside a subshell with ulimit -v set (we memory-bound each row of a verification farm)
What happens
Two #[kani::proof] harnesses enumerating u128 edge values (perfect squares +-1 and powers of two +-1, for an integer sqrt) show a failure mode that changes with the address-space limit:
- Under
ulimit -v 6291456 (6 GiB): clean, graceful failure ~36 s in — Out of memory + CBMC failed with status 6. Expected behavior.
- Under
ulimit -v 10485760 (10 GiB): SIGSEGV (CBMC failed with status 139) ~315-342 s in, the last output being:
Post-processing
Runtime Post-process: 0.000947636s
Solving with CaDiCaL 2.0.0
CBMC failed with status 139
VERIFICATION:- FAILED
Reproduced on both harnesses in the same run (342 s and 315 s respectively). The pattern suggests an allocation-failure path reached under VA pressure during SAT solving that is not handled (segfault), while the smaller limit hits a handled path and reports OOM properly. A crash where a graceful OOM is expected matters for anyone memory-bounding CBMC/Kani in CI.
Same surfacing note as the companion SIGFPE report: Kani labels these VERIFICATION:- FAILED, which downstream triage can mistake for a counterexample.
Repro status
Private codebase; the SAT instances are large (u128 bit-blasting at unwind 24). Happy to provide full logs and exact numbers, and to test candidate fixes. A minimized reproducer may be possible with a synthetic u128-heavy harness plus ulimit -v if that helps.
Environment
--sat-solver cadical, Kani's default)cargo kani --harness <name> --default-unwind 24, run inside a subshell withulimit -vset (we memory-bound each row of a verification farm)What happens
Two
#[kani::proof]harnesses enumerating u128 edge values (perfect squares +-1 and powers of two +-1, for an integer sqrt) show a failure mode that changes with the address-space limit:ulimit -v 6291456(6 GiB): clean, graceful failure ~36 s in —Out of memory+CBMC failed with status 6. Expected behavior.ulimit -v 10485760(10 GiB): SIGSEGV (CBMC failed with status 139) ~315-342 s in, the last output being:Reproduced on both harnesses in the same run (342 s and 315 s respectively). The pattern suggests an allocation-failure path reached under VA pressure during SAT solving that is not handled (segfault), while the smaller limit hits a handled path and reports OOM properly. A crash where a graceful OOM is expected matters for anyone memory-bounding CBMC/Kani in CI.
Same surfacing note as the companion SIGFPE report: Kani labels these
VERIFICATION:- FAILED, which downstream triage can mistake for a counterexample.Repro status
Private codebase; the SAT instances are large (u128 bit-blasting at unwind 24). Happy to provide full logs and exact numbers, and to test candidate fixes. A minimized reproducer may be possible with a synthetic u128-heavy harness plus
ulimit -vif that helps.