#![feature(iter_advance_by)]

use std::iter::DoubleEndedIterator;

fn addr() -> usize {
    let addr = kani::any_where::<usize, _>(|val| *val == 9223372036854775809);
    // ***** Uncomment the line below to make the harness pass. ******
    // let addr =  9223372036854775809;
    assert_eq!(addr, 9223372036854775809);
    addr
}

fn any_slice(orig_slice: &[u8]) -> &[u8] {
    let ptr = addr() as *const u8;
    unsafe { core::slice::from_raw_parts(ptr, 0) }
}

mod verify_u8 {
    use super::*;
    const MAX_LEN: usize = 1;

    #[kanitool::proof]
    fn check_nth_back() {
        let array = [0u8; 0];
        let slice = any_slice(&array);
        assert!(slice.is_empty());
        let mut iter = slice.iter();
        let _ = iter.advance_by(kani::any());
    }
}