the trait core::kani::BoundedArbitrary is not implemented for vec::Vec<i32>

[Timmmm]

Hi, if I try to verify this on its own with cargo kani it works fine:

#[cfg(kani)]
#[kani::proof]
#[kani::unwind(17)]
pub fn verify_pop() {
    let mut vect: Vec<i32> = kani::bounded_any::<_, 16>();

    let original_len = vect.len();
    let original_vec = vect.clone();

    if original_vec.is_empty() {
        assert_eq!(vect.pop(), None);
        assert_eq!(vect, original_vec);
    } else {
        assert_eq!(vect.pop().unwrap(), *original_vec.last().unwrap());
        assert_eq!(vect.len(), original_len - 1);

        // Check that all other unaffected elements remain unchanged
        let k = kani::any_where(|&x: &usize| x < original_len - 1);
        assert!(vect[k] == original_vec[k]);
    }
}

However if I put it in library/alloc/src/vec/mod.rs in this repo and run ./scripts/run-kani.sh --path . --kani-args --harness verify_pop --output-format=terse I get this error:

error[E0277]: the trait bound `vec::Vec<i32>: core::kani::BoundedArbitrary` is not satisfied
    --> /home/tim/workspace/verify-rust-std/library/alloc/src/vec/mod.rs:4368:54
     |
4368 |         let mut vect: Vec<i32> = kani::bounded_any::<_, 16>();
     |                                                      ^ unsatisfied trait bound
     |
help: the trait `core::kani::BoundedArbitrary` is not implemented for `vec::Vec<i32>`
    --> /home/tim/workspace/verify-rust-std/library/alloc/src/vec/mod.rs:434:1
     |
 434 | pub struct Vec<T, #[unstable(feature = "allocator_api", issue = "32838")] A: Allocator = Global> {
     | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
     = help: the following other types implement trait `core::kani::BoundedArbitrary`:
               core::option::Option<T>
               core::result::Result<T, E>
note: required by a bound in `core::kani::bounded_any`
    --> /home/tim/workspace/verify-rust-std/library/core/src/lib.rs:388:1
     |
 388 | kani_core::kani_lib!(core);
     | ^^^^^^^^^^^^^^^^^^^^^^^^^^ required by this bound in `bounded_any`
     = note: this error originates in the macro `kani_core::kani_intrinsics` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)

Any idea why?