// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT fn find_positive(nums: &[i32]) -> Option<i32> { for &num in nums { if num > 0 { return Some(num); } } // This part is unreachable if there is at least one positive number. None } #[kani::proof] fn main() { let numbers = [-3, -1, 0, 2, 4]; let result = find_positive(&numbers); assert_eq!(result, Some(2)); }