// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT fn find_index(nums: &[i32], target: i32) -> Option<usize> { for (index, &num) in nums.iter().enumerate() { if num == target { return Some(index); } } None } #[kani::proof] fn main() { let numbers = [10, 20, 30, 40, 50]; let target = 30; let result = find_index(&numbers, target); assert_eq!(result, Some(2)); }