diff --git a/tests/spec/extend_extern.i b/tests/spec/extend_extern.i
index 8dffe2261770f824cb6dd7c1ffbf81597c9f15a1..c3c61836044e2aa33369d00e439c5806eff9e106 100644
--- a/tests/spec/extend_extern.i
+++ b/tests/spec/extend_extern.i
@@ -1,5 +1,4 @@
 /* run.config
-   MACRO: PTEST_MAKE_MODULE make FRAMAC_USER_OFLAGS="-package why3" FRAMAC_USER_BFLAGS="-package why3"
    MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
    OPT:
  */
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
index 70f1ad660c25adcf657ff3b007b5cd5ec6ecf8fb..6662949743276cd8e2fdd61b04cd9c0f32660382 100644
--- a/tests/spec/extend_extern.ml
+++ b/tests/spec/extend_extern.ml
@@ -3,9 +3,7 @@ open Cil_types
 
 let load_theory = function
   | { pred_content = Papp (_, [], [ { term_node = TConst(LStr _name) } ] ) } ->
-    let open Why3 in ignore (
-      Theory.import_namespace Theory.empty_ns [_name]
-    )
+    raise Not_found
   | _ -> assert false
 
 let typing ~typing_context ~loc lexprs =
@@ -20,3 +18,14 @@ let typing ~typing_context ~loc lexprs =
 
 let () =
   Logic_typing.register_global_extension "why3" false typing
+
+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"
+
+let () = Kernel.TypeCheck.set false
+
+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..a5e2e92faf274485511f88e89c2366da1a3cea5e
--- /dev/null
+++ b/tests/spec/oracle/extend_extern.res.oracle
@@ -0,0 +1,3 @@
+[kernel] Checking handler of exception occurring in extension typing
+[kernel] Parsing tests/spec/extend_extern.i (no preprocessing)
+[kernel] Extension typing failed as expected