diff --git a/src/logging.ml b/src/logging.ml
index 3a258a2d565aca47df29f0b3d25e2d2d804f852b..2d93d00b3e46394e300e590efe98150f32f1688f 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -23,9 +23,10 @@
 type tag =
   | Autodetect
   | Specification
+  | CallProver
 [@@deriving show { with_path = false }]
 
-let tags_available () = [ Autodetect; Specification ]
+let tags_available () = [ Autodetect; Specification; CallProver ]
 let tag_defs_enabled = ref []
 
 let tag_def_auto =
@@ -34,13 +35,22 @@ let tag_def_auto =
 let tag_def_spec =
   Logs.Tag.def "spec" ~doc:"Prover-tailored specification" Fmt.string
 
+let tag_def_call = Logs.Tag.def "call_prover" ~doc:"Call prover" Fmt.string
+
 let tag_def_of_tag = function
   | Autodetect -> tag_def_auto
   | Specification -> tag_def_spec
+  | CallProver -> tag_def_call
 
 let tag_auto = Logs.Tag.add tag_def_auto "AUTO"
 let tag_spec = Logs.Tag.add tag_def_spec "SPEC"
-let add_tag = function Autodetect -> tag_auto | Specification -> tag_spec
+let tag_call = Logs.Tag.add tag_def_call "CALL_PROVER"
+
+let add_tag = function
+  | Autodetect -> tag_auto
+  | Specification -> tag_spec
+  | CallProver -> tag_call
+
 let tag dt = add_tag dt Logs.Tag.empty
 
 let is_tag_enabled tag =
diff --git a/src/logging.mli b/src/logging.mli
index ab1dbf8512dd77f1f5a58d3b3c4a416fed293bd9..e406e0de1861ea1f7a84d3c11d319ac17d9e167e 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -25,6 +25,7 @@
 type tag =
   | Autodetect
   | Specification
+  | CallProver
 [@@deriving show { with_path = false }]
 
 val tags_available : unit -> tag list
diff --git a/src/verification.ml b/src/verification.ml
index 82019fea63b4f0215d67a4ee5edca2891a3ba8aa..1361fddf88bc748d77d1b1162817c264bc003829 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -304,8 +304,8 @@ let open_file ?format env file =
 
 let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
   file =
-  (if Logging.is_debug_level ()
-   then Debug.(set_flag (lookup_flag "call_prover")));
+  let debug = Logging.(is_debug_level () || is_tag_enabled CallProver) in
+  (if debug then Debug.(set_flag (lookup_flag "call_prover")));
   let env, config = create_env loadpath in
   let main = Whyconf.get_main config in
   let limit =