diff --git a/caisar.opam b/caisar.opam
index 81d04b88409f50a816f290213834ab98b6e36209..60de520366980053823117a77e434790f58254e7 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.4.0"}
+  "why3" {>= "1.5.0"}
   "re"
   "caisar-nnet" {= version}
   "caisar-ovo" {= version}
@@ -53,6 +53,3 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://git.frama-c.com/pub/caisar.git"
-pin-depends: [
-  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
-]
diff --git a/caisar.opam.template b/caisar.opam.template
index 562220ac323378469f979b37cfd8dbb936f32478..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644
--- a/caisar.opam.template
+++ b/caisar.opam.template
@@ -1,3 +0,0 @@
-pin-depends: [
-  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
-]
diff --git a/dune-project b/dune-project
index 585375a402054336a7d746e0a0f51b5c22e626a7..241ea49b7d16c8e4ebc1fcd5d4e828f79a02d6d6 100644
--- a/dune-project
+++ b/dune-project
@@ -72,7 +72,7 @@
    (menhirLib (>= 20210310))
    (ppx_deriving_yojson (>= 3.6.1))
    (csv (>= 2.4))
-   (why3 (= 1.4.0))
+   (why3 (>= 1.5.0))
    re
    (caisar-nnet (= :version))
    (caisar-ovo (= :version))
diff --git a/src/autodetect.ml b/src/autodetect.ml
index 3f98d68497deef4c250c8f3c9bb0cd0ebe077d0c..a7f5c262e029882bcaa7a9c30240bb6900ddbe0e 100644
--- a/src/autodetect.ml
+++ b/src/autodetect.ml
@@ -38,7 +38,18 @@ let autodetection ?(debug = false) () =
     lookup_file Dirs.Sites.config "caisar-detection-data.conf"
   in
   let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
+  let provers = Autodetection.find_provers data in
+  let provers =
+    List.fold_left ~init:[] provers ~f:(fun acc (path, name, version) ->
+      {
+        Autodetection.Partial.name;
+        path;
+        version;
+        shortcut = None;
+        manual = false;
+      }
+      :: acc)
+  in
   let config = Whyconf.init_config (Some null) in
-  let binaries = Autodetection.request_binaries_version config data in
-  let provers = Autodetection.compute_builtin_prover binaries config data in
+  let provers = Autodetection.compute_builtin_prover provers config data in
   Whyconf.set_provers config provers
diff --git a/tests/marabou.t b/tests/marabou.t
index dc2070d647ca980444b42652fcf0da55f5b65c60..263f8682885a54e264cc1cf22201cd70770af05b 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -34,12 +34,12 @@ Test verify
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
+  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>0 prover(s) added
   <autodetect>Generating strategies:
-  <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
-  <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
-  <autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
-  <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.
diff --git a/tests/simple.t b/tests/simple.t
index 55a2088c7f822fc222ec51c9a32d2767148efcad..0b8269928329fcf4ebbe7d10260a573a9ed88676 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -37,12 +37,12 @@ Test verify
   >      ((0.0:t) .< y1 \/ (0.5:t) .< y1) /\ (0.0:t) .< y2 .< (0.5:t)
   > end
   > EOF
+  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>0 prover(s) added
   <autodetect>Generating strategies:
-  <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
-  <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
-  <autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
-  <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.
diff --git a/tests/simple_onnx.t b/tests/simple_onnx.t
index b947d7d2469268a5b9660b4206a8c55956497897..600f9c82512f58a76b73fa4af4dd5e299135ece9 100644
--- a/tests/simple_onnx.t
+++ b/tests/simple_onnx.t
@@ -29,12 +29,12 @@ Test verify
   >      (0.0:t) .< y1 .< (0.5:t)
   > end
   > EOF
+  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>0 prover(s) added
   <autodetect>Generating strategies:
-  <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
-  <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
-  <autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
-  <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index 42e51aea9366bdc438e34d62c89fd4e7903e3e46..9225ad73ff5a76e6f2517fa2fff3c7cd7051abae 100644
--- a/tests/simple_ovo.t
+++ b/tests/simple_ovo.t
@@ -35,12 +35,12 @@ Test verify
   >      robust_to svm_apply a (8.0:t)
   > end
   > EOF
+  <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: ($TESTCASE_ROOT/bin/Marabou --version) > $TMPFILE 2>&1
   <autodetect>0 prover(s) added
   <autodetect>Generating strategies:
-  <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
-  <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
-  <autodetect>Run: (saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
-  <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.1, OK.