diff --git a/src/detection.ml b/src/autodetection.ml
similarity index 93%
rename from src/detection.ml
rename to src/autodetection.ml
index c4fa222a5ace8ff5025cb8e9eacd8bb058eb7c40..2cab84d4e912178422fa1ba1fc67246b2ca4178d 100644
--- a/src/detection.ml
+++ b/src/autodetection.ml
@@ -16,9 +16,9 @@ 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 detect () =
+let autodetect ~debug () =
   let open Why3 in
-  Debug.set_flag Why3.Autodetection.debug;
+  if debug then Debug.set_flag Autodetection.debug;
   let caisar_conf = lookup_file Dirs.Sites.config "caisar.conf" in
   let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
   let config = Whyconf.init_config (Some null) in
diff --git a/src/language.ml b/src/language.ml
index d5a0606319a70b39e25b5bb5c1f1c39477362269..12c379e1869d2cd6061deaca563b65bcef6ec05e 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -6,18 +6,20 @@
 
 open Base
 
-(* Register neural network formats. *)
+(* -- Register neural network format. *)
 
 let nnet_parser env _ filename _ =
   let open Why3 in
-  let nnet = Pmodule.read_module env [ "caisar" ] "NNet" in
-  let nnet_input_type =
-    Ty.ty_app Theory.(ns_find_ts nnet.mod_theory.th_export [ "input_type" ]) []
-  in
   let header = Nnet.parse filename in
   match header with
   | Error s -> Loc.errorm "%s" s
   | Ok header ->
+    let nnet = Pmodule.read_module env [ "caisar" ] "NNet" in
+    let nnet_input_type =
+      Ty.ty_app
+        Theory.(ns_find_ts nnet.mod_theory.th_export [ "input_type" ])
+        []
+    in
     let id_as_tuple = Ident.id_fresh "AsTuple" in
     let th_uc = Pmodule.create_module env id_as_tuple in
     let th_uc = Pmodule.use_export th_uc nnet in
diff --git a/src/main.ml b/src/main.ml
index 81d0a2b30f598b485333d04a8f127d8a97577ec8..fbcfe6075aed69dbeb549b6ae6200862110bf4cc 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -10,7 +10,7 @@ module Format = Caml.Format
 
 let caisar = "caisar"
 
-(* Logs. *)
+(* -- Logs. *)
 
 let pp_header =
   let x =
@@ -40,13 +40,30 @@ let setup_logs =
   in
   Term.(const setup_log $ Logs_cli.level ())
 
-(* Commands. *)
+(* -- Commands. *)
 
-let config cmd detect () =
-  Logs.debug (fun m -> m "Command `%s'." cmd);
-  if detect then Logs.app (fun m -> m "Automatic detection.")
+let config detect () =
+  if detect
+  then begin
+    Logs.debug (fun m -> m "Automatic detection.");
+    let config = Autodetection.autodetect ~debug:false () in
+    let open Why3 in
+    let provers = Whyconf.get_provers config in
+    Logs.app (fun m ->
+      m "@[<v>%a@]"
+        (Pp.print_iter2 Whyconf.Mprover.iter Pp.newline Pp.nothing
+           Whyconf.print_prover Pp.nothing)
+        provers)
+  end
 
-(* Command line. *)
+let verify format loadpath files =
+  List.iter ~f:(Verification.verify format loadpath) files
+
+let exec_cmd cmdname cmd =
+  Logs.debug (fun m -> m "Command `%s'." cmdname);
+  cmd ()
+
+(* -- Command line. *)
 
 let config_cmd =
   let cmdname = "config" in
@@ -83,7 +100,7 @@ let config_cmd =
            else
              (* TODO: Do not only check for [detect], and enable it by
                 default, as soon as other options are available. *)
-             `Ok (config cmdname true ()))
+             `Ok (exec_cmd cmdname (fun () -> config true ())))
         $ const cmdname $ detect $ setup_logs)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man )
 
@@ -111,7 +128,7 @@ let verify_cmd =
   ( Term.(
       ret
         (const (fun format loadpath files ->
-           `Ok (List.iter ~f:(Verify.do_verify format loadpath) files))
+           `Ok (exec_cmd cmdname (fun () -> verify format loadpath files)))
         $ format $ loadpath $ files)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 
diff --git a/src/verify.ml b/src/verification.ml
similarity index 93%
rename from src/verify.ml
rename to src/verification.ml
index 3aa60d7bb21fb797dcdb59d50db05836bd747db1..f4ba6da943c70b5317ba43aa0caf6d48030383e7 100644
--- a/src/verify.ml
+++ b/src/verification.ml
@@ -10,7 +10,7 @@ module Format = Caml.Format
 let () = Language.register ()
 
 let create_env loadpath =
-  let config = Detection.detect () in
+  let config = Autodetection.autodetect ~debug:true () in
   let stdlib = Dirs.Sites.stdlib in
 
   let open Why3 in
@@ -20,7 +20,7 @@ let create_env loadpath =
 
 let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
 
-let do_verify format loadpath file =
+let verify format loadpath file =
   let open Why3 in
   let env, config = create_env loadpath in
   let _, mstr_theory =
diff --git a/tests/autodetect.t b/tests/autodetect.t
new file mode 100644
index 0000000000000000000000000000000000000000..c391f46ed4bf37a864f1dacfed2017ebeaa596b3
--- /dev/null
+++ b/tests/autodetect.t
@@ -0,0 +1,3 @@
+Test verify
+  $ caisar config -d
+  [caisar] Alt-Ergo 2.4.0
diff --git a/tests/simple.t b/tests/simple.t
index 2fd8bba5e21304a722ac04c66183b78c91de96bf..567c187e1bbbcc95c2dc2908bed4b6c74959e25a 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -1,4 +1,4 @@
-Test help
+Test verify
   $ caisar verify -L . --format whyml - <<EOF
   > theory T
   >   use TestNetwork.AsTuple