[acearyanarun]

Problem

kani autoharness / cargo kani autoharness set a default loop-unwinding bound of 20 and a harness timeout of 60s so that automatic harnesses don't hang. KaniSession::add_default_bounds did this by writing into the session-wide VerificationArgs (args.default_unwind and args.harness_timeout). Every harness verified in the run reads those fields. That includes the manual #[kani::proof] / #[kani::proof_for_contract] harnesses, which autoharness also verifies:

• resolve_unwind_value resolves --unwind > #[kani::unwind] > --default-unwind. A manual harness without #[kani::unwind] therefore got --unwind 20. A manual harness whose loops need more than 20 iterations passes under cargo kani but fails with unwinding assertion loop N under cargo kani autoharness. This is the hifitime kani_harness_Epoch_now failure from cargo kani autoharness's default --default-unwind 20 silently applies to pre-existing manual harnesses too, causing spurious failures #5103. --include-pattern does not help, because it only selects which functions get automatic harnesses, and manual harnesses always run.
• The timeout has the same problem. run_cbmc_piped and run_terminal_timeout read args.harness_timeout, so every manual harness in an autoharness run was killed after 60s, even though cargo kani sets no timeout by default. A slow but correct manual harness was reported as a timeout failure.

Change

The autoharness defaults now live in two new KaniSession fields, autoharness_default_unwind and autoharness_harness_timeout, and no longer go into VerificationArgs. They are applied per harness, only when HarnessMetadata::is_automatically_generated is set:

• resolve_unwind_value(args, harness, autoharness_default_unwind) keeps the existing precedence and adds the autoharness default as the last fallback, for automatic harnesses only: --unwind > #[kani::unwind] > --default-unwind > autoharness default.
• The new resolve_harness_timeout(args, harness, autoharness_harness_timeout) returns --harness-timeout if passed. Otherwise it returns the autoharness default for automatic harnesses only. run_cbmc resolves the timeout once and passes it to run_cbmc_piped / run_terminal_timeout.

Existing behavior is preserved where it should be:

• An explicit --unwind, --default-unwind or --harness-timeout still applies to every harness, manual or automatic, exactly as before.
• A manual harness's #[kani::unwind] still beats --default-unwind.
• Automatic harnesses still get 20 / 60s by default. Since they never carry #[kani::unwind], their resolved bound is the same as before in every case.

I checked the other readers of these values:

• warn_if_bounds_reach_unwind is about automatic harnesses' bounded arguments, so it now takes the autoharness default into account explicitly. It warns in exactly the same cases as before.
• --export-json: resolved_unwind goes through resolve_unwind_value. It now reports 20 for automatic harnesses (unchanged) and the true bound for manual ones (previously a misreported 20). The run-level harness_timeout_s still reports 60 for an autoharness run without --harness-timeout, as before. That value describes the automatic harnesses; manual harnesses in such a run now have no timeout.
• The --unwind-in---cbmc-args conflict check (natives_unwind) runs during argument validation, before add_default_bounds, so it never saw the injected 20 and is unaffected.

User-facing text: the autoharness failure note now reads "sets default --harness-timeout of 60s and --default-unwind of 20 for automatic harnesses". The six .expected files containing it are updated to match. In the autoharness reference page, the "Default settings" section now says that both defaults apply only to automatic harnesses, and that explicit options still apply to every harness.

On the timeout, I chose to scope it rather than leave it global. It is the same bug: a manual harness's result in an autoharness run should match its result under cargo kani, and a hidden 60s cap breaks that just as much as a hidden unwind bound does. Keeping it global would also leave the two defaults inconsistent with each other and with the summary note.

Testing

New script-based test tests/script-based-pre/cargo_autoharness_default_bounds_scope. The crate has two functions that get automatic harnesses (loops of 10 and 30 iterations) and three manual harnesses: a 30-iteration loop with no #[kani::unwind], one with #[kani::unwind(31)], and one with #[kani::unwind(5)]. The script runs autoharness three times and checks each harness's verdict:

• Defaults (--include-pattern 'loop_', mirroring the issue). The manual harness without an unwind attribute passes. The automatic 30-iteration harness still fails under the default of 20, and the 10-iteration one passes. #[kani::unwind(31)] passes and #[kani::unwind(5)] fails, so the attribute still wins.
• --default-unwind 10. Applies to manual and automatic harnesses alike: the manual unattributed harness and the automatic 10-iteration harness now fail. The attributes still win.
• --default-unwind 40. Overrides the autoharness default for automatic harnesses: the automatic 30-iteration harness now passes.

--unwind requires --harness, and --harness never selects automatic harnesses, so --unwind is covered by the unit tests below rather than by the script.

New unit tests:

• call_cbmc::tests::autoharness_default_unwind_is_scoped_to_automatic_harnesses: the full precedence matrix for manual and automatic harnesses, with and without the autoharness default, including --unwind and --default-unwind.
• call_cbmc::tests::autoharness_timeout_is_scoped_to_automatic_harnesses: the same for --harness-timeout.
• frontend::schema_utils::tests::resolve_effective_unwind_tests::autoharness_default_unwind_is_reported_for_automatic_harnesses_only: the --export-json resolved_unwind.

Existing resolve_unwind_value / resolve_effective_unwind tests are updated for the new parameter.

