[verification] Pull out non-task specific code.

src/verification.ml

@@ -318,50 +318,48 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
       let th = JSON.theory_of_input env jin in
       Wstdlib.Mstr.singleton th.th_name.id_string th
   in
+  let config_prover =
+    let altern =
+      let default =
+        if Prover.has_vnnlib_support prover && Option.is_some dataset
+        then "VNNLIB"
+        else "" (* Select the default one, w/o an alternative. *)
+      in
+      Option.value prover_altern ~default
+    in
+    let prover = Prover.to_string prover in
+    try
+      Whyconf.(filter_one_prover config (mk_filter_prover ~altern prover))
+    with
+    | Whyconf.ProverNotFound _ ->
+      invalid_arg
+        (Fmt.str "No prover corresponds to %s%a" prover
+           (if String.equal altern ""
+           then Fmt.nop
+           else Fmt.(any " " ++ parens string))
+           altern)
+    | Whyconf.ProverAmbiguity _ ->
+      invalid_arg
+        (Fmt.str "More than one prover correspond to %s%a" prover
+           (if String.equal altern ""
+           then Fmt.nop
+           else Fmt.(any " " ++ parens string))
+           altern)
+  in
+  let driver =
+    match String.chop_prefix ~prefix:"caisar_drivers/" config_prover.driver with
+    | None -> Whyconf.(load_driver (get_main config) env config_prover)
+    | Some file ->
+      let file =
+        Filename.concat
+          (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
+          file
+      in
+      Driver.load_driver_absolute env file config_prover.extra_drivers
+  in
   Wstdlib.Mstr.map
     (fun theory ->
       let tasks = Task.split_theory theory None None in
-      let config_prover =
-        let altern =
-          let default =
-            if Prover.has_vnnlib_support prover && Option.is_some dataset
-            then "VNNLIB"
-            else "" (* Select the default one, w/o an alternative. *)
-          in
-          Option.value prover_altern ~default
-        in
-        let prover = Prover.to_string prover in
-        try
-          Whyconf.(filter_one_prover config (mk_filter_prover ~altern prover))
-        with
-        | Whyconf.ProverNotFound _ ->
-          invalid_arg
-            (Fmt.str "No prover corresponds to %s%a" prover
-               (if String.equal altern ""
-               then Fmt.nop
-               else Fmt.(any " " ++ parens string))
-               altern)
-        | Whyconf.ProverAmbiguity _ ->
-          invalid_arg
-            (Fmt.str "More than one prover correspond to %s%a" prover
-               (if String.equal altern ""
-               then Fmt.nop
-               else Fmt.(any " " ++ parens string))
-               altern)
-      in
-      let driver =
-        match
-          String.chop_prefix ~prefix:"caisar_drivers/" config_prover.driver
-        with
-        | None -> Whyconf.(load_driver (get_main config) env config_prover)
-        | Some file ->
-          let file =
-            Filename.concat
-              (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
-              file
-          in
-          Driver.load_driver_absolute env file config_prover.extra_drivers
-      in
       List.map
         ~f:(call_prover ?dataset ~limit main env prover config_prover driver)
         tasks)