diff --git a/caisar.opam b/caisar.opam
index b2a9fd775a6f73d2d6edca3561298f9f1f4f7236..3a0158d6f7109399c6c998e0316f63fd07c46533 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -42,5 +42,5 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 pin-depends: [
-  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#4e3d0bc71f153fe5625a4a7c92d4dd6cd5e8cf75" ]
+  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
 ]
diff --git a/caisar.opam.template b/caisar.opam.template
index fd083c6da94672bdd5fee1e7e621505c51b22215..562220ac323378469f979b37cfd8dbb936f32478 100644
--- a/caisar.opam.template
+++ b/caisar.opam.template
@@ -1,3 +1,3 @@
 pin-depends: [
-  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#4e3d0bc71f153fe5625a4a7c92d4dd6cd5e8cf75" ]
+  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#047c34a8" ]
 ]
diff --git a/src/autodetection.ml b/src/autodetection.ml
index d23bd40302bfda76d3ab144176a33529151fc7b4..329c50f742d47dacfec18c64f7ed83d10cce36fb 100644
--- a/src/autodetection.ml
+++ b/src/autodetection.ml
@@ -25,5 +25,5 @@ let autodetect ?(debug = false) () =
   let data = Autodetection.Prover_autodetection_data.from_file caisar_conf 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 data in
+  let provers = Autodetection.compute_builtin_prover binaries config data in
   Whyconf.set_provers config provers
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 15e77170ec6e9c4b6ba86803076840f2c217bab4..7844e8d9287a1db73ee7deb538bee064ab6d80d8 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -95,6 +95,7 @@ let simplify_goal env input_variables =
                       compute_defs = false;
                       compute_builtin = true;
                       compute_def_set = Term.Sls.empty;
+                      compute_max_quantifier_domain = 0;
                     }
                     env known
                 in
diff --git a/src/verification.ml b/src/verification.ml
index f2fcf8ac25ba7fe6052f715e9478310a42891bff..87131c109adfd59d973958a28b1afcf71d6bdb7f 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -37,7 +37,8 @@ let combine_prover_answers answers =
     | Call_provers.Valid, r | r, Call_provers.Valid -> r
     | _ -> acc)
 
-let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
+let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver task
+    =
   let open Why3 in
   let task_prepared = Driver.prepare_task driver task in
   let tasks =
@@ -53,10 +54,12 @@ let call_prover ~limit (prover : Why3.Whyconf.config_prover) driver task =
     | Some _ -> assert false (* By construction of the meta. *)
     | None -> invalid_arg (Fmt.str "No neural network model found in task")
   in
+  let nn_file = Filename.concat (Caml.Sys.getcwd ()) nn_file in
   let command = Re.replace_string nnet_or_onnx ~by:nn_file command in
   let call_prover_on_task task_prepared =
     let prover_call =
-      Driver.prove_task_prepared ~command ~limit driver task_prepared
+      Driver.prove_task_prepared ~libdir:(Whyconf.libdir config)
+        ~datadir:(Whyconf.datadir config) ~command ~limit driver task_prepared
     in
     let prover_result = Call_provers.wait_on_call prover_call in
     prover_result.pr_answer
@@ -109,5 +112,7 @@ let verify ?(debug = false) format loadpath ?memlimit ~prover file =
           in
           Driver.load_driver_absolute env file prover.extra_drivers
       in
-      List.iter ~f:(call_prover ~limit prover driver) tasks)
+      List.iter
+        ~f:(call_prover ~limit (Whyconf.get_main config) prover driver)
+        tasks)
     mstr_theory
diff --git a/tests/bin/pyrat.py b/tests/bin/pyrat.py
index e2c01b3822a1f3c39400f3df74fbe7eee2b29951..a6e81e991a96a4856284cf92d4e730568aeb05bb 100755
--- a/tests/bin/pyrat.py
+++ b/tests/bin/pyrat.py
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/sh -e
 
 
 case $1 in
@@ -6,7 +6,9 @@ case $1 in
         echo "PyRAT 1.1"
         ;;
     *)
+        echo "PWD: $(pwd)"
         echo "NN: $2"
+        test -e $2 || (echo "Can't find the file" && exit 1)
         echo "Goal:"
         cat $4
         echo "Result = Unknown"