// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

//! This test checks that Kani works when the target directory is a symlink,
//! which wasn't working previously (see
//! https://github.com/model-checking/kani/issues/2303)

#[kani::proof]
fn main() {
    let x: i32 = kani::any();
    let y: i32 = kani::any();
    kani::assume(y == 0);
    assert_eq!(x + y, x);
}