diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 94f5b8131ffe76c1ea358b39e5130bc4b1088a3f..9335161d010553d664de54516270ead945483112 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1239,3 +1239,13 @@ let print_generated ?header file =
     end
 
 (* -------------------------------------------------------------------------- *)
+(* --- Debugging                                                          --- *)
+(* -------------------------------------------------------------------------- *)
+
+let protect e =
+  if debug_atleast 1 then false else
+    match e with
+    | Db.Cancel | Log.AbortError _ | Log.AbortFatal _ -> false
+    | _ -> true
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index a37b5e895a7470f21a738e3c69a5c15dc9566796..97392faa580e3f4b36d686429ba3eb7b53c90c1d 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -175,3 +175,5 @@ val print_generated: ?header:string -> string -> unit
 (** print the given file if the debugging category
     "print-generated" is set *)
 val cat_print_generated: category
+
+val protect : exn -> bool