diff --git a/src/Translate.ml b/src/Translate.ml
index d24bf3751..c88d242e0 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -754,24 +754,26 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
 let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
     (ctx : gen_ctx) (trait_impl_id : Pure.trait_impl_id) : unit =
   (* Lookup the definition *)
-  let trait_impl = TraitImplId.Map.find trait_impl_id ctx.trans_trait_impls in
-  let trait_decl =
-    Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
-      ctx.trans_trait_decls
-  in
-  (* Check if the trait implementation is builtin *)
-  let builtin_info =
-    let open ExtractBuiltin in
-    let trait_impl =
-      TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
+  match TraitImplId.Map.find_opt trait_impl_id ctx.trans_trait_impls with
+  | None -> ()
+  | Some trait_impl ->
+    let trait_decl =
+      Pure.TraitDeclId.Map.find trait_impl.impl_trait.trait_decl_id
+        ctx.trans_trait_decls
     in
-    match_name_with_generics_find_opt ctx.trans_ctx trait_decl.item_meta.name
-      trait_impl.impl_trait.decl_generics
-      (builtin_trait_impls_map ())
-  in
-  match builtin_info with
-  | None -> Extract.extract_trait_impl ctx fmt trait_impl
-  | Some _ -> ()
+    (* Check if the trait implementation is builtin *)
+    let builtin_info =
+      let open ExtractBuiltin in
+      let trait_impl =
+        TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
+      in
+      match_name_with_generics_find_opt ctx.trans_ctx trait_decl.item_meta.name
+        trait_impl.impl_trait.decl_generics
+        (builtin_trait_impls_map ())
+    in
+    match builtin_info with
+    | None -> Extract.extract_trait_impl ctx fmt trait_impl
+    | Some _ -> ()
 
 (** A generic utility to generate the extracted definitions: as we may want to
     split the definitions between different files (or not), we can control
diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml
index 68e2f0a71..d8c50d1a0 100644
--- a/src/extract/Extract.ml
+++ b/src/extract/Extract.ml
@@ -2382,9 +2382,11 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
         let funs_map = StringMap.of_list info.methods in
         List.map
           (fun (item_name, _) ->
-            let info = StringMap.find item_name funs_map in
-            let fun_name = info.extract_name in
-            (item_name, fun_name))
+            match StringMap.find_opt item_name funs_map with
+            | Some info ->
+              let fun_name = info.extract_name in
+              (item_name, fun_name)
+            | None -> craise __FILE__ __LINE__ trait_decl.item_meta.span ("Could not find: " ^ item_name))
           methods
   in
   (* Register the names *)
diff --git a/src/interp/Interpreter.ml b/src/interp/Interpreter.ml
index c68714d78..2fbaf2865 100644
--- a/src/interp/Interpreter.ml
+++ b/src/interp/Interpreter.ml
@@ -45,7 +45,9 @@ let compute_contexts (crate : crate) : decls_ctx =
        let ids = g_declaration_group_to_list g in
        let decls = List.map any_decl_id_to_string ids in
        let local_requires =
+       try
          LlbcAstUtils.find_local_transitive_dep crate (AnyDeclIdSet.of_list ids)
+         with _ -> []
        in
        let local_requires = List.map span_to_string local_requires in
        let local_requires =