diff --git a/src/autodetect.ml b/src/autodetect.ml
index 3ab29fcb3875ca3c17bd391190a6afedf5b28b2c..3c3f38e2927e6dda623156dcdf43477b4b6fc346 100644
--- a/src/autodetect.ml
+++ b/src/autodetect.ml
@@ -30,6 +30,13 @@ let rec lookup_file dirs filename =
     let file = Stdlib.Filename.concat dir filename in
     if Stdlib.Sys.file_exists file then file else lookup_file dirs filename
 
+let filter_binaries =
+  let d = lazy (Sys.getenv "CAISAR_AUTODETECT_BIN") in
+  fun path ->
+    match Lazy.force d with
+    | Some d -> String.equal (Stdlib.Filename.dirname path) d
+    | None -> true
+
 let autodetection () =
   let debug = Logging.(is_debug_level src_autodetect) in
   if debug then Debug.set_flag Autodetection.debug;
@@ -39,15 +46,15 @@ let autodetection () =
   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)
+    List.filter_map provers ~f:(fun (path, name, version) ->
+      Option.some_if (filter_binaries path)
+        {
+          Autodetection.Partial.name;
+          path;
+          version;
+          shortcut = None;
+          manual = false;
+        })
   in
   let config = Whyconf.init_config (Some Stdlib.Filename.null) in
   let provers = Autodetection.compute_builtin_prover provers config data in
diff --git a/tests/aimos.t b/tests/aimos.t
index 0ac820383c49c20deff4bb1dbcc441a94ab251a2..0e37f12305d03d86d5afdcfd17c0101e28d95dfd 100644
--- a/tests/aimos.t
+++ b/tests/aimos.t
@@ -5,13 +5,11 @@ Test verify
   > 2.500000000000000000e+02,2.222222222222222376e-01,-3.138814875812015348e+00,2.333333333333333428e+02,0.000000000000000000e+00
   > EOF
 
-  $ chmod u+x bin/aimos
+  $ . ./setup_env.sh
 
   $ bin/aimos --version
   AIMOS 1.0
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv - 2>&1 <<EOF
   > theory ACASXU_P5
   >   use TestNetwork.AsArray
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 5fee7ec434876b149122756fbe86229d36456e81..ef82fd184ceda081f495d7f97ddd6e11240a7cd0 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -4,7 +4,7 @@ Test autodetect
   > echo "2.4.0"
   > EOF
 
-  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver bin/aimos bin/cvc5 bin/nnenum.sh bin/abcrown.sh
+  $ . ./setup_env.sh
 
   $ bin/alt-ergo
   2.4.0
@@ -30,8 +30,6 @@ Test autodetect
   $ bin/abcrown.sh --version
   dummy-version
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar config -d --ltag=Autodetect -v 2>&1 | ./filter_tmpdir.sh
   <autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
diff --git a/tests/cvc5.t b/tests/cvc5.t
index e55696f37171cd8dc25fa4c1a6da7d5c7d17c4d1..cc1a1cd351c6667d683d147a6f156ca09a870af8 100644
--- a/tests/cvc5.t
+++ b/tests/cvc5.t
@@ -1,11 +1,9 @@
 Test verify
-  $ chmod u+x bin/cvc5
+  $ . ./setup_env.sh
 
   $ bin/cvc5 --version
   This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify -L . --format whyml --prover=CVC5 --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory CVC5
   >   use TestNetworkONNX.AsTuple as TN
diff --git a/tests/dataset.t b/tests/dataset.t
index 0e965840cde1604939d858d4ed9e0c710be4bd89..3476ac347cb8be7906ce2fa4b828d711cbb16287 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -4,7 +4,7 @@ Test verify on dataset
   > 0,0.941176471,0,0,0.011764706,0.039215686
   > EOF
 
-  $ chmod u+x bin/pyrat.py bin/Marabou
+  $ . ./setup_env.sh
 
   $ bin/pyrat.py --version
   PyRAT 1.1
@@ -12,8 +12,6 @@ Test verify on dataset
   $ bin/Marabou --version
   1.0.+
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use TestNetwork.AsArray as TN
diff --git a/tests/define.t b/tests/define.t
index b698beb81e1d88d7926f59610d0a8cd501fdbe54..058ca5b9cec6088769057c1b101780453f2f0ffb 100644
--- a/tests/define.t
+++ b/tests/define.t
@@ -1,12 +1,9 @@
 Test interpretation of on-the-fly definition of toplevel constants
-
-  $ chmod u+x bin/pyrat.py
+  $ . ./setup_env.sh
 
   $ bin/pyrat.py --version
   PyRAT 1.1
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ cat > file.mlw <<EOF
   > theory T
   >   use int.Int
