// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: --mir-linker --enable-unstable
//! Check the basic coercion when using box of box.
//! Tests are broken down into different crates to ensure that the reachability works for each case.

mod defs;
use defs::*;
use std::boxed::Box;

#[kani::proof]
fn check_double_coercion() {
    let id = kani::any();
    let inner: Box<Box<dyn Identity>> = Box::new(Box::new(Inner { id }));
    assert_eq!(inner.id(), id.into());
    assert_eq!(id_from_coerce(*inner), id.into());
}