diff --git a/examples/verus-snapshot/source/vstd/source/vstd/array.rs b/examples/verus-snapshot/source/vstd/source/vstd/array.rs
index b00f396..ed23646 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/array.rs
+++ b/examples/verus-snapshot/source/vstd/source/vstd/array.rs
@@ -42,6 +42,7 @@ impl<T, const N: usize> ArrayAdditionalExecFns<T> for [T; N] {
 }
 
 #[verifier(external_body)]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_index_get")]
 pub exec fn array_index_get<T, const N: usize>(ar: &[T; N], i: usize) -> (out: &T)
     requires
         0 <= i < N,
@@ -60,7 +61,7 @@ pub broadcast proof fn array_len_matches_n<T, const N: usize>(ar: &[T; N])
 
 // Referenced by Verus' internal encoding for array literals
 #[doc(hidden)]
-#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "vstd::array::array_index")]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_index")]
 pub open spec fn array_index<T, const N: usize>(ar: &[T; N], i: int) -> T {
     ar.view().index(i)
 }
@@ -78,7 +79,7 @@ pub broadcast proof fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
 #[doc(hidden)]
 #[verifier(external_body)]
 #[verifier::when_used_as_spec(spec_array_as_slice)]
-#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "vstd::array::array_as_slice")]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::array::array_as_slice")]
 pub fn array_as_slice<T, const N: usize>(ar: &[T; N]) -> (out: &[T])
     ensures
         ar@ == out@,
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/slice.rs b/examples/verus-snapshot/source/vstd/source/vstd/slice.rs
index 020d77d..960c1b8 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/slice.rs
+++ b/examples/verus-snapshot/source/vstd/source/vstd/slice.rs
@@ -29,6 +29,7 @@ impl<T> SliceAdditionalSpecFns<T> for [T] {
 }
 
 #[verifier(external_body)]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::slice::slice_index_get")]
 pub exec fn slice_index_get<T>(slice: &[T], i: usize) -> (out: &T)
     requires
         0 <= i < slice.view().len(),
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs
index 430b976..4522175 100644
--- a/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs
+++ b/examples/verus-snapshot/source/vstd/source/vstd/std_specs/vec.rs
@@ -66,6 +66,7 @@ impl<T, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A> {
 // be to have users call some function with a nonstandard name to perform indexing.
 /// This is a specification for the indexing operator `vec[i]`
 #[verifier::external_body]
+#[cfg_attr(verus_keep_ghost, rustc_diagnostic_item = "verus::vstd::std_specs::vec::vec_index")]
 pub fn vec_index<T, A: Allocator>(vec: &Vec<T, A>, i: usize) -> (element: &T)
     requires
         i < vec.view().len(),