diff --git a/charon-pin b/charon-pin
index fbf6f69f5..9acddcbee 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-b5dae67bb637d80ce61d8232df656ee7e243d6eb
+637a6bc8a4c2a79875af5aa4e413c7ef3aa7f391
diff --git a/flake.lock b/flake.lock
index b460a4001..1207b7a8a 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1763648393,
-        "narHash": "sha256-qMW1RmpjnzKHgNXDaNJnuHxC1YfmStwAeqmVL9pk3hs=",
+        "lastModified": 1764078511,
+        "narHash": "sha256-ZI/5ynYf/2zKNQaRJbKwyePpBcraqv1flbgRgcYfvDc=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "b5dae67bb637d80ce61d8232df656ee7e243d6eb",
+        "rev": "637a6bc8a4c2a79875af5aa4e413c7ef3aa7f391",
         "type": "github"
       },
       "original": {
@@ -158,17 +158,17 @@
         ]
       },
       "locked": {
-        "lastModified": 1762569282,
-        "narHash": "sha256-vINZAJpXQTZd5cfh06Rcw7hesH7sGSvi+Tn+HUieJn8=",
+        "lastModified": 1763952169,
+        "narHash": "sha256-+PeDBD8P+NKauH+w7eO/QWCIp8Cx4mCfWnh9sJmy9CM=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "a35a6144b976f70827c2fe2f5c89d16d8f9179d8",
+        "rev": "ab726555a9a72e6dc80649809147823a813fa95b",
         "type": "github"
       },
       "original": {
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "a35a6144b976f70827c2fe2f5c89d16d8f9179d8",
+        "rev": "ab726555a9a72e6dc80649809147823a813fa95b",
         "type": "github"
       }
     },
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 1463cfdab..b04155c1b 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -9,12 +9,12 @@ Local Open Scope Primitives_scope.
 Module Demo.
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2300:8-2300:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2315:8-2315:58
     Name pattern: [core::num::{u32}::wrapping_add] *)
 Axiom core_num_U32_wrapping_add : u32 -> u32 -> result u32.
 
 (** [core::num::{u32}::wrapping_sub]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2337:8-2337:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2352:8-2352:58
     Name pattern: [core::num::{u32}::wrapping_sub] *)
 Axiom core_num_U32_wrapping_sub : u32 -> u32 -> result u32.
 
diff --git a/tests/coq/misc/Traits.v b/tests/coq/misc/Traits.v
index 150dd3196..bdb304ed9 100644
--- a/tests/coq/misc/Traits.v
+++ b/tests/coq/misc/Traits.v
@@ -664,7 +664,7 @@ Definition TraittraitsWrapper {T : Type} (traitInst : Trait_t T) : Trait_t
 (** [traits::use_wrapper_len]:
     Source: 'tests/src/traits.rs', lines 324:0-326:1 *)
 Definition use_wrapper_len {T : Type} (traitInst : Trait_t T) : result usize :=
-  Ok (TraittraitsWrapper traitInst).(Trait_tTrait_t_LEN)
+  Ok (traittraits_wrapper_len traitInst)
 .
 
 (** [traits::Foo]
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index 2635d9563..4fc975be7 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -6,12 +6,12 @@ open Primitives
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
 (** [core::num::{u32}::wrapping_add]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2300:8-2300:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2315:8-2315:58
     Name pattern: [core::num::{u32}::wrapping_add] *)
 assume val core_num_U32_wrapping_add : u32 -> u32 -> result u32
 
 (** [core::num::{u32}::wrapping_sub]:
-    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2337:8-2337:58
+    Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2352:8-2352:58
     Name pattern: [core::num::{u32}::wrapping_sub] *)
 assume val core_num_U32_wrapping_sub : u32 -> u32 -> result u32
 
diff --git a/tests/fstar/misc/Traits.fst b/tests/fstar/misc/Traits.fst
index 1fcef1fc5..948277a00 100644
--- a/tests/fstar/misc/Traits.fst
+++ b/tests/fstar/misc/Traits.fst
@@ -525,7 +525,7 @@ let traittraitsWrapper (#t : Type0) (traitInst : trait_t t) : trait_t
 (** [traits::use_wrapper_len]:
     Source: 'tests/src/traits.rs', lines 324:0-326:1 *)
 let use_wrapper_len (#t : Type0) (traitInst : trait_t t) : result usize =
-  Ok (traittraitsWrapper traitInst).cLEN
+  Ok (traittraits_wrapper_len traitInst)
 
 (** [traits::Foo]
     Source: 'tests/src/traits.rs', lines 328:0-331:1 *)
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index ee0a9964c..efbe5ff1f 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -543,7 +543,7 @@ def TraittraitsWrapper {T : Type} (TraitInst : Trait T) : Trait (Wrapper T)
 /- [traits::use_wrapper_len]:
    Source: 'tests/src/traits.rs', lines 324:0-326:1 -/
 def use_wrapper_len {T : Type} (TraitInst : Trait T) : Result Usize := do
-  ok (TraittraitsWrapper TraitInst).LEN
+  ok (TraittraitsWrapper.LEN TraitInst)
 
 /- [traits::Foo]
    Source: 'tests/src/traits.rs', lines 328:0-331:1 -/