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

//! This test is used to test playback command on a unit test generated by the concrete playback.

#[cfg(kani)]
mod verify {
    #[kani::proof]
    fn cover_lib() {
        kani::cover!(kani::any::<u8>() == 200u8);
    }

    #[test]
    fn kani_concrete_playback_cover_lib_1234() {
        let concrete_vals: Vec<Vec<u8>> = vec![
            // 10
            vec![200],
        ];
        kani::concrete_playback_run(concrete_vals, cover_lib);
    }
}