diff --git a/Makefile b/Makefile
index 873b380..e68bf86 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 CHARON_HOME 	?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../charon
 KRML_HOME 	?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel
 EURYDICE	?= ./eurydice $(EURYDICE_FLAGS)
-CHARON		?= $(CHARON_HOME)/bin/charon --extract-opaque-bodies
+CHARON		?= $(CHARON_HOME)/bin/charon
 
 BROKEN_TESTS		= step_by where_clauses chunks mutable_slice_range closure
 TEST_DIRS		= $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxdepth 1 -mindepth 1 -type d)))
diff --git a/flake.lock b/flake.lock
index 293952b..1589425 100644
--- a/flake.lock
+++ b/flake.lock
@@ -11,11 +11,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1723650722,
-        "narHash": "sha256-B0nZV4o+ATb0/TS3AXl6KooL7+GTyrXWXQVoGWgtuaw=",
-        "owner": "AeneasVerif",
+        "lastModified": 1724239793,
+        "narHash": "sha256-aiR5BVfWpkzZWR1WZbMhqcuDAvznV5fq2nBDCqQEczc=",
+        "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "8de6020c10a3520a56fbf849176f8218e62435cf",
+        "rev": "9e782beeb099f447661ce91da9ba1181a94642fe",
         "type": "github"
       },
       "original": {
@@ -246,11 +246,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1723429325,
-        "narHash": "sha256-4x/32xTCd+xCwFoI/kKSiCr5LQA2ZlyTRYXKEni5HR8=",
+        "lastModified": 1724206841,
+        "narHash": "sha256-L8dKaX4T3k+TR2fEHCfGbH4UXdspovz/pj87iai9qmc=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "65e3dc0fe079fe8df087cd38f1fe6836a0373aad",
+        "rev": "45e98fbd62c32e5927e952d2833fa1ba4fb35a61",
         "type": "github"
       },
       "original": {
diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
index bd052e3..61e6b0b 100644
--- a/lib/AstOfLlbc.ml
+++ b/lib/AstOfLlbc.ml
@@ -750,22 +750,7 @@ let rec build_trait_clause_mapping env (trait_clauses : C.trait_clause list) =
             in
             ( (C.Clause clause_id, item_name),
               (decl_generics, ts, trait_decl.C.item_meta.name, decl.C.signature) ))
-          trait_decl.C.required_methods
-        @ List.map
-            (fun (item_name, decl_id) ->
-              match decl_id with
-              | Some decl_id ->
-                  let decl = env.get_nth_function decl_id in
-                  let ts =
-                    {
-                      K.n = List.length trait_decl.generics.types;
-                      n_cgs = List.length trait_decl.generics.const_generics;
-                    }
-                  in
-                  ( (C.Clause clause_id, item_name),
-                    (decl_generics, ts, trait_decl.C.item_meta.name, decl.C.signature) )
-              | None -> failwith ("TODO: handle provided trait methods, like " ^ item_name))
-            trait_decl.C.provided_methods
+          (trait_decl.C.required_methods @ trait_decl.C.provided_methods)
         @ List.flatten
             (List.mapi
                (fun i (parent_clause : C.trait_clause) ->