Several updates following the new Why3 (version 1.6.0) API changes.

Fix issue #26.

.ocamlformat

-version=0.23.0
+version=0.25.1
 exp-grouping=parens
 if-then-else=keyword-first
 max-indent=2

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}

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))

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

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

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 ->