diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index c255a3c6a8709e28d1f43d2d8fe42947ebae5fcc..9a4e778256848b45afbd0ea3e2c6d5733fcf1ecb 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -539,11 +539,23 @@ module Extensions = struct
     end
 
   let typer name ~typing_context:typing_context ~loc p =
+    let status,typer =
+      try find_typer name
+      with Not_found ->
+        Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
+    in
+    let normal_error = ref false in
+    let has_error () = normal_error := true in
+    let wrapper =
+      typing_context.on_error (typer ~typing_context ~loc) has_error
+    in
     try
-      let status,typer = find_typer name in
-      status, typer ~typing_context ~loc p
-    with Not_found ->
-      Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
+      status, wrapper p
+    with
+    | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
+    | exn when not !normal_error ->
+      Kernel.fatal "Typechecking ACSL extension %s raised exception %s"
+        name (Printexc.to_string exn)
 end
 
 let register_behavior_extension name f =
diff --git a/tests/spec/extend_extern.i b/tests/spec/extend_extern.i
new file mode 100644
index 0000000000000000000000000000000000000000..c3c61836044e2aa33369d00e439c5806eff9e106
--- /dev/null
+++ b/tests/spec/extend_extern.i
@@ -0,0 +1,6 @@
+/* run.config
+   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT:
+ */
+/*@ predicate load(char * x) = \true ; */
+/*@ why3 load("List"); */
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c60a714b9bf921abd03047c7e87337548365b108
--- /dev/null
+++ b/tests/spec/extend_extern.ml
@@ -0,0 +1,36 @@
+open Logic_typing
+open Cil_types
+
+let load_theory = function
+  | { pred_content = Papp (_, [], [ { term_node = TConst(LStr _name) } ] ) } ->
+    raise Not_found
+  | _ -> assert false
+
+let typing ~typing_context ~loc lexprs =
+  ignore loc ;
+  let type_predicate =
+    typing_context.type_predicate typing_context (Lenv.empty ())
+  in
+  let predicates = List.map type_predicate lexprs in
+  List.iter load_theory predicates ;
+  Ext_preds predicates
+
+
+let () =
+  Logic_typing.register_global_extension "why3" false typing
+
+let main () =
+  try
+    Kernel.feedback
+      "Checking handler of exception occurring in extension typing";
+    Ast.compute (); assert false
+  with
+    | Log.AbortFatal _ -> Kernel.feedback "Extension typing failed as expected"
+    | Not_found -> Kernel.fatal "kernel did not capture our exception"
+    | Assert_failure _ -> Kernel.fatal "kernel silently captured our exception"
+
+let () = Kernel.TypeCheck.set false
+
+let () = Kernel.Debug.set 1
+
+let () = Db.Main.extend main
diff --git a/tests/spec/oracle/extend_extern.res.oracle b/tests/spec/oracle/extend_extern.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3b7533295bbd2465e6b234f1ed957310f2e3e77e
--- /dev/null
+++ b/tests/spec/oracle/extend_extern.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Checking handler of exception occurring in extension typing
+[kernel] Parsing tests/spec/extend_extern.i (no preprocessing)
+[kernel] Failure: Typechecking ACSL extension why3 raised exception Not_found
+[kernel] Extension typing failed as expected