[SAVer] Optional argument for dataset-csv.

src/main.ml

@@ -73,7 +73,7 @@ let verify format loadpath memlimit timeout prover dataset_csv files =
   List.iter
     ~f:
       (Verification.verify ~debug format loadpath ?memlimit ?timeout prover
-         ~dataset_csv)
+         ?dataset_csv)
     files
 
 let exec_cmd cmdname cmd =

src/verification.ml

@@ -60,8 +60,8 @@ let answer_saver limit config task env prover dataset_csv =
   let handle_task_saver task env dataset_csv command =
     let dataset_filename =
       match dataset_csv with
-      | Some s -> s
-      | None -> failwith "Error, no dataset provided for SAVer."
+      | "" -> failwith "Error, no dataset provided for SAVer."
+      | s -> s
     in
     let goal = Task.task_goal_fmla task in
     let eps, svm_filename =
@@ -186,11 +186,13 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
     Call_provers.print_prover_answer prover_answer
 
 let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
-  ~dataset_csv file =
+  ?dataset_csv file =
+  let open Why3 in
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
   let env, config = create_env loadpath in
   let steplimit = None in
   let steps = match steplimit with Some 0 -> None | _ -> steplimit in
+  let dataset_csv = Option.value dataset_csv ~default:"" in
   let limit =
     let memlimit =
       Option.value memlimit ~default:Whyconf.(memlimit (get_main config))

src/verification.mli

@@ -18,7 +18,7 @@ val verify :
   ?memlimit:int ->
   ?timeout:int ->
   Prover.t ->
-  dataset_csv:string option ->
+  ?dataset_csv:string ->
   File.t ->
   unit
 (** [verify debug format loadpath memlimit timeout prover file] launches a