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

static mut X: i32 = 12;

fn foo() -> i32 {
    unsafe { X }
}

fn mutate_the_thing(new: i32) {
    unsafe {
        X = new;
    }
}

#[kani::proof]
fn main() {
    if kani::any() {
        assert!(10 == foo());
    }
    assert!(12 == foo());
    mutate_the_thing(10);
    assert!(10 == foo());
    assert!(12 == foo());
}