// Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT #[kani::proof] fn foo() { let x: i32 = kani::any(); if x > 5 { // fails assert!(x < 4); if x < 3 { // unreachable assert!(x == 2); } } else { // passes assert!(x <= 5); } }