diff --git a/.ocamlformat b/.ocamlformat
index f4273f4d43843fefc1021bdf3c01fd8d1194fcb8..f99ed8effa525e7a74eb1b093b7144aef6eabe12 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1,4 +1,4 @@
-version=0.23.0
+version=0.25.1
 exp-grouping=parens
 if-then-else=keyword-first
 max-indent=2
diff --git a/caisar.opam b/caisar.opam
index 1057e0bdd91d913ef5003c64fe679403abc8a14a..6747b514293ede9cba4336dce550b64cdf9e4e17 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -29,7 +29,7 @@ depends: [
   "menhirLib" {>= "20210310"}
   "ppx_deriving_yojson" {>= "3.6.1"}
   "csv" {>= "2.4"}
-  "why3" {= "1.5.1"}
+  "why3" {>= "1.6.0"}
   "re" {>= "1.10.4"}
   "caisar-nnet" {= version}
   "caisar-ovo" {= version}
diff --git a/dune-project b/dune-project
index e72f7f96d16594553d0b03e11968a9787098af7a..1776737cede72ebebf565c9a775bd60773e8b0d4 100644
--- a/dune-project
+++ b/dune-project
@@ -82,7 +82,7 @@
    (menhirLib (>= 20210310))
    (ppx_deriving_yojson (>= 3.6.1))
    (csv (>= 2.4))
-   (why3 (= 1.5.1))
+   (why3 (>= 1.6.0))
    (re (>= 1.10.4))
    (caisar-nnet (= :version))
    (caisar-ovo (= :version))
diff --git a/src/AIMOS.ml b/src/AIMOS.ml
index 1588dd387b51c22a05e63516f8cc16bc572c7499..50d2caf59029b9391feea251d066b7d262d07358 100644
--- a/src/AIMOS.ml
+++ b/src/AIMOS.ml
@@ -74,10 +74,8 @@ let call_prover limit config config_prover
         prp_model_parser = Model_parser.lookup_model_parser "no_model";
       }
     in
-    Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
-      ~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
-      ~filename:" " ~get_counterexmp:false ~gen_new_file:false
-      ~printing_info:Printer.default_printing_info (Buffer.create 10)
+    Call_provers.call_on_buffer ~command ~config ~limit ~res_parser
+      ~filename:" " ~get_model:None ~gen_new_file:false (Buffer.create 10)
   in
   let prover_result = Call_provers.wait_on_call prover_call in
   build_answer predicate.property prover_result
diff --git a/src/SAVer.ml b/src/SAVer.ml
index 40511c632e36025ae564c0660be34f2d8ddc012c..c86a8b1e917ef387f009617e3e11115af0089f11 100644
--- a/src/SAVer.ml
+++ b/src/SAVer.ml
@@ -131,10 +131,8 @@ let call_prover limit config config_prover predicate =
         prp_model_parser = Model_parser.lookup_model_parser "no_model";
       }
     in
-    Call_provers.call_on_buffer ~libdir:(Whyconf.libdir config)
-      ~datadir:(Whyconf.datadir config) ~command ~limit ~res_parser
-      ~filename:" " ~get_counterexmp:false ~gen_new_file:false
-      ~printing_info:Printer.default_printing_info (Buffer.create 10)
+    Call_provers.call_on_buffer ~command ~config ~limit ~res_parser
+      ~filename:" " ~get_model:None ~gen_new_file:false (Buffer.create 10)
   in
   let prover_result = Call_provers.wait_on_call prover_call in
   build_answer predicate.property prover_result
diff --git a/src/verification.ml b/src/verification.ml
index 1f9a37d8d12aaf8e996ead146d44554840800b2f..8fe43e4d62d58ce27cf604b9f6ebbe4e0c3eda2e 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -78,7 +78,7 @@ let create_env ?(debug = false) loadpath =
   let config = Autodetect.autodetection ~debug () in
   let config =
     let main = Whyconf.get_main config in
-    let dft_timelimit = 20 (* 20 seconds *) in
+    let dft_timelimit = 20.0 (* 20 seconds *) in
     let dft_memlimit = 4000 (* 4 GB *) in
     let main =
       Whyconf.(
@@ -163,8 +163,7 @@ let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
 
 let call_prover_on_task limit config command driver task =
   let prover_call =
-    Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
-      ~datadir:(Whyconf.datadir config) ~command ~limit driver task
+    Driver.prove_task_prepared ~command ~config ~limit driver task
   in
   let prover_result = Call_provers.wait_on_call prover_call in
   prover_result.pr_answer
@@ -282,7 +281,10 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
   let main = Whyconf.get_main config in
   let limit =
     let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
-    let timelimit = Option.value timelimit ~default:(Whyconf.timelimit main) in
+    let timelimit =
+      Option.value_map timelimit ~f:Float.of_int
+        ~default:(Whyconf.timelimit main)
+    in
     let def = Call_provers.empty_limit in
     {
       Call_provers.limit_time = timelimit;
@@ -318,27 +320,28 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
       invalid_arg
         (Fmt.str "No prover corresponds to %s%a" prover
            (if String.equal altern ""
-           then Fmt.nop
-           else Fmt.(any " " ++ parens string))
+            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))
+            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)
+    | None -> Driver.load_driver_for_prover main 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
+      Driver.load_driver_file_and_extras main env file
+        config_prover.extra_drivers
   in
   Wstdlib.Mstr.map
     (fun theory ->