diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml
index 7187865e6..49c3a11ed 100644
--- a/charon-ml/src/generated/Generated_GAst.ml
+++ b/charon-ml/src/generated/Generated_GAst.ml
@@ -431,15 +431,21 @@ type cli_options = {
           break this mutual recursion. *)
   precise_drops : bool;
       (** Whether to precisely translate drops and drop-related code. For this,
-          we add explicit [Destruct] bounds to all generic parameters, and set
-          the MIR level to at least [elaborated].
+          we add explicit [Destruct] bounds to all generic parameters, set the
+          MIR level to at least [elaborated], and attempt to retrieve drop glue
+          for all types.
+
+          This option is known to cause panics inside rustc, because their drop
+          handling is not design to work on polymorphic types. To silence the
+          warning, pass appropriate
+          [--opaque '{impl core::marker::Destruct for some::Type}'] options.
 
           Without this option, drops may be "conditional" and we may lack
           information about what code is run on drop in a given polymorphic
           function body. *)
   desugar_drops : bool;
-      (** If activated, transform [Drop(p)] to [Call drop_in_place(&raw mut p)].
-      *)
+      (** Transform precise drops to the equivalent [drop_in_place(&raw mut p)]
+          call. *)
   start_from : string list;
       (** A list of item paths to use as starting points for the translation. We
           will translate these items and any items they refer to, according to
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index 0af7f2054..17940dbad 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -836,7 +836,7 @@ dependencies = [
 [[package]]
 name = "hax-adt-into"
 version = "0.3.5"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#665a80bc5ad21cafb5081df336192ec0de62b9f5"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#5f86b92040418d3f025c2c274ecaf8f4a66016b5"
 dependencies = [
  "itertools 0.11.0",
  "proc-macro2",
@@ -847,7 +847,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter"
 version = "0.3.5"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#665a80bc5ad21cafb5081df336192ec0de62b9f5"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#5f86b92040418d3f025c2c274ecaf8f4a66016b5"
 dependencies = [
  "extension-traits",
  "hax-adt-into",
@@ -864,7 +864,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter-options"
 version = "0.3.5"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#665a80bc5ad21cafb5081df336192ec0de62b9f5"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#5f86b92040418d3f025c2c274ecaf8f4a66016b5"
 dependencies = [
  "hax-adt-into",
  "schemars",
diff --git a/charon/src/bin/charon-driver/translate/translate_drops.rs b/charon/src/bin/charon-driver/translate/translate_drops.rs
index b014511ac..2b3ae6e45 100644
--- a/charon/src/bin/charon-driver/translate/translate_drops.rs
+++ b/charon/src/bin/charon-driver/translate/translate_drops.rs
@@ -1,7 +1,7 @@
 use crate::translate::translate_crate::TransItemSourceKind;
 
 use super::translate_ctx::*;
-use charon_lib::ast::*;
+use charon_lib::{ast::*, formatter::IntoFormatter, pretty::FmtWithCtx};
 use hax::FullDefKind;
 
 impl ItemTransCtx<'_, '_> {
@@ -9,14 +9,46 @@ impl ItemTransCtx<'_, '_> {
         &mut self,
         span: Span,
         def: &hax::FullDef,
+        self_ty: &Ty,
     ) -> Result<Body, Error> {
         let (hax::FullDefKind::Adt { drop_glue, .. } | hax::FullDefKind::Closure { drop_glue, .. }) =
             def.kind()
         else {
-            return Ok(Body::Opaque);
+            return Ok(Body::Missing);
         };
-        let Some(body) = drop_glue else {
-            return Ok(Body::Opaque);
+
+        let tmp_body;
+        let body = match drop_glue {
+            Some(body) => body,
+            None if self.options.translate_poly_drop_glue => {
+                let ctx = std::panic::AssertUnwindSafe(&mut *self);
+                // This is likely to panic, see the docs of `--precise-drops`.
+                let Ok(body) =
+                    std::panic::catch_unwind(move || def.this().drop_glue_shim(ctx.hax_state()))
+                else {
+                    let self_ty_name = if let TyKind::Adt(TypeDeclRef {
+                        id: TypeId::Adt(type_id),
+                        ..
+                    }) = self_ty.kind()
+                        && let Some(name) = self.translated.item_name(*type_id)
+                    {
+                        name.to_string_with_ctx(&self.into_fmt())
+                    } else {
+                        "crate::the::Type".to_string()
+                    };
+                    raise_error!(
+                        self,
+                        span,
+                        "rustc panicked while retrieving drop glue. \
+                        This is known to happen with `--precise-drops`; to silence this warning, \
+                        pass `--opaque '{{impl core::marker::Destruct for {}}}'` to charon",
+                        self_ty_name
+                    )
+                };
+                tmp_body = body;
+                &tmp_body
+            }
+            None => return Ok(Body::Missing),
         };
 
         Ok(self.translate_body(span, body, &def.source_text))
@@ -82,7 +114,7 @@ impl ItemTransCtx<'_, '_> {
         let body = if item_meta.opacity.with_private_contents().is_opaque() {
             Body::Opaque
         } else {
-            self.translate_drop_in_place_method_body(span, def)?
+            self.translate_drop_in_place_method_body(span, def, &self_ty)?
         };
 
         let input = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
diff --git a/charon/src/options.rs b/charon/src/options.rs
index 3998fad2e..137a30398 100644
--- a/charon/src/options.rs
+++ b/charon/src/options.rs
@@ -180,15 +180,19 @@ pub struct CliOpts {
     #[serde(default)]
     pub remove_unused_self_clauses: bool,
     /// Whether to precisely translate drops and drop-related code. For this, we add explicit
-    /// `Destruct` bounds to all generic parameters, and set the MIR level to at least
-    /// `elaborated`.
+    /// `Destruct` bounds to all generic parameters, set the MIR level to at least `elaborated`,
+    /// and attempt to retrieve drop glue for all types.
+    ///
+    /// This option is known to cause panics inside rustc, because their drop handling is not
+    /// design to work on polymorphic types. To silence the warning, pass appropriate `--opaque
+    /// '{impl core::marker::Destruct for some::Type}'` options.
     ///
     /// Without this option, drops may be "conditional" and we may lack information about what code
     /// is run on drop in a given polymorphic function body.
     #[clap(long)]
     #[serde(default)]
     pub precise_drops: bool,
-    /// If activated, transform `Drop(p)` to `Call drop_in_place(&raw mut p)`.
+    /// Transform precise drops to the equivalent `drop_in_place(&raw mut p)` call.
     #[clap(long)]
     #[serde(default)]
     pub desugar_drops: bool,
@@ -490,7 +494,10 @@ pub struct TranslateOptions {
     pub remove_associated_types: Vec<NamePattern>,
     /// Transform Drop to Call drop_in_place
     pub desugar_drops: bool,
+    /// Add `Destruct` bounds to all generic params.
     pub add_destruct_bounds: bool,
+    /// Translate drop glue for poly types, knowing that this may cause ICEs.
+    pub translate_poly_drop_glue: bool,
 }
 
 impl TranslateOptions {
@@ -575,8 +582,9 @@ impl TranslateOptions {
             raw_boxes: options.raw_boxes,
             remove_associated_types,
             translate_all_methods: options.translate_all_methods,
-            add_destruct_bounds: options.precise_drops,
             desugar_drops: options.desugar_drops,
+            add_destruct_bounds: options.precise_drops,
+            translate_poly_drop_glue: options.precise_drops,
         }
     }
 
diff --git a/charon/tests/help-output.txt b/charon/tests/help-output.txt
index 48fefbdba..33d779517 100644
--- a/charon/tests/help-output.txt
+++ b/charon/tests/help-output.txt
@@ -112,12 +112,14 @@ Options:
           Trait method declarations take a `Self: Trait` clause as parameter, so that they can be reused by multiple trait impls. This however causes trait definitions to be mutually recursive with their method declarations. This flag removes `Self` clauses that aren't used to break this mutual recursion
 
       --precise-drops
-          Whether to precisely translate drops and drop-related code. For this, we add explicit `Destruct` bounds to all generic parameters, and set the MIR level to at least `elaborated`.
+          Whether to precisely translate drops and drop-related code. For this, we add explicit `Destruct` bounds to all generic parameters, set the MIR level to at least `elaborated`, and attempt to retrieve drop glue for all types.
+          
+          This option is known to cause panics inside rustc, because their drop handling is not design to work on polymorphic types. To silence the warning, pass appropriate `--opaque '{impl core::marker::Destruct for some::Type}'` options.
           
           Without this option, drops may be "conditional" and we may lack information about what code is run on drop in a given polymorphic function body.
 
       --desugar-drops
-          If activated, transform `Drop(p)` to `Call drop_in_place(&raw mut p)`
+          Transform precise drops to the equivalent `drop_in_place(&raw mut p)` call
 
       --start-from <START_FROM>
           A list of item paths to use as starting points for the translation. We will translate these items and any items they refer to, according to the opacity rules. When absent, we start from the path `crate` (which translates the whole crate)
diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out
index c8d546a12..000840ec6 100644
--- a/charon/tests/ui/arrays.out
+++ b/charon/tests/ui/arrays.out
@@ -298,7 +298,49 @@ const UNIT_METADATA: () = @Fun0()
 fn {impl Destruct for Array<T, N>}::drop_in_place<T, const N : usize>(@1: *mut Array<T, N>)
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut Array<T, N>; // arg #1
+    let @2: &'_ mut (Array<T, N>); // anonymous local
+    let @3: *mut Array<T, N>; // anonymous local
+    let @4: *mut Slice<T>; // anonymous local
+    let @5: usize; // anonymous local
+    let @6: usize; // anonymous local
+    let @7: *mut T; // anonymous local
+    let @8: bool; // anonymous local
+    let @9: &'_ mut (Slice<T>); // anonymous local
+    let @10: &'_ mut (T); // anonymous local
+
+    storage_live(@2)
+    storage_live(@3)
+    storage_live(@4)
+    storage_live(@5)
+    storage_live(@6)
+    storage_live(@7)
+    storage_live(@8)
+    @0 := ()
+    @2 := &mut *(@1)
+    @3 := &raw mut *(@2)
+    @4 := unsize_cast<*mut Array<T, N>, *mut Slice<T>, N>(move (@3))
+    @5 := copy (@4.metadata)
+    @6 := const (0 : usize)
+    loop {
+        @8 := copy (@6) == copy (@5)
+        if move (@8) {
+            break 0
+        } else {
+            storage_live(@9)
+            @9 := &mut *(@4) with_metadata(copy (@4.metadata))
+            storage_live(@10)
+            @10 := @SliceIndexMut<'_, T>(move (@9), copy (@6))
+            @7 := &raw mut *(@10)
+            @6 := move (@6) wrap.+ const (1 : usize)
+            drop[{built_in impl Destruct for T}] *(@7)
+            continue 0
+        }
+    }
+    return
+}
 
 // Full name: test_crate::<array>::{impl Destruct for Array<T, N>}
 impl<T, const N : usize> Destruct for Array<T, N>
diff --git a/charon/tests/ui/closure-as-fn.out b/charon/tests/ui/closure-as-fn.out
index a7d5951bc..f2e1b3850 100644
--- a/charon/tests/ui/closure-as-fn.out
+++ b/charon/tests/ui/closure-as-fn.out
@@ -129,7 +129,7 @@ fn {impl FnMut<()> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: ())
 
 // Full name: test_crate::main::closure::{impl Destruct for closure}::drop_in_place
 fn {impl Destruct for closure}::drop_in_place(@1: *mut closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::main::closure::{impl Destruct for closure}
 impl Destruct for closure {
diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out
index 6d69ee89c..773ea48be 100644
--- a/charon/tests/ui/closures.out
+++ b/charon/tests/ui/closures.out
@@ -154,7 +154,17 @@ const UNIT_METADATA: () = @Fun0()
 
 // Full name: test_crate::<tuple_1>::{impl Destruct for (A)}::drop_in_place
 fn {impl Destruct for (A)}::drop_in_place<A>(@1: *mut (A))
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut (A); // arg #1
+    let @2: &'_ mut ((A)); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1) with_metadata(copy (@1.metadata))
+    drop[{built_in impl Destruct for A}] (*(@2)).0
+    return
+}
 
 // Full name: test_crate::<tuple_1>::{impl Destruct for (A)}
 impl<A> Destruct for (A) {
@@ -311,7 +321,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_closure_u32::closure}::call_mut<
 
 // Full name: test_crate::test_closure_u32::closure::{impl Destruct for test_crate::test_closure_u32::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_closure_u32::closure}::drop_in_place(@1: *mut test_crate::test_closure_u32::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_u32::closure::{impl Destruct for test_crate::test_closure_u32::closure}
 impl Destruct for test_crate::test_closure_u32::closure {
@@ -451,7 +461,7 @@ fn {impl FnMut<(u32, u32), u32> for test_crate::test_closure_u32s::closure}::cal
 
 // Full name: test_crate::test_closure_u32s::closure::{impl Destruct for test_crate::test_closure_u32s::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_closure_u32s::closure}::drop_in_place(@1: *mut test_crate::test_closure_u32s::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_u32s::closure::{impl Destruct for test_crate::test_closure_u32s::closure}
 impl Destruct for test_crate::test_closure_u32s::closure {
@@ -582,7 +592,7 @@ fn {impl FnMut<(&'_ (u32)), &'_ (u32)> for test_crate::test_closure_ref_u32::clo
 
 // Full name: test_crate::test_closure_ref_u32::closure::{impl Destruct for test_crate::test_closure_ref_u32::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_closure_ref_u32::closure}::drop_in_place(@1: *mut test_crate::test_closure_ref_u32::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_ref_u32::closure::{impl Destruct for test_crate::test_closure_ref_u32::closure}
 impl Destruct for test_crate::test_closure_ref_u32::closure {
@@ -721,7 +731,7 @@ where
 fn {impl Destruct for test_crate::test_closure_ref_param::closure<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut test_crate::test_closure_ref_param::closure<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_ref_param::closure::{impl Destruct for test_crate::test_closure_ref_param::closure<T>[@TraitClause0]}
 impl<T> Destruct for test_crate::test_closure_ref_param::closure<T>[@TraitClause0]
@@ -889,7 +899,7 @@ fn {impl Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Trait<'a, T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_ref_early_bound::closure::{impl Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]}
 impl<'a, T> Destruct for test_crate::test_closure_ref_early_bound::closure<'_, T>[@TraitClause0, @TraitClause1]
@@ -1051,7 +1061,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_map_option2::closure}::call_mut<
 
 // Full name: test_crate::test_map_option2::closure::{impl Destruct for test_crate::test_map_option2::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_map_option2::closure}::drop_in_place(@1: *mut test_crate::test_map_option2::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_map_option2::closure::{impl Destruct for test_crate::test_map_option2::closure}
 impl Destruct for test_crate::test_map_option2::closure {
@@ -1313,7 +1323,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_map_option3::closure}::call_mut<
 
 // Full name: test_crate::test_map_option3::closure::{impl Destruct for test_crate::test_map_option3::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_map_option3::closure}::drop_in_place(@1: *mut test_crate::test_map_option3::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_map_option3::closure::{impl Destruct for test_crate::test_map_option3::closure}
 impl Destruct for test_crate::test_map_option3::closure {
@@ -1446,7 +1456,7 @@ fn {impl FnMut<(&'_ (&'_ (u32))), u32> for test_crate::test_regions::closure}::c
 
 // Full name: test_crate::test_regions::closure::{impl Destruct for test_crate::test_regions::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_regions::closure}::drop_in_place(@1: *mut test_crate::test_regions::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_regions::closure::{impl Destruct for test_crate::test_regions::closure}
 impl Destruct for test_crate::test_regions::closure {
@@ -1531,7 +1541,7 @@ fn {impl FnMut<(&'_ (&'_ (u32))), u32> for test_crate::test_regions_casted::clos
 
 // Full name: test_crate::test_regions_casted::closure::{impl Destruct for test_crate::test_regions_casted::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_regions_casted::closure}::drop_in_place(@1: *mut test_crate::test_regions_casted::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_regions_casted::closure::{impl Destruct for test_crate::test_regions_casted::closure}
 impl Destruct for test_crate::test_regions_casted::closure {
@@ -1721,7 +1731,7 @@ fn {impl FnMut<(u32), u32> for test_crate::test_closure_capture::closure<'_0, '_
 
 // Full name: test_crate::test_closure_capture::closure::{impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}::drop_in_place
 fn {impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}::drop_in_place<'_0, '_1>(@1: *mut test_crate::test_closure_capture::closure<'_0, '_1>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_capture::closure::{impl Destruct for test_crate::test_closure_capture::closure<'_0, '_1>}
 impl<'_0, '_1> Destruct for test_crate::test_closure_capture::closure<'_0, '_1> {
@@ -1859,7 +1869,7 @@ fn {impl Destruct for test_crate::test_closure_clone::closure<T>[@TraitClause0,
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Clone<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_closure_clone::closure::{impl Destruct for test_crate::test_closure_clone::closure<T>[@TraitClause0, @TraitClause1]}
 impl<T> Destruct for test_crate::test_closure_clone::closure<T>[@TraitClause0, @TraitClause1]
@@ -1949,7 +1959,7 @@ fn {impl FnMut<(i32), i32> for test_crate::test_array_map::closure}::call_mut<'_
 
 // Full name: test_crate::test_array_map::closure::{impl Destruct for test_crate::test_array_map::closure}::drop_in_place
 fn {impl Destruct for test_crate::test_array_map::closure}::drop_in_place(@1: *mut test_crate::test_array_map::closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_array_map::closure::{impl Destruct for test_crate::test_array_map::closure}
 impl Destruct for test_crate::test_array_map::closure {
@@ -2090,7 +2100,7 @@ fn test_fnmut_with_ref()
 
 // Full name: test_crate::test_fnmut_with_ref::closure::{impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}::drop_in_place
 fn {impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}::drop_in_place<'_0>(@1: *mut test_crate::test_fnmut_with_ref::closure<'_0>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test_fnmut_with_ref::closure::{impl Destruct for test_crate::test_fnmut_with_ref::closure<'_0>}
 impl<'_0> Destruct for test_crate::test_fnmut_with_ref::closure<'_0> {
diff --git a/charon/tests/ui/closures_with_where.out b/charon/tests/ui/closures_with_where.out
index 21060e780..1c49745df 100644
--- a/charon/tests/ui/closures_with_where.out
+++ b/charon/tests/ui/closures_with_where.out
@@ -132,7 +132,7 @@ fn {impl Destruct for closure<T, K>[@TraitClause0, @TraitClause1]}::drop_in_plac
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Ops<T, K>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::test::closure::{impl Destruct for closure<T, K>[@TraitClause0, @TraitClause1]}
 impl<T, const K : usize> Destruct for closure<T, K>[@TraitClause0, @TraitClause1]
diff --git a/charon/tests/ui/impl-trait.out b/charon/tests/ui/impl-trait.out
index 2a5959141..0f89a1ac3 100644
--- a/charon/tests/ui/impl-trait.out
+++ b/charon/tests/ui/impl-trait.out
@@ -327,7 +327,7 @@ where
 fn {impl Destruct for closure<U>[@TraitClause0]}::drop_in_place<U>(@1: *mut closure<U>[@TraitClause0])
 where
     [@TraitClause0]: Sized<U>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::wrap::closure::{impl Destruct for closure<U>[@TraitClause0]}
 impl<U> Destruct for closure<U>[@TraitClause0]
diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out
index 58f3093e3..f3dbae7e6 100644
--- a/charon/tests/ui/issue-114-opaque-bodies.out
+++ b/charon/tests/ui/issue-114-opaque-bodies.out
@@ -126,7 +126,7 @@ impl From<i32> for i64 {
 pub struct PhantomData<T> {}
 
 fn core::marker::Destruct::drop_in_place<Self>(@1: *mut Self)
-= <opaque>
+= <missing>
 
 // Full name: core::num::niche_types::UsizeNoHighBit
 pub struct UsizeNoHighBit {
diff --git a/charon/tests/ui/issue-114-opaque-bodies.rs b/charon/tests/ui/issue-114-opaque-bodies.rs
index aac5d5372..01173e272 100644
--- a/charon/tests/ui/issue-114-opaque-bodies.rs
+++ b/charon/tests/ui/issue-114-opaque-bodies.rs
@@ -1,4 +1,5 @@
 //@ charon-args=--extract-opaque-bodies
+//@ charon-arg=--opaque={impl core::marker::Destruct for alloc::vec::Vec}
 //@ aux-crate=issue-114-opaque-bodies-aux.rs
 
 fn use_inlines() -> u32 {
diff --git a/charon/tests/ui/issue-120-bare-discriminant-read.out b/charon/tests/ui/issue-120-bare-discriminant-read.out
index 93d0f7a0e..b93545433 100644
--- a/charon/tests/ui/issue-120-bare-discriminant-read.out
+++ b/charon/tests/ui/issue-120-bare-discriminant-read.out
@@ -21,7 +21,7 @@ pub trait Destruct<Self>
 }
 
 fn core::marker::Destruct::drop_in_place<Self>(@1: *mut Self)
-= <opaque>
+= <missing>
 
 // Full name: core::option::Option
 #[lang_item("Option")]
@@ -37,7 +37,7 @@ where
 fn {impl Destruct for Option<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut Option<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: core::option::Option::{impl Destruct for Option<T>[@TraitClause0]}
 impl<T> Destruct for Option<T>[@TraitClause0]
diff --git a/charon/tests/ui/issue-323-closure-borrow.out b/charon/tests/ui/issue-323-closure-borrow.out
index 394cf9ba9..cece37d03 100644
--- a/charon/tests/ui/issue-323-closure-borrow.out
+++ b/charon/tests/ui/issue-323-closure-borrow.out
@@ -136,7 +136,7 @@ fn {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_1>(@1: &'_1 mut (closure<'
 
 // Full name: test_crate::new::closure::{impl Destruct for closure<'_0>}::drop_in_place
 fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::new::closure::{impl Destruct for closure<'_0>}
 impl<'_0> Destruct for closure<'_0> {
diff --git a/charon/tests/ui/issue-394-rpit-with-lifetime.out b/charon/tests/ui/issue-394-rpit-with-lifetime.out
index 63a7a1624..9165b09ef 100644
--- a/charon/tests/ui/issue-394-rpit-with-lifetime.out
+++ b/charon/tests/ui/issue-394-rpit-with-lifetime.out
@@ -116,7 +116,7 @@ fn {impl FnMut<()> for closure<'_>}::call_mut<'a, '_1>(@1: &'_1 mut (closure<'_>
 
 // Full name: test_crate::sparse_transitions::closure::{impl Destruct for closure<'_>}::drop_in_place
 fn {impl Destruct for closure<'_>}::drop_in_place<'a>(@1: *mut closure<'_>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::sparse_transitions::closure::{impl Destruct for closure<'_>}
 impl<'a> Destruct for closure<'_> {
diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out
index f5ab09f19..5c68f48d2 100644
--- a/charon/tests/ui/issue-45-misc.out
+++ b/charon/tests/ui/issue-45-misc.out
@@ -582,7 +582,7 @@ fn {impl FnMut<(i32)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (i
 
 // Full name: test_crate::map::closure::{impl Destruct for closure}::drop_in_place
 fn {impl Destruct for closure}::drop_in_place(@1: *mut closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::map::closure::{impl Destruct for closure}
 impl Destruct for closure {
diff --git a/charon/tests/ui/no_nested_borrows.out b/charon/tests/ui/no_nested_borrows.out
index 6d666aba4..ab5ebc55b 100644
--- a/charon/tests/ui/no_nested_borrows.out
+++ b/charon/tests/ui/no_nested_borrows.out
@@ -145,7 +145,7 @@ where
 fn {impl Destruct for List<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut List<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::List::{impl Destruct for List<T>[@TraitClause0]}
 impl<T> Destruct for List<T>[@TraitClause0]
@@ -260,7 +260,7 @@ where
 fn {impl Destruct for IdType<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut IdType<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::IdType::{impl Destruct for IdType<T>[@TraitClause0]}
 impl<T> Destruct for IdType<T>[@TraitClause0]
diff --git a/charon/tests/ui/raw-boxes.out b/charon/tests/ui/raw-boxes.out
index fe303b621..2eddf110c 100644
--- a/charon/tests/ui/raw-boxes.out
+++ b/charon/tests/ui/raw-boxes.out
@@ -1689,7 +1689,7 @@ where
 }
 
 fn core::marker::Destruct::drop_in_place<Self>(@1: *mut Self)
-= <opaque>
+= <missing>
 
 // Full name: core::num::niche_types::NonZeroUsizeInner
 pub struct NonZeroUsizeInner {
@@ -3262,7 +3262,7 @@ where
     [@TraitClause0]: MetaSized<T>,
     [@TraitClause1]: Sized<A>,
     [@TraitClause2]: Allocator<A>,
-= <opaque>
+= <missing>
 
 // Full name: alloc::boxed::Box::{impl Destruct for Box<T, A>[@TraitClause0, @TraitClause1, @TraitClause2]}
 impl<T, A> Destruct for Box<T, A>[@TraitClause0, @TraitClause1, @TraitClause2]
diff --git a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out
index 96796d1b5..944c810b8 100644
--- a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out
+++ b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out
@@ -173,7 +173,7 @@ fn {impl Destruct for closure<F, Clause1_Repr>[@TraitClause0, @TraitClause1]}::d
 where
     [@TraitClause0]: Sized<F>,
     [@TraitClause1]: PrimeField<F, Clause1_Repr>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::{SqrtTables<F>[@TraitClause0]}::sqrt_common::closure::{impl Destruct for closure<F, Clause1_Repr>[@TraitClause0, @TraitClause1]}
 impl<F, Clause1_Repr> Destruct for closure<F, Clause1_Repr>[@TraitClause0, @TraitClause1]
diff --git a/charon/tests/ui/result-unwrap.out b/charon/tests/ui/result-unwrap.out
index f770e9ea6..07d106ee6 100644
--- a/charon/tests/ui/result-unwrap.out
+++ b/charon/tests/ui/result-unwrap.out
@@ -204,7 +204,7 @@ pub trait Destruct<Self>
 
 // Full name: core::marker::Destruct::drop_in_place
 fn drop_in_place<Self>(@1: *mut Self)
-= <opaque>
+= <missing>
 
 fn UNIT_METADATA()
 {
diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out
index c80aebc26..8f00a4799 100644
--- a/charon/tests/ui/rvalues.out
+++ b/charon/tests/ui/rvalues.out
@@ -452,7 +452,7 @@ fn {impl FnMut<(u8)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (u8
 
 // Full name: test_crate::fn_casts::closure::{impl Destruct for closure}::drop_in_place
 fn {impl Destruct for closure}::drop_in_place(@1: *mut closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::fn_casts::closure::{impl Destruct for closure}
 impl Destruct for closure {
diff --git a/charon/tests/ui/simple/additions.out b/charon/tests/ui/simple/additions.out
index 0b1f14fe4..d6751376e 100644
--- a/charon/tests/ui/simple/additions.out
+++ b/charon/tests/ui/simple/additions.out
@@ -122,7 +122,7 @@ impl Copy for u8 {
 
 // Full name: core::marker::Destruct::drop_in_place
 fn drop_in_place<Self>(@1: *mut Self)
-= <opaque>
+= <missing>
 
 pub fn core::num::{u8}::saturating_add(@1: u8, @2: u8) -> u8
 {
diff --git a/charon/tests/ui/simple/builtin-drop-mono.out b/charon/tests/ui/simple/builtin-drop-mono.out
index 44411b654..caff4d9ae 100644
--- a/charon/tests/ui/simple/builtin-drop-mono.out
+++ b/charon/tests/ui/simple/builtin-drop-mono.out
@@ -161,22 +161,22 @@ pub trait Destruct::<(String, String)>
 }
 
 fn core::marker::Destruct::drop_in_place::<Global>(@1: *mut Global)
-= <opaque>
+= <missing>
 
 fn core::marker::Destruct::drop_in_place::<alloc::boxed::Box<Slice<String>>[{built_in impl MetaSized::<Slice<String>>}, {built_in impl Sized::<Global>}, {impl Destruct::<Slice<String>>}::<String>, {impl Destruct::<Global>}]>(@1: *mut alloc::boxed::Box<Slice<String>>[{built_in impl MetaSized::<Slice<String>>}, {built_in impl Sized::<Global>}, {impl Destruct::<Slice<String>>}::<String>, {impl Destruct::<Global>}])
-= <opaque>
+= <missing>
 
 fn core::marker::Destruct::drop_in_place::<String>(@1: *mut String)
-= <opaque>
+= <missing>
 
 fn core::marker::Destruct::drop_in_place::<Array<String, 4 : usize>>(@1: *mut Array<String, 4 : usize>)
-= <opaque>
+= <missing>
 
 fn core::marker::Destruct::drop_in_place::<Slice<String>>(@1: *mut Slice<String>)
-= <opaque>
+= <missing>
 
 fn core::marker::Destruct::drop_in_place::<(String, String)>(@1: *mut (String, String))
-= <opaque>
+= <missing>
 
 // Full name: alloc::boxed::Box::{impl Destruct::<alloc::boxed::Box<Slice<String>>[{built_in impl MetaSized::<Slice<String>>}, {built_in impl Sized::<Global>}, {impl Destruct::<Slice<String>>}::<String>, {impl Destruct::<Global>}]>}::drop_in_place::<Slice<String>, Global>
 fn {impl Destruct::<alloc::boxed::Box<Slice<String>>[{built_in impl MetaSized::<Slice<String>>}, {built_in impl Sized::<Global>}, {impl Destruct::<Slice<String>>}::<String>, {impl Destruct::<Global>}]>}::drop_in_place::<Slice<String>, Global>(@1: *mut alloc::boxed::Box<Slice<String>>[{built_in impl MetaSized::<Slice<String>>}, {built_in impl Sized::<Global>}, {impl Destruct::<Slice<String>>}::<String>, {impl Destruct::<Global>}])
diff --git a/charon/tests/ui/simple/builtin-drop.out b/charon/tests/ui/simple/builtin-drop.out
index c2b561aa7..269d40919 100644
--- a/charon/tests/ui/simple/builtin-drop.out
+++ b/charon/tests/ui/simple/builtin-drop.out
@@ -87,7 +87,49 @@ fn {impl Destruct for Array<T, N>}::drop_in_place<T, const N : usize>(@1: *mut A
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Destruct<T>,
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut Array<T, N>; // arg #1
+    let @2: &'_ mut (Array<T, N>); // anonymous local
+    let @3: *mut Array<T, N>; // anonymous local
+    let @4: *mut Slice<T>; // anonymous local
+    let @5: usize; // anonymous local
+    let @6: usize; // anonymous local
+    let @7: *mut T; // anonymous local
+    let @8: bool; // anonymous local
+    let @9: &'_ mut (Slice<T>); // anonymous local
+    let @10: &'_ mut (T); // anonymous local
+
+    storage_live(@2)
+    storage_live(@3)
+    storage_live(@4)
+    storage_live(@5)
+    storage_live(@6)
+    storage_live(@7)
+    storage_live(@8)
+    @0 := ()
+    @2 := &mut *(@1)
+    @3 := &raw mut *(@2)
+    @4 := unsize_cast<*mut Array<T, N>, *mut Slice<T>, N>(move (@3))
+    @5 := copy (@4.metadata)
+    @6 := const (0 : usize)
+    loop {
+        @8 := copy (@6) == copy (@5)
+        if move (@8) {
+            break 0
+        } else {
+            storage_live(@9)
+            @9 := &mut *(@4) with_metadata(copy (@4.metadata))
+            storage_live(@10)
+            @10 := @SliceIndexMut<'_, T>(move (@9), copy (@6))
+            @7 := &raw mut *(@10)
+            @6 := move (@6) wrap.+ const (1 : usize)
+            drop[@TraitClause1] *(@7)
+            continue 0
+        }
+    }
+    return
+}
 
 // Full name: test_crate::<array>::{impl Destruct for Array<T, N>}
 impl<T, const N : usize> Destruct for Array<T, N>
@@ -104,7 +146,43 @@ fn {impl Destruct for Slice<T>}::drop_in_place<T>(@1: *mut Slice<T>)
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Destruct<T>,
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut Slice<T>; // arg #1
+    let @2: &'_ mut (Slice<T>); // anonymous local
+    let @3: usize; // anonymous local
+    let @4: usize; // anonymous local
+    let @5: *mut T; // anonymous local
+    let @6: bool; // anonymous local
+    let @7: &'_ mut (Slice<T>); // anonymous local
+    let @8: &'_ mut (T); // anonymous local
+
+    storage_live(@2)
+    storage_live(@3)
+    storage_live(@4)
+    storage_live(@5)
+    storage_live(@6)
+    @0 := ()
+    @2 := &mut *(@1) with_metadata(copy (@1.metadata))
+    @3 := copy (@2.metadata)
+    @4 := const (0 : usize)
+    loop {
+        @6 := copy (@4) == copy (@3)
+        if move (@6) {
+            break 0
+        } else {
+            storage_live(@7)
+            @7 := &mut *(@2) with_metadata(copy (@2.metadata))
+            storage_live(@8)
+            @8 := @SliceIndexMut<'_, T>(move (@7), copy (@4))
+            @5 := &raw mut *(@8)
+            @4 := move (@4) wrap.+ const (1 : usize)
+            drop[@TraitClause1] *(@5)
+            continue 0
+        }
+    }
+    return
+}
 
 // Full name: test_crate::<slice>::{impl Destruct for Slice<T>}
 impl<T> Destruct for Slice<T>
@@ -122,7 +200,18 @@ where
     [@TraitClause0]: Sized<A>,
     [@TraitClause1]: Destruct<A>,
     [@TraitClause2]: Destruct<B>,
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut (A, B); // arg #1
+    let @2: &'_ mut ((A, B)); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1) with_metadata(copy (@1.metadata))
+    drop[@TraitClause1] (*(@2)).0
+    drop[@TraitClause2] (*(@2)).1
+    return
+}
 
 // Full name: test_crate::<tuple_2>::{impl Destruct for (A, B)}
 impl<A, B> Destruct for (A, B)
diff --git a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out
index 55f1d59d1..e9294f38d 100644
--- a/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out
+++ b/charon/tests/ui/simple/call-inherent-method-with-trait-bound.out
@@ -60,7 +60,7 @@ where
 fn {impl Destruct for HashMap<S>[@TraitClause0]}::drop_in_place<S>(@1: *mut HashMap<S>[@TraitClause0])
 where
     [@TraitClause0]: Sized<S>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::HashMap::{impl Destruct for HashMap<S>[@TraitClause0]}
 impl<S> Destruct for HashMap<S>[@TraitClause0]
diff --git a/charon/tests/ui/simple/closure-capture-ref-by-move.out b/charon/tests/ui/simple/closure-capture-ref-by-move.out
index 493d2bac4..9a9fd3b89 100644
--- a/charon/tests/ui/simple/closure-capture-ref-by-move.out
+++ b/charon/tests/ui/simple/closure-capture-ref-by-move.out
@@ -133,7 +133,7 @@ fn foo()
 
 // Full name: test_crate::foo::closure::{impl Destruct for closure<'_0>}::drop_in_place
 fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::foo::closure::{impl Destruct for closure<'_0>}
 impl<'_0> Destruct for closure<'_0> {
diff --git a/charon/tests/ui/simple/closure-fn.out b/charon/tests/ui/simple/closure-fn.out
index 3beb39295..16164114f 100644
--- a/charon/tests/ui/simple/closure-fn.out
+++ b/charon/tests/ui/simple/closure-fn.out
@@ -232,7 +232,7 @@ fn {impl FnMut<(u8, u8)> for closure<'_0, '_1>}::call_mut<'_0, '_1, '_2>(@1: &'_
 
 // Full name: test_crate::main::closure::{impl Destruct for closure<'_0, '_1>}::drop_in_place
 fn {impl Destruct for closure<'_0, '_1>}::drop_in_place<'_0, '_1>(@1: *mut closure<'_0, '_1>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::main::closure::{impl Destruct for closure<'_0, '_1>}
 impl<'_0, '_1> Destruct for closure<'_0, '_1> {
diff --git a/charon/tests/ui/simple/closure-fnmut.out b/charon/tests/ui/simple/closure-fnmut.out
index 999dcb3d3..b9070e389 100644
--- a/charon/tests/ui/simple/closure-fnmut.out
+++ b/charon/tests/ui/simple/closure-fnmut.out
@@ -135,7 +135,7 @@ fn {impl FnMut<(u8)> for closure<'_0>}::call_mut<'_0, '_1>(@1: &'_1 mut (closure
 
 // Full name: test_crate::main::closure::{impl Destruct for closure<'_0>}::drop_in_place
 fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::main::closure::{impl Destruct for closure<'_0>}
 impl<'_0> Destruct for closure<'_0> {
diff --git a/charon/tests/ui/simple/closure-inside-impl.out b/charon/tests/ui/simple/closure-inside-impl.out
index ad1190081..c3cb949c6 100644
--- a/charon/tests/ui/simple/closure-inside-impl.out
+++ b/charon/tests/ui/simple/closure-inside-impl.out
@@ -166,7 +166,7 @@ fn {impl Destruct for closure<F, T>[@TraitClause0, @TraitClause1]}::drop_in_plac
 where
     [@TraitClause0]: Sized<F>,
     [@TraitClause1]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::{Foo<F>[@TraitClause0]}::method::closure::{impl Destruct for closure<F, T>[@TraitClause0, @TraitClause1]}
 impl<F, T> Destruct for closure<F, T>[@TraitClause0, @TraitClause1]
diff --git a/charon/tests/ui/simple/closure-inside-inline-const.out b/charon/tests/ui/simple/closure-inside-inline-const.out
index 16e9f0c92..8657a71f0 100644
--- a/charon/tests/ui/simple/closure-inside-inline-const.out
+++ b/charon/tests/ui/simple/closure-inside-inline-const.out
@@ -157,7 +157,7 @@ where
 fn {impl Destruct for closure<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut closure<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::foo::{const}::closure::{impl Destruct for closure<T>[@TraitClause0]}
 impl<T> Destruct for closure<T>[@TraitClause0]
diff --git a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out
index c352f5d76..13302e6c3 100644
--- a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out
+++ b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out
@@ -105,7 +105,17 @@ trait Thing<Self>
 
 // Full name: test_crate::<tuple_1>::{impl Destruct for (A)}::drop_in_place
 fn {impl Destruct for (A)}::drop_in_place<A>(@1: *mut (A))
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut (A); // arg #1
+    let @2: &'_ mut ((A)); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1) with_metadata(copy (@1.metadata))
+    drop[{built_in impl Destruct for A}] (*(@2)).0
+    return
+}
 
 // Full name: test_crate::<tuple_1>::{impl Destruct for (A)}
 impl<A> Destruct for (A) {
@@ -194,7 +204,7 @@ where
 fn {impl Destruct for closure<Self>[@TraitClause0]}::drop_in_place<Self>(@1: *mut closure<Self>[@TraitClause0])
 where
     [@TraitClause0]: Thing<Self>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::Thing::foo::closure::{impl Destruct for closure<Self>[@TraitClause0]}
 impl<Self> Destruct for closure<Self>[@TraitClause0]
diff --git a/charon/tests/ui/simple/closure-with-drops.out b/charon/tests/ui/simple/closure-with-drops.out
index 3722a18d1..fefe33638 100644
--- a/charon/tests/ui/simple/closure-with-drops.out
+++ b/charon/tests/ui/simple/closure-with-drops.out
@@ -122,7 +122,17 @@ fn {impl Destruct for test_crate::foo::closure<T>[@TraitClause0, @TraitClause1]}
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Destruct<T>,
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut test_crate::foo::closure<T>[@TraitClause0, @TraitClause1]; // arg #1
+    let @2: &'_ mut (test_crate::foo::closure<T>[@TraitClause0, @TraitClause1]); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1)
+    drop[@TraitClause1] (*(@2)).0
+    return
+}
 
 // Full name: test_crate::foo::closure::{impl Destruct for test_crate::foo::closure<T>[@TraitClause0, @TraitClause1]}
 impl<T> Destruct for test_crate::foo::closure<T>[@TraitClause0, @TraitClause1]
@@ -208,7 +218,16 @@ fn bar()
 
 // Full name: test_crate::bar::closure::{impl Destruct for test_crate::bar::closure}::drop_in_place
 fn {impl Destruct for test_crate::bar::closure}::drop_in_place(@1: *mut test_crate::bar::closure)
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut test_crate::bar::closure; // arg #1
+    let @2: &'_ mut (test_crate::bar::closure); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1)
+    return
+}
 
 // Full name: test_crate::bar::closure::{impl Destruct for test_crate::bar::closure}
 impl Destruct for test_crate::bar::closure {
diff --git a/charon/tests/ui/simple/drop-cow.out b/charon/tests/ui/simple/drop-cow.out
index 42a6a9204..563260998 100644
--- a/charon/tests/ui/simple/drop-cow.out
+++ b/charon/tests/ui/simple/drop-cow.out
@@ -93,7 +93,24 @@ where
     [@TraitClause2]: Destruct<B>,
     B : 'a,
     B : 'a,
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]; // arg #1
+    let @2: &'_ mut (Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1)
+    match *(@2) {
+        Cow::Borrowed => {
+        },
+        _ => {
+            drop[@TraitClause1::parent_clause4] (*(@2) as variant Cow::Owned).0
+            return
+        },
+    }
+    return
+}
 
 // Full name: test_crate::Cow::{impl Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]}
 impl<'a, B> Destruct for Cow<'a, B>[@TraitClause0, @TraitClause1, @TraitClause2]
diff --git a/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.out b/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.out
new file mode 100644
index 000000000..dea42175d
--- /dev/null
+++ b/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.out
@@ -0,0 +1,82 @@
+# Final LLBC before serialization:
+
+// Full name: core::marker::MetaSized
+#[lang_item("meta_sized")]
+pub trait MetaSized<Self>
+
+// Full name: core::marker::Sized
+#[lang_item("sized")]
+pub trait Sized<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    non-dyn-compatible
+}
+
+// Full name: core::marker::Destruct
+#[lang_item("destruct")]
+pub trait Destruct<Self>
+{
+    fn drop_in_place = core::marker::Destruct::drop_in_place<Self>
+    vtable: core::marker::Destruct::{vtable}
+}
+
+fn core::marker::Destruct::drop_in_place<Self>(@1: *mut Self)
+= <opaque>
+
+// Full name: alloc::alloc::Global
+#[lang_item("global_alloc_ty")]
+pub struct Global {}
+
+// Full name: alloc::alloc::Global::{impl Destruct for Global}::drop_in_place
+fn {impl Destruct for Global}::drop_in_place(@1: *mut Global)
+= <opaque>
+
+// Full name: alloc::alloc::Global::{impl Destruct for Global}
+impl Destruct for Global {
+    fn drop_in_place = {impl Destruct for Global}::drop_in_place
+    non-dyn-compatible
+}
+
+fn UNIT_METADATA()
+{
+    let @0: (); // return
+
+    @0 := ()
+    return
+}
+
+const UNIT_METADATA: () = @Fun0()
+
+// Full name: test_crate::KeccakState
+struct KeccakState {}
+
+// Full name: test_crate::PortableHash
+struct PortableHash<const K : usize> {
+  shake128_state: Array<KeccakState, K>,
+  make_non_trivial: alloc::boxed::Box<u32>[{built_in impl MetaSized for u32}, {built_in impl Sized for Global}, {built_in impl Destruct for u32}, {impl Destruct for Global}],
+}
+
+// Full name: test_crate::PortableHash::{impl Destruct for PortableHash<K>}::drop_in_place
+fn {impl Destruct for PortableHash<K>}::drop_in_place<const K : usize>(@1: *mut PortableHash<K>)
+= <opaque>
+
+// Full name: test_crate::PortableHash::{impl Destruct for PortableHash<K>}
+impl<const K : usize> Destruct for PortableHash<K> {
+    fn drop_in_place = {impl Destruct for PortableHash<K>}::drop_in_place<K>
+    non-dyn-compatible
+}
+
+// Full name: test_crate::foo
+fn foo(@1: PortableHash<42 : usize>)
+{
+    let @0: (); // return
+    let @1: PortableHash<42 : usize>; // arg #1
+
+    @0 := ()
+    @0 := ()
+    drop[{impl Destruct for PortableHash<K>}<42 : usize>] @1
+    return
+}
+
+
+
diff --git a/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.rs b/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.rs
new file mode 100644
index 000000000..4fdbd0053
--- /dev/null
+++ b/charon/tests/ui/simple/drop-glue-with-const-generic-silenced.rs
@@ -0,0 +1,10 @@
+//@ charon-args=--precise-drops
+//@ charon-arg=--opaque={impl core::marker::Destruct for crate::PortableHash}
+struct KeccakState;
+
+struct PortableHash<const K: usize> {
+    shake128_state: [KeccakState; K],
+    make_non_trivial: Box<u32>,
+}
+
+fn foo(_: PortableHash<42>) {}
diff --git a/charon/tests/ui/simple/drop-glue-with-const-generic.out b/charon/tests/ui/simple/drop-glue-with-const-generic.out
new file mode 100644
index 000000000..f79028fc1
--- /dev/null
+++ b/charon/tests/ui/simple/drop-glue-with-const-generic.out
@@ -0,0 +1,29 @@
+error: internal compiler error: compiler/rustc_middle/src/ty/sty.rs:373:13: cannot find `K/#0` in param-env: ParamEnv {
+                                    caller_bounds: [
+                                        Binder { value: HostEffectPredicate { trait_ref: <T as std::marker::Destruct>, constness: Maybe }, bound_vars: [] },
+                                        Binder { value: TraitPredicate(<T as std::marker::Destruct>, polarity:Positive), bound_vars: [] },
+                                    ],
+                                }
+
+
+thread 'rustc' panicked at compiler/rustc_middle/src/ty/sty.rs:373:13:
+Box<dyn Any>
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+error: rustc panicked while retrieving drop glue. This is known to happen with `--precise-drops`; to silence this warning, pass `--opaque '{impl core::marker::Destruct for test_crate::PortableHash}'` to charon
+ --> tests/ui/simple/drop-glue-with-const-generic.rs:5:1
+  |
+5 | / struct PortableHash<const K: usize> {
+6 | |     shake128_state: [KeccakState; K],
+7 | |     make_non_trivial: Box<u32>,
+8 | | }
+  | |_^
+
+error: Item `test_crate::PortableHash` caused errors; ignoring.
+ --> tests/ui/simple/drop-glue-with-const-generic.rs:5:1
+  |
+5 | struct PortableHash<const K: usize> {
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 1 previous error
+
+ERROR Code failed to compile
diff --git a/charon/tests/ui/simple/drop-glue-with-const-generic.rs b/charon/tests/ui/simple/drop-glue-with-const-generic.rs
new file mode 100644
index 000000000..5b09c5133
--- /dev/null
+++ b/charon/tests/ui/simple/drop-glue-with-const-generic.rs
@@ -0,0 +1,10 @@
+//@ known-failure
+//@ charon-args=--precise-drops
+struct KeccakState;
+
+struct PortableHash<const K: usize> {
+    shake128_state: [KeccakState; K],
+    make_non_trivial: Box<u32>,
+}
+
+fn foo(_: PortableHash<42>) {}
diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out
index 5ecb6eba5..638766ab3 100644
--- a/charon/tests/ui/simple/dyn-fn.out
+++ b/charon/tests/ui/simple/dyn-fn.out
@@ -175,7 +175,7 @@ fn {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_1>(@1: &'_1 mut (c
 
 // Full name: test_crate::gives_fn::closure::{impl Destruct for closure}::drop_in_place
 fn {impl Destruct for closure}::drop_in_place(@1: *mut closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::gives_fn::closure::{impl Destruct for closure}
 impl Destruct for closure {
diff --git a/charon/tests/ui/simple/foreign-inline-const.out b/charon/tests/ui/simple/foreign-inline-const.out
index d4b1be843..7cea121cd 100644
--- a/charon/tests/ui/simple/foreign-inline-const.out
+++ b/charon/tests/ui/simple/foreign-inline-const.out
@@ -157,7 +157,7 @@ where
 fn {impl Destruct for closure<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut closure<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: closure_inside_inline_const::foo::{const}::closure::{impl Destruct for closure<T>[@TraitClause0]}
 impl<T> Destruct for closure<T>[@TraitClause0]
diff --git a/charon/tests/ui/simple/lending-iterator-gat.out b/charon/tests/ui/simple/lending-iterator-gat.out
index c83f9eb1e..307938784 100644
--- a/charon/tests/ui/simple/lending-iterator-gat.out
+++ b/charon/tests/ui/simple/lending-iterator-gat.out
@@ -126,7 +126,17 @@ pub trait LendingIterator<Self>
 
 // Full name: test_crate::<tuple_1>::{impl Destruct for (A)}::drop_in_place
 fn {impl Destruct for (A)}::drop_in_place<A>(@1: *mut (A))
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut (A); // arg #1
+    let @2: &'_ mut ((A)); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1) with_metadata(copy (@1.metadata))
+    drop[{built_in impl Destruct for A}] (*(@2)).0
+    return
+}
 
 // Full name: test_crate::<tuple_1>::{impl Destruct for (A)}
 impl<A> Destruct for (A) {
@@ -279,7 +289,7 @@ fn {impl FnMut<(&'_ (i32))> for closure<'_0>}::call_mut<'_0, '_1, '_2>(@1: &'_2
 
 // Full name: test_crate::main::closure::{impl Destruct for closure<'_0>}::drop_in_place
 fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::main::closure::{impl Destruct for closure<'_0>}
 impl<'_0> Destruct for closure<'_0> {
diff --git a/charon/tests/ui/simple/manual-drop-impl.out b/charon/tests/ui/simple/manual-drop-impl.out
index 2b3809810..0a8038ee2 100644
--- a/charon/tests/ui/simple/manual-drop-impl.out
+++ b/charon/tests/ui/simple/manual-drop-impl.out
@@ -70,7 +70,7 @@ where
 fn {impl Destruct for Foo<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut Foo<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::Foo::{impl Destruct for Foo<T>[@TraitClause0]}
 impl<T> Destruct for Foo<T>[@TraitClause0]
diff --git a/charon/tests/ui/simple/nested-closure-trait-ref.out b/charon/tests/ui/simple/nested-closure-trait-ref.out
index af2a80e86..8e1d4060a 100644
--- a/charon/tests/ui/simple/nested-closure-trait-ref.out
+++ b/charon/tests/ui/simple/nested-closure-trait-ref.out
@@ -130,7 +130,7 @@ fn {impl Destruct for test_crate::foo::closure<T>[@TraitClause0, @TraitClause1]}
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Clone<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::foo::closure::{impl Destruct for test_crate::foo::closure<T>[@TraitClause0, @TraitClause1]}
 impl<T> Destruct for test_crate::foo::closure<T>[@TraitClause0, @TraitClause1]
@@ -239,7 +239,7 @@ fn {impl Destruct for test_crate::foo::closure::closure<T>[@TraitClause0, @Trait
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Clone<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::foo::closure::closure::{impl Destruct for test_crate::foo::closure::closure<T>[@TraitClause0, @TraitClause1]}
 impl<T> Destruct for test_crate::foo::closure::closure<T>[@TraitClause0, @TraitClause1]
diff --git a/charon/tests/ui/simple/nested-closure.out b/charon/tests/ui/simple/nested-closure.out
index 22f41f97e..de05ff8d4 100644
--- a/charon/tests/ui/simple/nested-closure.out
+++ b/charon/tests/ui/simple/nested-closure.out
@@ -311,7 +311,7 @@ fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closu
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Clone<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::{impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}
 impl<'a, '_1, T> Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]
@@ -406,7 +406,7 @@ fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closu
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Clone<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::{impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}
 impl<'a, '_1, T> Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]
@@ -501,7 +501,7 @@ fn {impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closu
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Clone<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure::{impl Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]}
 impl<'a, '_1, T> Destruct for test_crate::{Foo<'a, T>[@TraitClause0]}::test_nested_closures::closure::closure::closure<'_, '_1, T>[@TraitClause0, @TraitClause1]
diff --git a/charon/tests/ui/simple/promoted-closure-no-warns.out b/charon/tests/ui/simple/promoted-closure-no-warns.out
index 15b03ba61..1da3898dc 100644
--- a/charon/tests/ui/simple/promoted-closure-no-warns.out
+++ b/charon/tests/ui/simple/promoted-closure-no-warns.out
@@ -152,7 +152,7 @@ fn {impl FnMut<(u32)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (u
 
 // Full name: test_crate::foo::closure::{impl Destruct for closure}::drop_in_place
 fn {impl Destruct for closure}::drop_in_place(@1: *mut closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::foo::closure::{impl Destruct for closure}
 impl Destruct for closure {
diff --git a/charon/tests/ui/simple/promoted-closure.out b/charon/tests/ui/simple/promoted-closure.out
index 15b03ba61..1da3898dc 100644
--- a/charon/tests/ui/simple/promoted-closure.out
+++ b/charon/tests/ui/simple/promoted-closure.out
@@ -152,7 +152,7 @@ fn {impl FnMut<(u32)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (u
 
 // Full name: test_crate::foo::closure::{impl Destruct for closure}::drop_in_place
 fn {impl Destruct for closure}::drop_in_place(@1: *mut closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::foo::closure::{impl Destruct for closure}
 impl Destruct for closure {
diff --git a/charon/tests/ui/simple/promoted_in_closure.out b/charon/tests/ui/simple/promoted_in_closure.out
index 4aef7bfaa..09d0d3ac6 100644
--- a/charon/tests/ui/simple/promoted_in_closure.out
+++ b/charon/tests/ui/simple/promoted_in_closure.out
@@ -152,7 +152,7 @@ fn {impl FnMut<()> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: ())
 
 // Full name: test_crate::main::closure::{impl Destruct for closure}::drop_in_place
 fn {impl Destruct for closure}::drop_in_place(@1: *mut closure)
-= <opaque>
+= <missing>
 
 // Full name: test_crate::main::closure::{impl Destruct for closure}
 impl Destruct for closure {
diff --git a/charon/tests/ui/simple/vec-with-capacity.out b/charon/tests/ui/simple/vec-with-capacity.out
index 2501e5f12..07addd999 100644
--- a/charon/tests/ui/simple/vec-with-capacity.out
+++ b/charon/tests/ui/simple/vec-with-capacity.out
@@ -158,7 +158,7 @@ fn {impl Destruct for Vec<T>[@TraitClause0, @TraitClause1]}::drop_in_place<T, A>
 where
     [@TraitClause0]: Sized<T>,
     [@TraitClause1]: Sized<A>,
-= <opaque>
+= <missing>
 
 // Full name: alloc::vec::Vec::{impl Destruct for Vec<T>[@TraitClause0, @TraitClause1]}
 impl<T, A> Destruct for Vec<T>[@TraitClause0, @TraitClause1]
diff --git a/charon/tests/ui/traits.out b/charon/tests/ui/traits.out
index d936b6f0b..62563ab13 100644
--- a/charon/tests/ui/traits.out
+++ b/charon/tests/ui/traits.out
@@ -146,7 +146,18 @@ pub trait BoolTrait<Self>
 fn {impl Destruct for (A, B)}::drop_in_place<A, B>(@1: *mut (A, B))
 where
     [@TraitClause0]: Sized<A>,
-= <opaque>
+{
+    let @0: (); // return
+    let @1: *mut (A, B); // arg #1
+    let @2: &'_ mut ((A, B)); // anonymous local
+
+    storage_live(@2)
+    @0 := ()
+    @2 := &mut *(@1) with_metadata(copy (@1.metadata))
+    drop[{built_in impl Destruct for A}] (*(@2)).0
+    drop[{built_in impl Destruct for B}] (*(@2)).1
+    return
+}
 
 // Full name: test_crate::<tuple_2>::{impl Destruct for (A, B)}
 impl<A, B> Destruct for (A, B)
@@ -454,7 +465,7 @@ where
 fn {impl Destruct for Wrapper<T>[@TraitClause0]}::drop_in_place<T>(@1: *mut Wrapper<T>[@TraitClause0])
 where
     [@TraitClause0]: Sized<T>,
-= <opaque>
+= <missing>
 
 // Full name: test_crate::Wrapper::{impl Destruct for Wrapper<T>[@TraitClause0]}
 impl<T> Destruct for Wrapper<T>[@TraitClause0]