diff --git a/src/main.ml b/src/main.ml
index 42ae008f8d195cb3dca6c7ca264a7c207226c0a3..843aa75f26431712ca38f15959f56e0fd1e6cee8 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -120,7 +120,7 @@ let timelimit_of_string s =
   | [ v ], [ "h" ] -> Int.of_string v * 3600
   | _ -> invalid_arg "Unrecognized time limit"
 
-let verify format loadpath memlimit timelimit prover dataset_csv files =
+let verify ?format loadpath ?memlimit ?timelimit prover dataset_csv files =
   let debug = log_level_is_debug () in
   let memlimit = Option.map memlimit ~f:memlimit_of_string in
   let timelimit = Option.map timelimit ~f:timelimit_of_string in
@@ -130,7 +130,7 @@ let verify format loadpath memlimit timelimit prover dataset_csv files =
          ?dataset_csv)
     files
 
-let verify_json format loadpath memlimit timelimit file =
+let verify_json loadpath ?memlimit ?timelimit file =
   let json_config =
     match
       Verification.File.json_config_of_yojson (Yojson.Safe.from_file file)
@@ -154,7 +154,7 @@ let verify_json format loadpath memlimit timelimit file =
       failwith
         (Fmt.str "No '%s' file or directory" json_config.property.dataset)
   in
-  verify format loadpath memlimit timelimit json_config.prover dataset_csv
+  verify loadpath ?memlimit ?timelimit json_config.prover dataset_csv
     [ Verification.File.of_json_config json_config ]
 
 let exec_cmd cmdname cmd =
@@ -210,10 +210,6 @@ let timelimit =
   Arg.(
     value & opt (some string) None & info [ "t"; "timelimit" ] ~doc ~docv:"TIME")
 
-let format =
-  let doc = "File format." in
-  Arg.(value & opt (some string) None & info [ "format" ] ~doc)
-
 let loadpath =
   let doc = "Additional loadpath." in
   Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
@@ -226,6 +222,10 @@ let verify_cmd =
       ~doc
       ~man:[ `S Manpage.s_description; `P doc ]
   in
+  let format =
+    let doc = "File format." in
+    Arg.(value & opt (some string) None & info [ "format" ] ~doc)
+  in
   let term =
     let files =
       let doc = "File to verify." in
@@ -253,7 +253,7 @@ let verify_cmd =
       const
         (fun format loadpath memlimit timelimit prover dataset_csv files _ ->
         exec_cmd cmdname (fun () ->
-          verify format loadpath memlimit timelimit prover dataset_csv files))
+          verify ?format loadpath ?memlimit ?timelimit prover dataset_csv files))
       $ format $ loadpath $ memlimit $ timelimit $ prover $ dataset_csv $ files
       $ setup_logs)
   in
@@ -277,10 +277,10 @@ let verify_json_cmd =
         required & pos ~rev:true 0 (some file) None & info [] ~doc ~docv:"FILE")
     in
     Term.(
-      const (fun format loadpath memlimit timelimit json _ ->
+      const (fun loadpath memlimit timelimit json _ ->
         exec_cmd cmdname (fun () ->
-          verify_json format loadpath memlimit timelimit json))
-      $ format $ loadpath $ memlimit $ timelimit $ json $ setup_logs)
+          verify_json loadpath ?memlimit ?timelimit json))
+      $ loadpath $ memlimit $ timelimit $ json $ setup_logs)
   in
   Cmd.v info term