// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
#[kani::proof]
fn main() {
    let a: u32 = kani::any();

    if a % 3 == 0 {
        assert!(a != 4);
    }

    if a % 3 == 0 {
        assert!(a != 5);
    } else if a % 3 == 1 {
        assert!(a > 0);
    } else {
        assert!(a > 1);
    }
}