[r-near]

__VERIFIER_kani_{enter,exit}_contract_clause aren't instrumented by DFCC but called saturating_add/saturating_sub, which are, so every proof_for_contract harness printed CBMC's "not enough arguments" warning. This replaces the calls with a bounds-checked + 1/- 1. The two capture_load_* check counts go up by 2 for the new overflow checks.

Adds tests/script-based-pre/contract_clause_write_set, which fails before this change.

Related to #4796

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

[Copilot]

🟢 Approval recommended

No active review issues are recorded for the contract-clause depth helper changes.

No open issues 🎉

What changed in this PR

This PR removes saturating method calls from Kani’s contract-clause depth helpers to avoid CBMC’s “not enough arguments” warning during function-contract verification. It addresses a related helper issue, not the broader loop-invariant method-call problem in #4796.

Changes:

• Replace saturating calls with bounds-checked arithmetic, preserving saturation behavior.
• Add a regression test requiring successful verification without missing-argument warnings.
• Update two expected check counts for the added overflow checks.

File	Description
library/​kani_core/​src/​lib.rs	Use guarded increments and decrements for contract-clause depth.
tests/​script-based-pre/​contract_clause_write_set/​write_set.sh	Check verification succeeds without missing-argument warnings.
tests/​script-based-pre/​contract_clause_write_set/​write_set.expected	Define the regression test’s success output.
tests/​script-based-pre/​contract_clause_write_set/​fixture.rs	Provide a function-contract proof fixture.
tests/​script-based-pre/​contract_clause_write_set/​config.yml	Register the regression script and expected output.
tests/​expected/​function-contract/​capture_load_user_deref_pass.expected	Increase the expected check count from 58 to 60.
tests/​expected/​function-contract/​capture_load_checks_elided.expected	Increase the expected check count from 34 to 36.

_{Review effort: Balanced}