Results

Run on macOS with the pinned toolchain (nightly-2026-10-23), with the change on top of e8afed3. Rebasing onto the current main changed only docs/src/reference/experimental/autoharness.md, which conflicted with the restructured page from #4991. The code and tests are identical to what was run. On the rebased branch, cargo test -p kani-driver (211 passed), cargo clippy -p kani-driver --tests -- -D warnings and cargo fmt --check -p kani-driver were re-run with stable Rust and passed.

• cargo build-dev: passed.
• cargo test -p kani-driver: 211 passed, including the three new unit tests.
• compiletest --suite script-based-pre --mode exec cargo_autoharness_default_bounds_scope (the new test): passed.
• Existing suites, all passed:
  • script-based-pre autoharness: 43 tests, including the new test and five of the six tests whose .expected note was reworded;
  • script-based-pre autoderive: 2 tests, including autoderive_arbitrary_enums, the sixth;
  • json-handler: 7 tests.
• ./scripts/kani-fmt.sh --check, cargo clippy --workspace --tests -- -D warnings and RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings: passed.
• Interaction with Autoharness: report bounded Rc/Arc reference-count models #5070, which also changes autoharness output: the code merges without conflicts. On a local merge of the two branches, cargo test -p kani-driver passes (217 tests), as do the script-based-pre autoharness and json-handler suites.

Not run: the full ./scripts/kani-regression.sh and Linux. Both are left to CI. The timeout scoping is covered by the unit test only. An integration test would need a harness that runs for more than 60 s.

Fixes #5103

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[acearyanarun]

@Tianshu-Huang @srivatsansamraj @CYJ904 @wodex1nhaoIeng Please take a look and review when you have the chance

[Copilot]

Warning

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Copilot review overview

1 open issue

• echo \"$output\" prints the full (and potentially nondeterministic/verbose) autoharness output in… · New

What changed in this PR

This PR fixes kani autoharness default bounds leaking into manual harness verification by scoping the autoharness-only defaults (unwind bound and harness timeout) to automatically generated harnesses, restoring parity with cargo kani for manual #[kani::proof] harnesses.

Changes:

• Move autoharness default unwind/timeout from VerificationArgs into per-session autoharness-only fields and resolve them per harness based on is_automatically_generated.
• Update CBMC invocation and JSON export to use the scoped timeout/unwind resolution.
• Add a new script-based regression test plus update documentation and existing .expected outputs to reflect the new user-facing wording.

File	Description
tests/​script-based-pre/​cargo_autoharness_type_invariant/​type-invariant.expected	Updates the autoharness default-bounds note to clarify it applies only to automatic harnesses.
tests/​script-based-pre/​cargo_autoharness_termination_unwind/​termination_unwind.expected	Same note update for termination/unwind fixture output.
tests/​script-based-pre/​cargo_autoharness_termination_timeout/​termination_timeout.expected	Same note update for termination/timeout fixture output.
tests/​script-based-pre/​cargo_autoharness_harnesses_fail/​harnesses_fail.expected	Same note update for failing-harnesses fixture output.
tests/​script-based-pre/​cargo_autoharness_contracts/​contracts.expected	Same note update for contracts fixture output.
tests/​script-based-pre/​autoderive_arbitrary_enums/​enums.expected	Same note update for autoderive fixture output.
tests/​script-based-pre/​cargo_autoharness_default_bounds_scope/​src/​lib.rs	New regression test crate exercising scoped default unwind behavior across manual vs automatic harnesses.
tests/​script-based-pre/​cargo_autoharness_default_bounds_scope/​default_bounds_scope.sh	New script test driver that runs autoharness with varying unwind settings and prints normalized per-harness results.
tests/​script-based-pre/​cargo_autoharness_default_bounds_scope/​default_bounds_scope.expected	Expected normalized per-harness outcomes for the new regression script.
tests/​script-based-pre/​cargo_autoharness_default_bounds_scope/​config.yml	Registers the new script-based test.
tests/​script-based-pre/​cargo_autoharness_default_bounds_scope/​Cargo.toml	New test crate manifest.
kani-driver/​src/​session.rs	Adds autoharness-only default unwind/timeout fields and makes terminal timeout execution accept a per-call timeout.
kani-driver/​src/​frontend/​schema_utils.rs	Plumbs autoharness default unwind/timeout into effective unwind resolution and JSON export reporting.
kani-driver/​src/​call_cbmc.rs	Resolves timeout/unwind per harness (scoped to automatic harnesses) and passes timeout explicitly to CBMC runners; adds unit tests.
kani-driver/​src/​autoharness/​mod.rs	Updates default-bounds handling to set autoharness-only defaults, updates warnings logic, and adjusts summary note wording.
docs/​src/​reference/​experimental/​autoharness.md	Documents that the 60s timeout and unwind=20 defaults apply only to automatic harnesses (unless overridden explicitly).

_{Review effort: Lite}

[feliperodri]

Thanks. The scoping is right: manual harnesses now resolve unwind and timeout the way cargo kani does, and the precedence is documented and tested.

Please address the Copilot point: default_bounds_scope.sh echoes the full autoharness output, which makes the test noisy. Keep only the normalized [label] result: lines.

Also check the four changed .expected files still reflect only the intended change, and re-run the three cancelled macOS jobs.