CodesInChaos

    #[cfg(kani)]
    #[kani::proof]
    fn verify_success() {
        let x: u32 = kani::any();
        // estimate_size rejects x >= 4096, so this prevents failure from argument verification panicking
        kani::assume(x < 4096);
        let y = estimate_size(x);
        assert!(y < 10);
    }