diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f855e46565028d2688eaf214588451e066668753..5920671ad02db63028dc97ad00e383adfbe3ff12 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -544,7 +544,13 @@ module Extensions = struct
       with Not_found ->
         Kernel.fatal ~source:(fst loc) "unsupported clause of name '%s'" name
     in
-    status, typer ~typing_context ~loc p
+    try
+      status, typer ~typing_context ~loc p
+    with
+    | (Log.AbortError _ | Log.AbortFatal _) as exn -> raise exn
+    | exn ->
+      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.ml b/tests/spec/extend_extern.ml
index 6662949743276cd8e2fdd61b04cd9c0f32660382..c60a714b9bf921abd03047c7e87337548365b108 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -23,9 +23,14 @@ let main () =
   try
     Kernel.feedback
       "Checking handler of exception occurring in extension typing";
-    Ast.compute (); Kernel.fatal "Extension typing should have failed"
-  with Not_found -> Kernel.feedback "Extension typing failed as expected"
+    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
index a5e2e92faf274485511f88e89c2366da1a3cea5e..3b7533295bbd2465e6b234f1ed957310f2e3e77e 100644
--- a/tests/spec/oracle/extend_extern.res.oracle
+++ b/tests/spec/oracle/extend_extern.res.oracle
@@ -1,3 +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