diff --git a/src/main.ml b/src/main.ml
index 60b7c26f720feb3ac1a8e3fb994dd0e4bfba3e17..214f8df480638ff6f31b60657942dfc37e06e355 100644
--- a/src/main.ml
+++ b/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 =
diff --git a/src/verification.ml b/src/verification.ml
index 3a7bacdb55f8da024dd714031e792a7b429e3257..ee54efabc9acbe2dd4a9edd793e065feccbac9f9 100644
--- a/src/verification.ml
+++ b/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))
diff --git a/src/verification.mli b/src/verification.mli
index 5f8f7ae2bfdc102c1c265888fe48f1143b750b7a..270048cdc2b03a1c2bfc3ad977da5ea2a3cacf39 100644
--- a/src/verification.mli
+++ b/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