diff --git a/charon/src/ast/types_utils.rs b/charon/src/ast/types_utils.rs
index aa2a41f23..907b769fb 100644
--- a/charon/src/ast/types_utils.rs
+++ b/charon/src/ast/types_utils.rs
@@ -1305,6 +1305,21 @@ impl TypeDecl {
             .as_ref()
             .is_some_and(|repr| repr.repr_algo == ReprAlgorithm::C)
     }
+
+    pub fn get_field_by_name(
+        &self,
+        variant: Option<VariantId>,
+        field_name: &str,
+    ) -> Option<(FieldId, &Field)> {
+        let fields = match &self.kind {
+            TypeDeclKind::Struct(fields) | TypeDeclKind::Union(fields) => fields,
+            TypeDeclKind::Enum(variants) => &variants[variant.unwrap()].fields,
+            _ => return None,
+        };
+        fields
+            .iter_indexed()
+            .find(|(_, field)| field.name.as_deref() == Some(field_name))
+    }
 }
 
 impl Layout {
diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs
index e53ed8cd7..5a9bbbcd8 100644
--- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs
+++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs
@@ -297,7 +297,7 @@ impl ItemTransCtx<'_, '_> {
         mk_field("size".into(), usize_ty());
         // Field: `align: usize`
         mk_field("align".into(), usize_ty());
-        // Field: `drop: fn(*mut Self)`
+        // Field: `drop: fn(*mut Self)` -- `Self` is just a placeholder, will be dynified below.
         mk_field("drop".into(), {
             let self_ty = TyKind::TypeVar(DeBruijnVar::new_at_zero(TypeVarId::ZERO)).into_ty();
             let self_ptr = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs
index 7a43c25a0..ea58dd7c2 100644
--- a/charon/src/transform/ctx.rs
+++ b/charon/src/transform/ctx.rs
@@ -445,6 +445,29 @@ impl BodyTransformCtx for UllbcStatementTransformCtx<'_> {
 }
 
 impl FunDecl {
+    pub fn transform_ullbc_terminators(
+        &mut self,
+        ctx: &mut TransformCtx,
+        mut f: impl FnMut(&mut UllbcStatementTransformCtx, &mut ullbc_ast::Terminator),
+    ) {
+        if let Ok(body) = &mut self.body {
+            let params = &self.signature.generics;
+            let body = body.as_unstructured_mut().unwrap();
+            body.body.iter_mut().for_each(|block| {
+                let span = block.terminator.span;
+                let mut ctx = UllbcStatementTransformCtx {
+                    ctx,
+                    params,
+                    locals: &mut body.locals,
+                    span,
+                    statements: std::mem::take(&mut block.statements),
+                };
+                f(&mut ctx, &mut block.terminator);
+                block.statements = ctx.statements;
+            });
+        }
+    }
+
     pub fn transform_ullbc_statements(
         &mut self,
         ctx: &mut TransformCtx,
diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs
index 06c292fd8..91269e570 100644
--- a/charon/src/transform/mod.rs
+++ b/charon/src/transform/mod.rs
@@ -26,6 +26,7 @@ pub mod normalize {
     pub mod filter_unreachable_blocks;
     pub mod monomorphize;
     pub mod skip_trait_refs_when_known;
+    pub mod transform_dyn_trait_calls;
 }
 
 /// Passes that undo some lowering done by rustc to recover an operation closer to what the user
@@ -101,13 +102,16 @@ pub static INITIAL_CLEANUP_PASSES: &[Pass] = &[
     // # Micro-pass: remove the explicit `Self: Trait` clause of methods/assoc const declaration
     // items if they're not used. This simplifies the graph of dependencies between definitions.
     NonBody(&simplify_output::remove_unused_self_clause::Transform),
-    // Change trait associated types to be type parameters instead. See the module for details.
-    // This also normalizes any use of an associated type that we can resolve.
-    NonBody(&normalize::expand_associated_types::Transform),
     // # Micro-pass: whenever we call a trait method on a known type, refer to the method `FunDecl`
     // directly instead of going via a `TraitRef`. This is done before `reorder_decls` to remove
     // some sources of mutual recursion.
     UnstructuredBody(&normalize::skip_trait_refs_when_known::Transform),
+    // Transform dyn trait method calls to vtable function pointer calls
+    // This should be early to handle the calls before other transformations
+    UnstructuredBody(&normalize::transform_dyn_trait_calls::Transform),
+    // Change trait associated types to be type parameters instead. See the module for details.
+    // This also normalizes any use of an associated type that we can resolve.
+    NonBody(&normalize::expand_associated_types::Transform),
 ];
 
 /// Body cleanup passes on the ullbc.
diff --git a/charon/src/transform/normalize/expand_associated_types.rs b/charon/src/transform/normalize/expand_associated_types.rs
index 1d28627e6..02f32df98 100644
--- a/charon/src/transform/normalize/expand_associated_types.rs
+++ b/charon/src/transform/normalize/expand_associated_types.rs
@@ -65,7 +65,6 @@
 //! ```
 //!
 //! Limitations:
-//! - we're missing assoc type info in `dyn Trait`, so we can't fixup the generics there.
 //! - we don't track bound lifetimes in quantified clauses properly (<https://github.com/AeneasVerif/charon/issues/534>).
 //! - type aliases don't have the correct clauses in scope (<https://github.com/AeneasVerif/charon/issues/531>).
 //! - we don't take into account unicity of trait implementations. This means we won't detect type
@@ -404,8 +403,12 @@ mod type_constraint_set {
             self.insert_inner(&path, Some(cid), ty);
         }
 
-        /// Find the entry at that path from the trie, if it exists.
-        pub fn find(&self, path: &AssocTypePath) -> Option<(Option<TraitTypeConstraintId>, &Ty)> {
+        /// Find the entry at that path from the trie, if it exists. Also returns the type
+        /// constraint that gave us that type.
+        pub fn find_ty_and_used_constraint(
+            &self,
+            path: &AssocTypePath,
+        ) -> Option<(Option<TraitTypeConstraintId>, &Ty)> {
             if let BaseClause::Local(var) = path.tref.base {
                 // Only lookup at level zero because replacements are always at level zero relative to
                 // the item.
@@ -419,6 +422,10 @@ mod type_constraint_set {
                 .get(&path.type_name)
                 .map(|(id, ty)| (*id, ty))
         }
+        /// Find the entry at that path from the trie, if it exists.
+        pub fn find(&self, path: &AssocTypePath) -> Option<&Ty> {
+            Some(self.find_ty_and_used_constraint(path)?.1)
+        }
 
         pub fn iter(&self) -> impl Iterator<Item = (AssocTypePath, Ty)> {
             let mut vec = vec![];
@@ -534,7 +541,7 @@ impl ItemModifications {
     /// Record that we must replace this path. If there is a relevant type constraint we can use
     /// it, otherwise we will need to add a new type parameter to supply a value for this path.
     fn replace_path(&mut self, path: AssocTypePath) {
-        if let Some((cstr_id, _)) = self.type_constraints.find(&path) {
+        if let Some((cstr_id, _)) = self.type_constraints.find_ty_and_used_constraint(&path) {
             // The local constraints already give us a value for this associated type; we
             // use that.
             if let Some(cstr_id) = cstr_id {
@@ -840,14 +847,13 @@ impl<'a> ComputeItemModifications<'a> {
     }
 
     /// Returns the associated types values known for the given trait ref.
-    // TODO: also extract refs from `dyn Trait` refs.
-    fn compute_assoc_tys_for_tref_kind(
+    fn compute_assoc_tys_for_tref(
         &mut self,
         span: Span,
-        tref: &TraitRefKind,
+        tref: &TraitRef,
     ) -> Vec<(AssocTypePath, Ty)> {
-        let mut out = vec![];
-        match tref {
+        let mut tys = vec![];
+        match &tref.kind {
             TraitRefKind::Clause(..)
             | TraitRefKind::ParentClause(..)
             | TraitRefKind::ItemClause(..)
@@ -855,7 +861,7 @@ impl<'a> ComputeItemModifications<'a> {
             | TraitRefKind::Unknown(_) => {}
             TraitRefKind::TraitImpl(impl_ref) => {
                 if let Some(set_for_clause) = self.compute_assoc_tys_for_impl(impl_ref.id) {
-                    out.extend(set_for_clause.iter_self_paths_subst(&impl_ref.generics));
+                    tys.extend(set_for_clause.iter_self_paths_subst(&impl_ref.generics));
                 }
             }
             TraitRefKind::BuiltinOrAuto {
@@ -865,11 +871,11 @@ impl<'a> ComputeItemModifications<'a> {
             } => {
                 for (name, assoc_ty) in types.iter().cloned() {
                     let path = TraitRefPath::self_ref().with_assoc_type(name);
-                    out.push((path, assoc_ty.value));
+                    tys.push((path, assoc_ty.value));
                 }
                 for (parent_clause_id, parent_ref) in parent_trait_refs.iter_indexed() {
                     let clause_path = TraitRefPath::parent_clause(parent_clause_id);
-                    out.extend(
+                    tys.extend(
                         self.compute_assoc_tys_for_tref(span, parent_ref)
                             .into_iter()
                             .map(|(path, ty)| {
@@ -879,23 +885,39 @@ impl<'a> ComputeItemModifications<'a> {
                     )
                 }
             }
-            TraitRefKind::Dyn { .. } => {
-                register_error!(
-                    self.ctx,
-                    span,
-                    "Can't process associated types for `dyn Trait`"
-                );
+            TraitRefKind::Dyn => {
+                let pred = &tref.trait_decl_ref;
+                let self_ty = pred.skip_binder.generics.types[0]
+                    .clone()
+                    .move_from_under_binder()
+                    .unwrap();
+                if !self_ty.is_error() {
+                    let TyKind::DynTrait(dyn_pred) = self_ty.kind() else {
+                        unreachable!(
+                            "`TraitRefKind::Dyn` only makes sense with a `dyn Trait` Self type"
+                        )
+                    };
+                    tys.extend(
+                        self.compute_constraint_set(&dyn_pred.binder.params)
+                            .iter()
+                            // Paths apply to the first clause of the binder, which is the one
+                            // that's being implemented. FIXME: is that true? if not, ask hax to
+                            // resolve the correct clause.
+                            .filter(|(path, _ty)| {
+                                matches!(path.tref.base, BaseClause::Local(id)
+                                    if id == DeBruijnVar::new_at_zero(TraitClauseId::ZERO))
+                            })
+                            .map(|(path, ty)| {
+                                (
+                                    path.pop_base(),
+                                    ty.move_from_under_binder()
+                                        .expect("unepected dyn type constraint"),
+                                )
+                            }),
+                    );
+                }
             }
         }
-        out
-    }
-
-    fn compute_assoc_tys_for_tref(
-        &mut self,
-        span: Span,
-        tref: &TraitRef,
-    ) -> Vec<(AssocTypePath, Ty)> {
-        let mut tys = self.compute_assoc_tys_for_tref_kind(span, &tref.kind);
         if let Some(base_path) = tref.to_path() {
             for (path, ty) in
                 self.compute_implied_constraints_for_poly_predicate(&tref.trait_decl_ref)
@@ -942,17 +964,17 @@ impl UpdateItemBody<'_> {
             }
             _ => self.type_replacements.depth(),
         };
-        let ty = self.type_replacements[dbid].find(&path)?.1;
+        let ty = self.type_replacements[dbid].find(&path)?;
         Some(ty.clone().move_under_binders(dbid))
     }
 
-    fn lookup_path_on_trait_ref(&self, path: &AssocTypePath, tref: &TraitRefKind) -> Option<Ty> {
+    fn lookup_path_on_trait_ref(&self, path: &AssocTypePath, tref: &TraitRef) -> Option<Ty> {
         assert!(path.tref.base.is_self_clause());
-        match tref {
+        match &tref.kind {
             TraitRefKind::TraitImpl(impl_ref) => {
                 // The type constraints of trait impls already contain all relevant type
                 // equalities.
-                let (_, ty) = self
+                let ty = self
                     .item_modifications
                     .get(&GenericsSource::item(impl_ref.id))?
                     .type_constraints
@@ -969,7 +991,7 @@ impl UpdateItemBody<'_> {
             }
             TraitRefKind::ParentClause(parent, clause_id) => {
                 let path = path.on_tref(&TraitRefPath::parent_clause(*clause_id));
-                self.lookup_path_on_trait_ref(&path, &parent.kind)
+                self.lookup_path_on_trait_ref(&path, parent)
             }
             TraitRefKind::ItemClause(..) => None,
             TraitRefKind::BuiltinOrAuto {
@@ -983,11 +1005,31 @@ impl UpdateItemBody<'_> {
                     .map(|(_, assoc_ty)| assoc_ty.value.clone()),
                 Some((parent_clause_id, sub_path)) => {
                     let parent_ref = &parent_trait_refs[parent_clause_id];
-                    self.lookup_path_on_trait_ref(&sub_path, &parent_ref.kind)
+                    self.lookup_path_on_trait_ref(&sub_path, parent_ref)
                 }
             },
-            // TODO: add enough info to recover assoc types.
-            TraitRefKind::Dyn { .. } => None,
+            TraitRefKind::Dyn => {
+                let pred = &tref.trait_decl_ref;
+                let self_ty = pred.skip_binder.generics.types[0]
+                    .clone()
+                    .move_from_under_binder()
+                    .unwrap();
+                if self_ty.is_error() {
+                    return None;
+                }
+                let TyKind::DynTrait(dyn_pred) = self_ty.kind() else {
+                    unreachable!(
+                        "`TraitRefKind::Dyn` only makes sense with a `dyn Trait` Self type"
+                    )
+                };
+                // Paths apply to the first clause of the binder, which is the one that's being
+                // implemented. FIXME: is that true? if not, ask hax to resolve the correct clause.
+                let path = &path.on_local_clause(TraitClauseId::ZERO);
+                self.compute_constraints_for_binder(&dyn_pred.binder)
+                    .find(path)?
+                    .clone()
+                    .move_from_under_binder()
+            }
             TraitRefKind::Unknown(..) => None,
         }
     }
@@ -996,7 +1038,7 @@ impl UpdateItemBody<'_> {
         &mut self,
         args: &mut GenericArgs,
         target: GenericsSource,
-        self_path: Option<TraitRefKind>,
+        self_path: Option<TraitRef>,
     ) {
         let Some(modifications) = self.item_modifications.get(&target) else {
             return;
@@ -1010,7 +1052,7 @@ impl UpdateItemBody<'_> {
                         .bound_at_depth(DeBruijnId::zero())
                         .expect("found replacement not at binder level 0?");
                     path = path.pop_base();
-                    &args.trait_refs[clause_id].kind
+                    &args.trait_refs[clause_id]
                 }
             };
             let ty = if let Some(ty) = self.lookup_path_on_trait_ref(&path, &base_tref) {
@@ -1051,7 +1093,11 @@ impl UpdateItemBody<'_> {
     fn process_trait_decl_ref(&mut self, tref: &mut TraitDeclRef, self_path: TraitRefKind) {
         trace!("{tref:?}");
         let target = GenericsSource::item(tref.id);
-        self.update_generics(&mut tref.generics, target, Some(self_path));
+        let self_tref = TraitRef {
+            kind: self_path,
+            trait_decl_ref: RegionBinder::empty(tref.clone()),
+        };
+        self.update_generics(&mut tref.generics, target, Some(self_tref));
     }
 
     /// See `process_trait_decl_ref`.
@@ -1066,22 +1112,12 @@ impl UpdateItemBody<'_> {
             this.process_trait_decl_ref(&mut tref.skip_binder, self_path)
         });
     }
-}
 
-impl VisitAstMut for UpdateItemBody<'_> {
-    // Track binding levels.
-    fn visit_binder<T: AstVisitable>(
-        &mut self,
-        binder: &mut Binder<T>,
-    ) -> ControlFlow<Self::Break> {
-        let generics = &mut binder.params;
-        // An inner binder. Apart from the case of trait method declarations, this is not a
-        // globally-addressable item, so we haven't computed appropriate modifications yet. Hence
-        // we compute them here.
+    fn compute_constraints_for_binder<T>(&self, binder: &Binder<T>) -> TypeConstraintSet {
         let mut type_constraints =
-            TypeConstraintSet::from_constraints(&generics.trait_type_constraints);
+            TypeConstraintSet::from_constraints(&binder.params.trait_type_constraints);
         // Clauses may provide more type constraints.
-        for clause in &generics.trait_clauses {
+        for clause in &binder.params.trait_clauses {
             if let Some(pred) = clause.trait_.skip_binder.clone().move_from_under_binder() {
                 if let Some(tmods) = self.item_modifications.get(&GenericsSource::item(pred.id)) {
                     for (path, ty) in tmods.type_constraints.iter_self_paths_subst(&pred.generics) {
@@ -1091,7 +1127,22 @@ impl VisitAstMut for UpdateItemBody<'_> {
                 }
             }
         }
+        type_constraints
+    }
+}
+
+impl VisitAstMut for UpdateItemBody<'_> {
+    // Track binding levels.
+    fn visit_binder<T: AstVisitable>(
+        &mut self,
+        binder: &mut Binder<T>,
+    ) -> ControlFlow<Self::Break> {
+        // An inner binder. Apart from the case of trait method declarations, this is not a
+        // globally-addressable item, so we haven't computed appropriate modifications yet. Hence
+        // we compute them here.
+        let type_constraints = self.compute_constraints_for_binder(binder);
         let mut modifications = ItemModifications::from_constraint_set(type_constraints, true);
+        let generics = &mut binder.params;
         for clause in &generics.trait_clauses {
             let trait_id = clause.trait_.skip_binder.id;
             if let Some(tmods) = self.item_modifications.get(&GenericsSource::item(trait_id)) {
@@ -1214,7 +1265,7 @@ impl VisitAstMut for UpdateItemBody<'_> {
     fn enter_ty_kind(&mut self, kind: &mut TyKind) {
         if let TyKind::TraitType(tref, name) = kind {
             let path = TraitRefPath::self_ref().with_assoc_type(name.clone());
-            if let Some(new_ty) = self.lookup_path_on_trait_ref(&path, &tref.kind) {
+            if let Some(new_ty) = self.lookup_path_on_trait_ref(&path, tref) {
                 *kind = new_ty.kind().clone();
                 // Fix the newly-substituted type.
                 let _ = self.visit(kind);
@@ -1328,7 +1379,7 @@ impl TransformPass for Transform {
                     }
                     for path in decl_modifs.required_extra_assoc_types() {
                         let new_type_name = TraitItemName(path.to_name());
-                        if let Some((_, ty)) = type_replacements.find(&path) {
+                        if let Some(ty) = type_replacements.find(&path) {
                             trace!("Adding associated type {new_type_name} = {ty:?}");
                             timpl.types.push((
                                 new_type_name.clone(),
diff --git a/charon/src/transform/normalize/transform_dyn_trait_calls.rs b/charon/src/transform/normalize/transform_dyn_trait_calls.rs
new file mode 100644
index 000000000..dfcb29171
--- /dev/null
+++ b/charon/src/transform/normalize/transform_dyn_trait_calls.rs
@@ -0,0 +1,130 @@
+//! Transform method calls on `&dyn Trait` to vtable function pointer calls.
+//!
+//! This pass converts direct method calls on trait objects into calls through vtable
+//! function pointers. For example:
+//!
+//! ```rust,ignore
+//! let x: &dyn Trait = &obj;
+//! x.method(args);
+//! ```
+//!
+//! is transformed from:
+//! ```text
+//! @0 := call <dyn Trait as Trait>::method(x, args)
+//! ```
+//! to:
+//! ```text
+//! @0 := (move (*@receiver.ptr_metadata).method_check)(move (@receiver), move (@args)) // Call through function pointer
+//! ```
+
+use super::super::ctx::UllbcPass;
+use crate::{
+    errors::Error,
+    formatter::IntoFormatter,
+    pretty::FmtWithCtx,
+    raise_error, register_error,
+    transform::{TransformCtx, ctx::UllbcStatementTransformCtx},
+    ullbc_ast::*,
+};
+
+impl<'a> UllbcStatementTransformCtx<'a> {
+    /// Transform a call to a trait method on a dyn trait object
+    fn transform_dyn_trait_call(&mut self, call: &mut Call) -> Result<(), Error> {
+        let fmt_ctx = &self.ctx.into_fmt();
+
+        // Detect if this call should be transformed
+        let FnOperand::Regular(fn_ptr) = &call.func else {
+            return Ok(()); // Not a regular function call
+        };
+        let FnPtrKind::Trait(trait_ref, method_name, _) = &fn_ptr.kind else {
+            return Ok(()); // Not a trait method call
+        };
+        let TraitRefKind::Dyn = &trait_ref.kind else {
+            return Ok(()); // Not a dyn trait trait call
+        };
+        let trait_pred = trait_ref.trait_decl_ref.clone().erase();
+
+        // Get the type of the vtable struct.
+        let vtable_decl_ref: TypeDeclRef = {
+            // Get the trait declaration by its ID
+            let Some(trait_decl) = self.ctx.translated.trait_decls.get(trait_pred.id) else {
+                return Ok(()); // Unknown trait
+            };
+            // Get vtable ref from definition for correct ID.
+            let Some(vtable_ty) = &trait_decl.vtable else {
+                raise_error!(
+                    self.ctx,
+                    self.span,
+                    "Found a `dyn Trait` method call for non-dyn-compatible trait `{}`!",
+                    trait_pred.id.with_ctx(fmt_ctx)
+                );
+            };
+            vtable_ty
+                .clone()
+                .substitute_with_self(&trait_pred.generics, &trait_ref.kind)
+        };
+        let vtable_decl_id = *vtable_decl_ref.id.as_adt().unwrap();
+        let Some(vtable_decl) = self.ctx.translated.type_decls.get(vtable_decl_id) else {
+            return Ok(()); // Missing data
+        };
+
+        // Retreive the method field from the vtable struct definition.
+        let method_field_name = format!("method_{}", method_name);
+        let Some((method_field_id, method_field)) =
+            vtable_decl.get_field_by_name(None, &method_field_name)
+        else {
+            let vtable_name = vtable_decl_ref.id.with_ctx(fmt_ctx).to_string();
+            raise_error!(
+                self.ctx,
+                self.span,
+                "Could not determine method index for {} in vtable {}",
+                method_name,
+                vtable_name
+            );
+        };
+        let method_ty = method_field
+            .ty
+            .clone()
+            .substitute(&vtable_decl_ref.generics);
+
+        // Get the receiver (first argument).
+        if call.args.is_empty() {
+            raise_error!(self.ctx, self.span, "Dyn trait call has no arguments!");
+        }
+        let dyn_trait_place = match &call.args[0] {
+            Operand::Copy(place) | Operand::Move(place) => place,
+            Operand::Const(_) => {
+                panic!("Unexpected constant as receiver for dyn trait method call")
+            }
+        };
+
+        // Construct the `(*ptr.ptr_metadata).method_field` place.
+        let vtable_ty = TyKind::Adt(vtable_decl_ref).into_ty();
+        let ptr_to_vtable_ty = Ty::new(TyKind::RawPtr(vtable_ty.clone(), RefKind::Shared));
+        let method_field_place = dyn_trait_place
+            .clone()
+            .project(ProjectionElem::PtrMetadata, ptr_to_vtable_ty)
+            .project(ProjectionElem::Deref, vtable_ty)
+            .project(
+                ProjectionElem::Field(FieldProjKind::Adt(vtable_decl_id, None), method_field_id),
+                method_ty,
+            );
+
+        // Transform the original call to use the function pointer
+        call.func = FnOperand::Move(method_field_place);
+
+        Ok(())
+    }
+}
+
+pub struct Transform;
+
+impl UllbcPass for Transform {
+    fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
+        decl.transform_ullbc_terminators(ctx, |ctx, term| {
+            if let TerminatorKind::Call { call, .. } = &mut term.kind {
+                let _ = ctx.transform_dyn_trait_call(call);
+            }
+        });
+    }
+}
diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out
index 8495ae7ca..8873b4527 100644
--- a/charon/tests/ui/dyn-trait.out
+++ b/charon/tests/ui/dyn-trait.out
@@ -105,9 +105,9 @@ struct core::ops::function::Fn::{vtable}<Args, Ty0> {
   size: usize,
   align: usize,
   drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)),
-  method_call: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), Args) -> Fn<(dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0), Args>::parent_clause1::parent_clause1::Output,
+  method_call: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), Args) -> Ty0,
   super_trait_0: &'static (core::marker::MetaSized::{vtable}),
-  super_trait_1: &'static (core::ops::function::FnMut::{vtable}<Args, Fn<(dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0), Args>::parent_clause1::parent_clause1::Output>),
+  super_trait_1: &'static (core::ops::function::FnMut::{vtable}<Args, Ty0>),
 }
 
 // Full name: core::ops::function::Fn
diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out
index 9c1cdaf93..e66957f58 100644
--- a/charon/tests/ui/dyn-with-diamond-supertraits.out
+++ b/charon/tests/ui/dyn-with-diamond-supertraits.out
@@ -115,10 +115,10 @@ struct test_crate::Join::{vtable}<T, Ty0, Ty1, Ty2, Ty3> {
   size: usize,
   align: usize,
   drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3)),
-  method_join_method: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3))) -> (Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3), T>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3), T>::parent_clause2::Right),
+  method_join_method: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3))) -> (Ty3, Ty2),
   super_trait_0: &'static (core::marker::MetaSized::{vtable}),
-  super_trait_1: &'static (test_crate::Left::{vtable}<Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3), T>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3), T>::parent_clause1::parent_clause1::Internal>),
-  super_trait_2: &'static (test_crate::Right::{vtable}<T, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3), T>::parent_clause2::Right, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, T> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty0 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = Ty1 + @TraitClause1_0::parent_clause2::Right = Ty2 + @TraitClause1_0::parent_clause1::Left = Ty3), T>::parent_clause1::parent_clause1::Internal>),
+  super_trait_1: &'static (test_crate::Left::{vtable}<Ty3, Ty1>),
+  super_trait_2: &'static (test_crate::Right::{vtable}<T, Ty2, Ty1>),
 }
 
 // Full name: test_crate::Join
@@ -319,9 +319,9 @@ fn {impl Join<i32> for i32}::{vtable}() -> test_crate::Join::{vtable}<i32, i32,
 {
     let ret@0: test_crate::Join::{vtable}<i32, i32, i32, i32, i32>; // return
     let @1: (); // anonymous local
-    let @2: &'static (test_crate::Left::{vtable}<Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::Left, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local
+    let @2: &'static (test_crate::Left::{vtable}<i32, i32>); // anonymous local
     let @3: (); // anonymous local
-    let @4: &'static (test_crate::Right::{vtable}<i32, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause2::Right, Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::parent_clause1::parent_clause1::Internal>); // anonymous local
+    let @4: &'static (test_crate::Right::{vtable}<i32, i32, i32>); // anonymous local
 
     storage_live(@1)
     @1 := ()
@@ -373,7 +373,7 @@ fn main()
     storage_live(@5)
     storage_live(@6)
     @6 := &*(v@1) with_metadata(copy (v@1.metadata))
-    @5 := Join<(dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32), i32>::join_method<'_>(move (@6))
+    @5 := (move (*(@6.metadata)).method_join_method)(move (@6))
     storage_dead(@6)
     storage_dead(@5)
     @0 := ()
diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out
index 2056b680f..06b817fbf 100644
--- a/charon/tests/ui/simple/dyn-fn.out
+++ b/charon/tests/ui/simple/dyn-fn.out
@@ -63,9 +63,9 @@ struct core::ops::function::Fn::{vtable}<Args, Ty0> {
   size: usize,
   align: usize,
   drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)),
-  method_call: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), Args) -> Fn<(dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0), Args>::parent_clause1::parent_clause1::Output,
+  method_call: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0)), Args) -> Ty0,
   super_trait_0: &'static (core::marker::MetaSized::{vtable}),
-  super_trait_1: &'static (core::ops::function::FnMut::{vtable}<Args, Fn<(dyn exists<_dyn> [@TraitClause0]: Fn<_dyn, Args> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Output = Ty0), Args>::parent_clause1::parent_clause1::Output>),
+  super_trait_1: &'static (core::ops::function::FnMut::{vtable}<Args, Ty0>),
 }
 
 // Full name: core::ops::function::Fn
@@ -126,7 +126,7 @@ fn takes_fn<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (
     @7 := &mut counter@2
     @6 := &two-phase-mut *(@7)
     @5 := (move (@6))
-    @3 := Fn<(dyn exists<_dyn> [@TraitClause0]: for<'a> Fn<_dyn, (&'a mut (u32))> + _dyn : '_ + for<'a> @TraitClause1_0::parent_clause1::parent_clause1::Output = bool), (&'_ mut (u32))>::call<'_>(move (@4), move (@5))
+    @3 := (move (*(@4.metadata)).method_call)(move (@4), move (@5))
     if move (@3) {
         storage_dead(@7)
         storage_dead(@6)
diff --git a/charon/tests/ui/simple/impl-with-dyn-assoc-ty.out b/charon/tests/ui/simple/impl-with-dyn-assoc-ty.out
new file mode 100644
index 000000000..92f19088e
--- /dev/null
+++ b/charon/tests/ui/simple/impl-with-dyn-assoc-ty.out
@@ -0,0 +1,58 @@
+# 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
+}
+
+fn UNIT_METADATA()
+{
+    let @0: (); // return
+
+    @0 := ()
+    return
+}
+
+const UNIT_METADATA: () = @Fun0()
+
+struct test_crate::DynableTrait::{vtable}<Ty0> {
+  size: usize,
+  align: usize,
+  drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: DynableTrait<_dyn, Ty0> + _dyn : '_)),
+  super_trait_0: &'static (core::marker::MetaSized::{vtable}),
+}
+
+// Full name: test_crate::DynableTrait
+trait DynableTrait<Self, Self_DynableTraitType>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: Sized<Self_DynableTraitType>
+    vtable: test_crate::DynableTrait::{vtable}<Self_DynableTraitType>
+}
+
+// Full name: test_crate::Trait
+trait Trait<Self, Self_TraitType, Self_Clause2_DynableTraitType>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: MetaSized<Self_TraitType>
+    parent_clause2 : [@TraitClause2]: DynableTrait<Self_TraitType, Self_Clause2_DynableTraitType>
+    vtable: test_crate::Trait::{vtable}<Self_TraitType>
+}
+
+// Full name: test_crate::{impl Trait<(dyn exists<_dyn> [@TraitClause0]: DynableTrait<_dyn, ()> + _dyn : 'static), ()> for ()}
+impl Trait<(dyn exists<_dyn> [@TraitClause0]: DynableTrait<_dyn, ()> + _dyn : 'static), ()> for () {
+    parent_clause0 = MetaSized<()>
+    parent_clause1 = MetaSized<(dyn exists<_dyn> [@TraitClause0]: DynableTrait<_dyn, ()> + _dyn : '_)>
+    parent_clause2 = DynableTrait<(dyn exists<_dyn> [@TraitClause0]: DynableTrait<_dyn, ()> + _dyn : '_), ()>
+    vtable: {impl Trait<(dyn exists<_dyn> [@TraitClause0]: DynableTrait<_dyn, ()> + _dyn : 'static), ()> for ()}::{vtable}
+}
+
+
+
diff --git a/charon/tests/ui/simple/impl-with-dyn-assoc-ty.rs b/charon/tests/ui/simple/impl-with-dyn-assoc-ty.rs
new file mode 100644
index 000000000..2db1c5688
--- /dev/null
+++ b/charon/tests/ui/simple/impl-with-dyn-assoc-ty.rs
@@ -0,0 +1,12 @@
+//@ charon-args=--remove-associated-types=*
+trait DynableTrait {
+    type DynableTraitType;
+}
+
+trait Trait {
+    type TraitType: DynableTrait + ?Sized;
+}
+
+impl Trait for () {
+    type TraitType = dyn DynableTrait<DynableTraitType = ()>;
+}
diff --git a/charon/tests/ui/vtable-simple.out b/charon/tests/ui/vtable-simple.out
new file mode 100644
index 000000000..fe2b69230
--- /dev/null
+++ b/charon/tests/ui/vtable-simple.out
@@ -0,0 +1,212 @@
+# 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::clone::Clone
+#[lang_item("clone")]
+pub trait Clone<Self>
+{
+    parent_clause0 : [@TraitClause0]: Sized<Self>
+    fn clone<'_0> = core::clone::Clone::clone<'_0_0, Self>[Self]
+    non-dyn-compatible
+}
+
+#[lang_item("clone_fn")]
+pub fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self
+where
+    [@TraitClause0]: Clone<Self>,
+
+// Full name: core::clone::impls::{impl Clone for i32}::clone
+pub fn {impl Clone for i32}::clone<'_0>(@1: &'_0 (i32)) -> i32
+
+// Full name: core::clone::impls::{impl Clone for i32}
+impl Clone for i32 {
+    parent_clause0 = Sized<i32>
+    fn clone<'_0> = {impl Clone for i32}::clone<'_0_0>
+    non-dyn-compatible
+}
+
+// Full name: core::marker::Destruct
+#[lang_item("destruct")]
+pub trait Destruct<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    vtable: core::marker::Destruct::{vtable}
+}
+
+fn UNIT_METADATA()
+{
+    let @0: (); // return
+
+    @0 := ()
+    return
+}
+
+const UNIT_METADATA: () = @Fun0()
+
+struct test_crate::Modifiable::{vtable}<T> {
+  size: usize,
+  align: usize,
+  drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)),
+  method_modify: fn<'_0, '_1>(&'_0_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)), &'_0_1 (T)) -> T,
+  super_trait_0: &'static (core::marker::MetaSized::{vtable}),
+}
+
+// Full name: test_crate::Modifiable
+trait Modifiable<Self, T>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    parent_clause1 : [@TraitClause1]: Sized<T>
+    fn modify<'_0, '_1> = test_crate::Modifiable::modify<'_0_0, '_0_1, Self, T>[Self]
+    vtable: test_crate::Modifiable::{vtable}<T>
+}
+
+fn test_crate::Modifiable::modify<'_0, '_1, Self, T>(@1: &'_0 mut (Self), @2: &'_1 (T)) -> T
+where
+    [@TraitClause0]: Modifiable<Self, T>,
+
+// Full name: test_crate::{impl Modifiable<T> for i32}::modify
+fn {impl Modifiable<T> for i32}::modify<'_0, '_1, T>(@1: &'_0 mut (i32), @2: &'_1 (T)) -> T
+where
+    [@TraitClause0]: Sized<T>,
+    [@TraitClause1]: Clone<T>,
+{
+    let @0: T; // return
+    let self@1: &'_ mut (i32); // arg #1
+    let arg@2: &'_ (T); // arg #2
+    let @3: i32; // anonymous local
+    let @4: &'_ (T); // anonymous local
+
+    storage_live(@3)
+    @3 := copy (*(self@1)) panic.+ const (1 : i32)
+    *(self@1) := move (@3)
+    storage_live(@4)
+    @4 := &*(arg@2)
+    @0 := @TraitClause1::clone<'_>(move (@4))
+    storage_dead(@4)
+    return
+}
+
+// Full name: test_crate::{impl Modifiable<T> for i32}::modify::{vtable_method}
+fn {vtable_method}<'_0, '_1, T>(@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)), @2: &'_1 (T)) -> T
+where
+    [@TraitClause0]: Sized<T>,
+    [@TraitClause1]: Clone<T>,
+{
+    let @0: T; // return
+    let @1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)); // arg #1
+    let @2: &'_1 (T); // arg #2
+    let @3: &'_0 mut (i32); // anonymous local
+
+    storage_live(@3)
+    @3 := concretize<&'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)), &'_0 mut (i32)>(move (@1))
+    @0 := {impl Modifiable<T> for i32}::modify<'_0, '_1, T>[@TraitClause0, @TraitClause1](move (@3), move (@2))
+    return
+}
+
+// Full name: test_crate::{impl Modifiable<T> for i32}::{vtable}
+fn {impl Modifiable<T> for i32}::{vtable}<T>() -> test_crate::Modifiable::{vtable}<T>
+where
+    [@TraitClause0]: Sized<T>,
+    [@TraitClause1]: Clone<T>,
+{
+    let ret@0: test_crate::Modifiable::{vtable}<T>; // return
+
+    ret@0 := test_crate::Modifiable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_modify: const ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) }
+    return
+}
+
+// Full name: test_crate::{impl Modifiable<T> for i32}::{vtable}
+static {impl Modifiable<T> for i32}::{vtable}<T>: test_crate::Modifiable::{vtable}<T>
+where
+    [@TraitClause0]: Sized<T>,
+    [@TraitClause1]: Clone<T>,
+ = {impl Modifiable<T> for i32}::{vtable}()
+
+// Full name: test_crate::{impl Modifiable<T> for i32}
+impl<T> Modifiable<T> for i32
+where
+    [@TraitClause0]: Sized<T>,
+    [@TraitClause1]: Clone<T>,
+{
+    parent_clause0 = MetaSized<i32>
+    parent_clause1 = @TraitClause0
+    fn modify<'_0, '_1> = {impl Modifiable<T> for i32}::modify<'_0_0, '_0_1, T>[@TraitClause0, @TraitClause1]
+    vtable: {impl Modifiable<T> for i32}::{vtable}<T>[@TraitClause0, @TraitClause1]
+}
+
+// Full name: test_crate::modify_trait_object
+fn modify_trait_object<'_0, T>(@1: &'_0 (T)) -> T
+where
+    [@TraitClause0]: Sized<T>,
+    [@TraitClause1]: Clone<T>,
+{
+    let @0: T; // return
+    let arg@1: &'_ (T); // arg #1
+    let x@2: &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)); // local
+    let @3: &'_ mut (i32); // anonymous local
+    let @4: &'_ mut (i32); // anonymous local
+    let @5: i32; // anonymous local
+    let @6: &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)); // anonymous local
+    let @7: &'_ (T); // anonymous local
+
+    storage_live(x@2)
+    storage_live(@3)
+    storage_live(@4)
+    storage_live(@5)
+    @5 := const (199 : i32)
+    @4 := &mut @5
+    @3 := &mut *(@4)
+    x@2 := unsize_cast<&'_ mut (i32), &'_ mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)), {impl Modifiable<T> for i32}<T>[@TraitClause0, @TraitClause1]>(move (@3))
+    storage_dead(@3)
+    storage_dead(@4)
+    storage_live(@6)
+    @6 := &two-phase-mut *(x@2) with_metadata(copy (x@2.metadata))
+    storage_live(@7)
+    @7 := &*(arg@1)
+    @0 := (move (*(@6.metadata)).method_modify)(move (@6), move (@7))
+    storage_dead(@7)
+    storage_dead(@6)
+    storage_dead(@5)
+    storage_dead(x@2)
+    return
+}
+
+// Full name: test_crate::main
+fn main()
+{
+    let @0: (); // return
+    let @1: i32; // anonymous local
+    let @2: &'_ (i32); // anonymous local
+    let @3: &'_ (i32); // anonymous local
+    let @4: i32; // anonymous local
+
+    @0 := ()
+    storage_live(@1)
+    storage_live(@2)
+    storage_live(@3)
+    storage_live(@4)
+    @4 := const (42 : i32)
+    @3 := &@4
+    @2 := &*(@3)
+    @1 := modify_trait_object<'_, i32>[Sized<i32>, {impl Clone for i32}](move (@2))
+    storage_dead(@2)
+    storage_dead(@4)
+    storage_dead(@3)
+    storage_dead(@1)
+    @0 := ()
+    return
+}
+
+
+
diff --git a/charon/tests/ui/vtable-simple.rs b/charon/tests/ui/vtable-simple.rs
new file mode 100644
index 000000000..f20210092
--- /dev/null
+++ b/charon/tests/ui/vtable-simple.rs
@@ -0,0 +1,17 @@
+trait Modifiable<T> {
+    fn modify(&mut self, arg: &T) -> T;
+}
+impl<T: Clone> Modifiable<T> for i32 {
+    fn modify(&mut self, arg: &T) -> T {
+        *self += 1;
+        arg.clone()
+    }
+}
+fn modify_trait_object<T: Clone>(arg: &T) -> T {
+    let x: &mut dyn Modifiable<T> = &mut 199;
+    x.modify(arg)
+}
+
+fn main() {
+    modify_trait_object(&42);
+}
\ No newline at end of file
diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out
index fd6faa45e..49c9b8d8b 100644
--- a/charon/tests/ui/vtables.out
+++ b/charon/tests/ui/vtables.out
@@ -504,7 +504,7 @@ where
     @6 := &two-phase-mut *(x@2) with_metadata(copy (x@2.metadata))
     storage_live(@7)
     @7 := &*(arg@1)
