diff --git a/charon/Cargo.lock b/charon/Cargo.lock
index bde0e636f..41cf37791 100644
--- a/charon/Cargo.lock
+++ b/charon/Cargo.lock
@@ -807,7 +807,7 @@ checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1"
 [[package]]
 name = "hax-adt-into"
 version = "0.3.4"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#5820a126375d41aeb89c508e94577125882eb978"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#193c439128a22a124ca3745c9836fbcd2a63e53b"
 dependencies = [
  "itertools 0.11.0",
  "proc-macro2",
@@ -818,7 +818,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter"
 version = "0.3.4"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#5820a126375d41aeb89c508e94577125882eb978"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#193c439128a22a124ca3745c9836fbcd2a63e53b"
 dependencies = [
  "extension-traits",
  "hax-adt-into",
@@ -835,7 +835,7 @@ dependencies = [
 [[package]]
 name = "hax-frontend-exporter-options"
 version = "0.3.4"
-source = "git+https://github.com/AeneasVerif/hax?branch=main#5820a126375d41aeb89c508e94577125882eb978"
+source = "git+https://github.com/AeneasVerif/hax?branch=main#193c439128a22a124ca3745c9836fbcd2a63e53b"
 dependencies = [
  "hax-adt-into",
  "schemars",
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 d027d094c..cd6dc366d 100644
--- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs
+++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs
@@ -225,7 +225,7 @@ impl ItemTransCtx<'_, '_> {
         )?;
         let hax::FullDefKind::AssocFn {
             sig,
-            vtable_safe: true,
+            vtable_sig: Some(_),
             ..
         } = item_def.kind()
         else {
@@ -234,7 +234,7 @@ impl ItemTransCtx<'_, '_> {
 
         let item_name = self.t_ctx.translate_trait_item_name(item_def_id)?;
         // It's ok to translate the method signature in the context of the trait because
-        // `vtable_safe: true` ensures the method has no generics of its own.
+        // `vtable_sig: Some(_)` ensures the method has no generics of its own.
         let sig = self.translate_fun_sig(span, sig)?;
         let ty = TyKind::FnPtr(sig).into_ty();
 
@@ -535,7 +535,8 @@ impl ItemTransCtx<'_, '_> {
         // Exit if the item isn't a vtable safe method.
         match self.poly_hax_def(&item.decl_def_id)?.kind() {
             hax::FullDefKind::AssocFn {
-                vtable_safe: true, ..
+                vtable_sig: Some(_),
+                ..
             } => {}
             _ => return Ok(()),
         }
diff --git a/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.out b/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.out
new file mode 100644
index 000000000..7ecc8faef
--- /dev/null
+++ b/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.out
@@ -0,0 +1,49 @@
+# Final LLBC before serialization:
+
+// Full name: core::marker::MetaSized
+#[lang_item("meta_sized")]
+pub trait MetaSized<Self>
+
+fn UNIT_METADATA()
+{
+    let @0: (); // return
+
+    @0 := ()
+    return
+}
+
+const UNIT_METADATA: () = @Fun0()
+
+struct test_crate::Trait::{vtable} {
+  size: usize,
+  align: usize,
+  drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: Trait<_dyn> + _dyn : '_)),
+  method_foo: fn<'_0>(&'_0_0 ((dyn exists<_dyn> [@TraitClause0]: Trait<_dyn> + _dyn : '_))),
+  super_trait_0: &'static (core::marker::MetaSized::{vtable}),
+}
+
+// Full name: test_crate::Trait
+trait Trait<Self>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized<Self>
+    fn foo<'a, '_1, Self : 'a> = test_crate::Trait::foo<'a, '_0_1, Self>[Self]
+    vtable: test_crate::Trait::{vtable}
+}
+
+fn test_crate::Trait::foo<'a, '_1, Self>(@1: &'_1 (Self))
+where
+    [@TraitClause0]: Trait<Self>,
+    Self : 'a,
+
+fn test_crate::foo<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Trait<_dyn> + _dyn : '_0)))
+{
+    let @0: (); // return
+    let x@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: Trait<_dyn> + _dyn : '_)); // arg #1
+
+    @0 := ()
+    @0 := ()
+    return
+}
+
+
+
diff --git a/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.rs b/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.rs
new file mode 100644
index 000000000..d3b2004b6
--- /dev/null
+++ b/charon/tests/ui/simple/dyn-method-with-early-bound-lifetimes.rs
@@ -0,0 +1,7 @@
+trait Trait {
+    fn foo<'a>(&self)
+    where
+        Self: 'a;
+}
+
+fn foo(x: &dyn Trait) {}