diff --git a/tests/dune b/tests/dune
index 09ce2af3f16be707a650459cb34e4a57dc6ccf71..e2e87361de2336686b9ef256fd6ba7eb2269f404 100644
--- a/tests/dune
+++ b/tests/dune
@@ -1,16 +1,11 @@
 (cram
  (deps
   (package caisar)
+  setup_env.sh
   TestNetwork.nnet
   TestNetworkONNX.onnx
   TestSVM.ovo
-  bin/pyrat.py
-  bin/Marabou
-  bin/saver
-  bin/aimos
-  bin/cvc5
-  bin/nnenum.sh
-  bin/abcrown.sh
+  (glob_files bin/*)
   filter_tmpdir.sh
   ../lib/xgboost/example/california.csv
   ../lib/xgboost/example/california.json)
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 28695a744ada60305f2c3a18842df557ff5e74ce..2e04d6c537bfac608531692739c0e51de3a9a1e3 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -1,12 +1,9 @@
 Test interpret on acasxu
-
-  $ chmod u+x bin/pyrat.py
+  $ . ./setup_env.sh
 
   $ bin/pyrat.py --version
   PyRAT 1.1
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 8ce1d6076853bf3f506625105d98ae35f5600ea9..2c140adb850d7cf9dc60bb0b23ea329738084871 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -4,13 +4,11 @@ Test interpret on dataset
   > 0,1.0,0.0,0.019607843,0.776470588,0.784313725
   > EOF
 
-  $ chmod u+x bin/Marabou
+  $ . ./setup_env.sh
 
   $ bin/Marabou --version
   1.0.+
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
diff --git a/tests/marabou.t b/tests/marabou.t
index 8ded847e994ab771f5e3bf150ec3b166eaba270d..e79433ad986881f07570b2d174fe5bca522a49f9 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -1,11 +1,9 @@
 Test verify
-  $ chmod u+x bin/Marabou
+  $ . ./setup_env.sh
 
   $ bin/Marabou --version
   1.0.+
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use ieee_float.Float64
diff --git a/tests/pyrat.t b/tests/pyrat.t
index 4c36cd0903f0aedcd140eea9e243a4611c96f20e..85acd3882f06b2b8fa4ca953a9966bb7097e5788 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -1,11 +1,9 @@
 Test verify
-  $ chmod u+x bin/pyrat.py
+  $ . ./setup_env.sh
 
   $ bin/pyrat.py --version
   PyRAT 1.1
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory PyRAT
   >   use TestNetwork.AsTuple
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index f6512e2bc0419ff272fc531ef9f4d5caa1f52898..5d2be1db6d59913d4c88db07b36dfaeabb95d0d7 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -1,11 +1,9 @@
 Test verify
-  $ chmod u+x bin/pyrat.py
+  $ . ./setup_env.sh
 
   $ bin/pyrat.py --version
   PyRAT 1.1
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory PyRAT_ONNX
   >   use ieee_float.Float64
diff --git a/tests/saver.t b/tests/saver.t
index a05fc8d70b7392ac79a4251c7a461197041700d3..4fccd5306a5b04301c86ce570fb11ecf668dc31c 100644
--- a/tests/saver.t
+++ b/tests/saver.t
@@ -4,13 +4,11 @@ Test verify
   > 1,0.5,0.5,0.0,
   > EOF
 
-  $ chmod u+x bin/saver
+  $ . ./setup_env.sh
 
   $ bin/saver --version
   v1.0
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify -L . --format whyml --prover=SAVer --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >   use TestSVM.AsArray
diff --git a/tests/setup_env.sh b/tests/setup_env.sh
new file mode 100644
index 0000000000000000000000000000000000000000..96726fec52b832361f954fee1506dd675ed9fb30
--- /dev/null
+++ b/tests/setup_env.sh
@@ -0,0 +1,3 @@
+chmod u+x bin/*
+PATH=$(pwd)/bin:$PATH
+export CAISAR_AUTODETECT_BIN=$(pwd)/bin
diff --git a/tests/verify_json.t b/tests/verify_json.t
index 39773a8285aafb8a3be4c53039fc657749158741..c3990cf7c9adff2faf1ab4cc15068adfa7eb0beb 100644
--- a/tests/verify_json.t
+++ b/tests/verify_json.t
@@ -7,13 +7,11 @@ Test verify-json
   > {"id":"foo","prover":["PyRAT"],"model":"TestNetwork.nnet","property":{"dataset":"test_data.csv","kind":["Robust",0.3]},"time_limit":null,"memory_limit":null,"output_file":null}
   > EOF
 
-  $ chmod u+x bin/pyrat.py
+  $ . ./setup_env.sh
 
   $ bin/pyrat.py --version
   PyRAT 1.1
 
-  $ PATH=$(pwd)/bin:$PATH
-
   $ caisar verify-json --ltag=ProverSpec config.json 2>&1 | ./filter_tmpdir.sh
   [DEBUG]{ProverSpec} Prover-tailored specification:
   ;;; produced by PyRAT/VNN-LIB driver
diff --git a/tests/xgboost.t b/tests/xgboost.t
index ca7e0904fb86acae4e79aa3c3197b331f3f0c1bb..4c73ef71156a277add162db5166805682e85b6b9 100644
--- a/tests/xgboost.t
+++ b/tests/xgboost.t
@@ -1,5 +1,5 @@
 Test verify
-  $ PATH=$(pwd)/bin:$PATH
+  $ . ./setup_env.sh
 
   $ caisar verify-xgboost ../lib/xgboost/example/california.json ../lib/xgboost/example/california.csv --prover CVC5 2>&1 | ./filter_tmpdir.sh
   result: Unknown