-    @0 := Modifiable<(dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_), T>::modify<'_, '_>(move (@6), move (@7))
+    @0 := (move (*(@6.metadata)).method_modify)(move (@6), move (@7))
     storage_dead(@7)
     storage_dead(@6)
     storage_dead(@5)
@@ -747,7 +747,7 @@ struct test_crate::LifetimeTrait::{vtable}<Ty0> {
   size: usize,
   align: usize,
   drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)),
-  method_lifetime_method: fn<'a, '_1>(&'_0_1 ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)), &'a (LifetimeTrait<(dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)>::Ty)) -> &'a (LifetimeTrait<(dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)>::Ty),
+  method_lifetime_method: fn<'a, '_1>(&'_0_1 ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)), &'a (Ty0)) -> &'a (Ty0),
   super_trait_0: &'static (core::marker::MetaSized::{vtable}),
 }
 
@@ -845,7 +845,7 @@ fn use_lifetime_trait<'a, '_1>(@1: &'_1 ((dyn exists<_dyn> [@TraitClause0]: Life
     @4 := &*(x@1) with_metadata(copy (x@1.metadata))
     storage_live(@5)
     @5 := &*(y@2)
-    @3 := LifetimeTrait<(dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)>::lifetime_method<'_, '_>(move (@4), move (@5))
+    @3 := (move (*(@4.metadata)).method_lifetime_method)(move (@4), move (@5))
     @0 := &*(@3)
     storage_dead(@5)
     storage_dead(@4)
@@ -883,7 +883,7 @@ fn use_alias<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Both32And64<_dyn>
     @9 := const (200 : i64)
     @8 := &@9
     @7 := &*(@8)
-    @2 := Both32And64<(dyn exists<_dyn> [@TraitClause0]: Both32And64<_dyn> + _dyn : '_)>::both_operate<'_, '_, '_>(move (@3), move (@4), move (@7))
+    @2 := (move (*(@3.metadata)).method_both_operate)(move (@3), move (@4), move (@7))
     storage_dead(@7)
     storage_dead(@4)
     storage_dead(@3)
@@ -1000,7 +1000,7 @@ fn main()
     storage_live(@5)
     storage_live(@6)
     @6 := &*(x@1) with_metadata(copy (x@1.metadata))
-    @5 := Checkable<(dyn exists<_dyn> [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_), i32>::check<'_>(move (@6))
+    @5 := (move (*(@6.metadata)).method_check)(move (@6))
     if move (@5) {
     }
     else {
@@ -1059,7 +1059,7 @@ fn main()
         @25 := const (100 : i32)
         @24 := &mut @25
         @23 := &*(@24)
-        @21 := Modifiable<(dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, i32> + _dyn : '_), i32>::modify<'_, '_>(move (@22), move (@23))
+        @21 := (move (*(@22.metadata)).method_modify)(move (@22), move (@23))
         storage_dead(@23)
         storage_dead(@22)
         @20 := &@21
@@ -1131,7 +1131,7 @@ fn main()
         storage_live(@46)
         storage_live(@47)
         @47 := &*(z@40) with_metadata(copy (z@40.metadata))
-        @46 := NoParam<(dyn exists<_dyn> [@TraitClause0]: NoParam<_dyn> + _dyn : '_)>::dummy<'_>(move (@47))
+        @46 := (move (*(@47.metadata)).method_dummy)(move (@47))
         storage_dead(@47)
         storage_dead(@46)
         storage_live(a@48)
@@ -1159,7 +1159,7 @@ fn main()
         @59 := const (200 : i64)
         @58 := &@59
         @57 := &*(@58)
-        @52 := Both32And64<(dyn exists<_dyn> [@TraitClause0]: Both32And64<_dyn> + _dyn : '_)>::both_operate<'_, '_, '_>(move (@53), move (@54), move (@57))
+        @52 := (move (*(@53.metadata)).method_both_operate)(move (@53), move (@54), move (@57))
         storage_dead(@57)
         storage_dead(@54)
         storage_dead(@53)