From 494b8040e5a8f9fa340007b15162ba6e2374a742 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 Feb 2026 13:29:19 +0000 Subject: [PATCH] Fix incorrect kani::index example in loop-contracts documentation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The existing example intended to demonstrate how `kani::index` works with loop invariants, but had a mismatch between the invariant and the loop body: - The loop invariant used `sum <= (kani::index as u32 * 20)` suggesting that array element values (each ≤ 20) were being summed - However, the loop body was adding `i` (the index) instead of `*j` (the array element value) - The use of `enumerate()` was also unnecessary for the example's purpose Co-authored-by: Alex Bagnall Resolves: #4534 --- docs/src/reference/experimental/loop-contracts.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index c757195011ca..b37ae6c10332 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -181,8 +181,8 @@ fn forloop() { let a: [u8; 10] = kani::any(); kani::assume(kani::forall!(|i in (0,10)| a[i] <= 20)); #[kani::loop_invariant(sum <= (kani::index as u32 * 20) )] - for (i, j) in a.iter().enumerate() { - sum = sum + (i as u32) ; + for x in a { + sum = sum + x as u32; } assert!(sum <= 200); }