diff --git a/src/autodetection.ml b/src/autodetection.ml
index ff79daa92780c633774adde95eea5f6a3a32e775..d23bd40302bfda76d3ab144176a33529151fc7b4 100644
--- a/src/autodetection.ml
+++ b/src/autodetection.ml
@@ -16,7 +16,7 @@ let rec lookup_file dirs filename =
     let file = Caml.Filename.concat dir filename in
     if Sys.file_exists file then file else lookup_file dirs filename
 
-let autodetect ~debug () =
+let autodetect ?(debug = false) () =
   let open Why3 in
   if debug then Debug.set_flag Autodetection.debug;
   let caisar_conf =
diff --git a/src/autodetection.mli b/src/autodetection.mli
index 42842afef2bfe1c9d74610dbf3e45bd2dc0ab3e2..65e97b263dd572afde902ce6a4155c8a877c50a2 100644
--- a/src/autodetection.mli
+++ b/src/autodetection.mli
@@ -4,7 +4,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val autodetect : debug:bool -> unit -> Why3.Whyconf.config
+val autodetect : ?debug:bool -> unit -> Why3.Whyconf.config
 (** Perform the autodetection of provers.
 
     @param debug activates debug information. *)
diff --git a/src/main.ml b/src/main.ml
index a86c5a947a69d9f9ea8ab38fee4bb6dd719b529c..34ec82cd5f71de303dab204ef17f7216788ef9e6 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -66,7 +66,10 @@ let config detect () =
         provers))
 
 let verify format loadpath memlimit prover files =
-  List.iter ~f:(Verification.verify format loadpath ?memlimit ~prover) files
+  let debug = match Logs.level () with Some Debug -> true | _ -> false in
+  List.iter
+    ~f:(Verification.verify ~debug format loadpath ?memlimit ~prover)
+    files
 
 let exec_cmd cmdname cmd =
   Logs.debug (fun m -> m "Command `%s'." cmdname);
@@ -141,11 +144,11 @@ let verify_cmd =
   let man = [ `S Manpage.s_description; `P doc ] in
   ( Term.(
       ret
-        (const (fun format loadpath memlimit prover files ->
+        (const (fun format loadpath memlimit prover files _ ->
            `Ok
              (exec_cmd cmdname (fun () ->
                 verify format loadpath memlimit prover files)))
-        $ format $ loadpath $ memlimit $ prover $ files)),
+        $ format $ loadpath $ memlimit $ prover $ files $ setup_logs)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 
 let default_cmd =
diff --git a/src/verification.ml b/src/verification.ml
index c7507c5b4c4efd4826374fba608991e55ab5e658..5bfa184cb9d5a03e28acc0c2a6c5561803a07750 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -7,9 +7,9 @@
 open Base
 module Filename = Caml.Filename
 
-let () = Language.register_nnet_support ()
-
-let () = Language.register_onnx_support ()
+let () =
+  Language.register_nnet_support ();
+  Language.register_onnx_support ()
 
 let create_env loadpath =
   let config = Autodetection.autodetect ~debug:true () in
@@ -73,9 +73,9 @@ let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
   Fmt.pr "Goal %a: %a@." Pretty.print_pr (Task.task_goal task)
     Call_provers.print_prover_answer answer
 
-let verify format loadpath ?memlimit ~prover file =
+let verify ?(debug = false) format loadpath ?memlimit ~prover file =
   let open Why3 in
-  (* Debug.(set_flag (lookup_flag "call_prover")); *)
+  if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env loadpath in
   let steplimit = None in
   let timeout = None in
diff --git a/src/verification.mli b/src/verification.mli
index 95432d0952df6c2e820e53e62ddc68acc87f9310..fd4c7635bf29a1abae1ad0e7ee74c36fe74663f2 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -5,15 +5,17 @@
 (**************************************************************************)
 
 val verify :
+  ?debug:bool ->
   string option ->
   string list ->
   ?memlimit:int ->
   prover:string ->
   string ->
   unit
-(** [verify format loadpath memlimit prover file] launches a verification of the
-    given [file] with the provided [prover].
+(** [verify debug format loadpath memlimit prover file] launches a verification
+    of the given [file] with the provided [prover].
 
+    @param debug when set, enables debug information.
     @param format is the [file] format.
     @param loadpath is the additional loadpath.
     @param memlimit