I tried this code:

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

#![feature(ptr_metadata)]

use std::ptr::NonNull;

#[derive(kani::Arbitrary)]
struct Wrapper<T: ?Sized>(usize, T);

#[cfg(kani)]
#[kani::proof]
fn main() {
    // Create a SampleTrait object from SampleStruct
    let original: Wrapper<[u8; 10]> = kani::any();
    let slice: &Wrapper<[u8]> = &original;

    // Get the raw data pointer and metadata for the trait object
    let slice_ptr = NonNull::new(slice as *const _ as *mut ()).unwrap();
    let metadata = std::ptr::metadata(slice);

    // Create NonNull<dyn SampleTrait> from the data pointer and metadata
    let nonnull: NonNull<Wrapper<[u8]>> =
        NonNull::from_raw_parts(slice_ptr, metadata);

}

using the following command line invocation:

kani slice_tail.rs

with Kani version: 0.56.0

I expected to see this happen: verification succeed

Instead, this happened: Kani compiler crashed

$ kani adt_slice.rs 
Kani Rust Verifier 0.56.0 (standalone)
thread 'rustc' panicked at /tmp/workspace/kani-project/kani/cprover_bindings/src/goto_program/expr.rs:733:9:
Can't apply .member operation to
	Expr { value: Symbol { identifier: "_RINvNtNtCsfIIKBCXq9GN_4core3ptr8metadata18from_raw_parts_mutINtCsgncW3vUYF2n_9adt_slice7WrapperShEuEBZ_::1::var_2::metadata" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }
	_vtable_ptr
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::ptr::from_raw_parts_mut::<Wrapper<[u8]>, ()>
_RINvNtNtCsfIIKBCXq9GN_4core3ptr8metadata18from_raw_parts_mutINtCsgncW3vUYF2n_9adt_slice7WrapperShEuEBZ_
[Kani] current codegen location: Loc { file: "/tmp/.rustup/toolchains/nightly-2024-10-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/metadata.rs", function: None, start_line: 125, start_col: Some(1), end_line: 128, end_col: Some(12), pragmas: [] }
warning: 2 warnings emitted

error: /tmp/workspace/kani-project/kani/target/kani/bin/kani-compiler exited with status exit status: 101