diff --git a/src/autodetect.ml b/src/autodetect.ml
index 3ab29fcb3875ca3c17bd391190a6afedf5b28b2c..52f38e5ee2a81603e8035e6ee70a053f4423b1ef 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_TEST") 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..a80cf6d2e97c195e4ba52254488c05e7ffd00b06 100644
--- a/tests/aimos.t
+++ b/tests/aimos.t
@@ -11,6 +11,7 @@ Test verify
AIMOS 1.0
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify -L . --format whyml --prover=AIMOS --dataset=test_data.csv - 2>&1 <<EOF
> theory ACASXU_P5
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 5fee7ec434876b149122756fbe86229d36456e81..8d28c231e13fecf2bc7971f6f997b81bec5cc1eb 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -32,29 +32,7 @@ Test autodetect
$ 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
- <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/aimos --version) > $TMPFILE 2>&1
- <autodetect>Run: ($TESTCASE_ROOT/bin/abcrown.sh --version) > $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>Run: ($TESTCASE_ROOT/bin/cvc5 --version) > $TMPFILE 2>&1
- <autodetect>0 prover(s) added
- <autodetect>Generating strategies:
- <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
- <autodetect>Found prover CVC5 version 1.0.2, OK.
- <autodetect>Found prover Marabou version 1.0.+, OK.
- <autodetect>Found prover PyRAT version 1.1, OK.
- <autodetect>Found prover PyRAT version 1.1 (alternative: VNNLIB)
- <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
- <autodetect>Found prover nnenum version dummy-version, OK.
- <autodetect>Found prover alpha-beta-CROWN version dummy-version, OK.
- <autodetect>Found prover alpha-beta-CROWN version dummy-version (alternative: ACAS)
- <autodetect>Found prover SAVer version v1.0, OK.
- <autodetect>Found prover AIMOS version 1.0, OK.
- <autodetect>11 prover(s) added
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin caisar config -d -v 2>&1 | ./filter_tmpdir.sh
AIMOS 1.0
Alt-Ergo 2.4.0
CVC5 1.0.2
diff --git a/tests/cvc5.t b/tests/cvc5.t
index e55696f37171cd8dc25fa4c1a6da7d5c7d17c4d1..cd2a68e87cb9c9031cbfacebba5d0980a9b94851 100644
--- a/tests/cvc5.t
+++ b/tests/cvc5.t
@@ -5,6 +5,7 @@ Test verify
This is cvc5 version 1.0.2 [git tag 1.0.2 branch HEAD]
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify -L . --format whyml --prover=CVC5 --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory CVC5
@@ -231,4 +232,4 @@ Test verify
(check-sat)
(get-info :reason-unknown)
- Goal G: Unknown (unknown)
+ Goal G: Timeout
diff --git a/tests/dataset.t b/tests/dataset.t
index 0e965840cde1604939d858d4ed9e0c710be4bd89..3a886a0d730ff2d083b11c8e975ef8770efa179f 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -13,6 +13,7 @@ Test verify on dataset
1.0.+
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify -L . --format whyml --ltag=ProverSpec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
diff --git a/tests/define.t b/tests/define.t
index b698beb81e1d88d7926f59610d0a8cd501fdbe54..262c67457910fe9496d62a84813a8f08ce75f833 100644
--- a/tests/define.t
+++ b/tests/define.t
@@ -6,6 +6,7 @@ Test interpretation of on-the-fly definition of toplevel constants
PyRAT 1.1
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ cat > file.mlw <<EOF
> theory T
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 28695a744ada60305f2c3a18842df557ff5e74ce..5f2dc73451882f8158c88108382adebc4c388ab9 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -6,6 +6,7 @@ Test interpret on acasxu
PyRAT 1.1
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 8ce1d6076853bf3f506625105d98ae35f5600ea9..e9551bfdfaffee4abbd1b34036741829aac83a0f 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -10,6 +10,7 @@ Test interpret on dataset
1.0.+
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
diff --git a/tests/marabou.t b/tests/marabou.t
index 8ded847e994ab771f5e3bf150ec3b166eaba270d..bc9dc999def19953cbf7f9ffb726aacea541ff22 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -5,6 +5,7 @@ Test verify
1.0.+
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
diff --git a/tests/pyrat.t b/tests/pyrat.t
index 4c36cd0903f0aedcd140eea9e243a4611c96f20e..6a9ba9365404fa5efa397f9c34efcaf1195c117b 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -5,6 +5,7 @@ Test verify
PyRAT 1.1
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index f6512e2bc0419ff272fc531ef9f4d5caa1f52898..422a318f9eead41e2ac255a45ce39e9bfd1aa00c 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -5,6 +5,7 @@ Test verify
PyRAT 1.1
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT_ONNX
diff --git a/tests/saver.t b/tests/saver.t
index a05fc8d70b7392ac79a4251c7a461197041700d3..94d471bde24d68110148a3b627b6a02dab1af4db 100644
--- a/tests/saver.t
+++ b/tests/saver.t
@@ -10,6 +10,7 @@ Test verify
v1.0
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify -L . --format whyml --prover=SAVer --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
diff --git a/tests/verify_json.t b/tests/verify_json.t
index 39773a8285aafb8a3be4c53039fc657749158741..e0cf12c5b7f42ae652dac9abd253baba762d886b 100644
--- a/tests/verify_json.t
+++ b/tests/verify_json.t
@@ -13,6 +13,7 @@ Test verify-json
PyRAT 1.1
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify-json --ltag=ProverSpec config.json 2>&1 | ./filter_tmpdir.sh
[DEBUG]{ProverSpec} Prover-tailored specification:
diff --git a/tests/xgboost.t b/tests/xgboost.t
index ca7e0904fb86acae4e79aa3c3197b331f3f0c1bb..de83fadc188b1240bb0eea1a7d67e813975f74c3 100644
--- a/tests/xgboost.t
+++ b/tests/xgboost.t
@@ -1,6 +1,6 @@
Test verify
$ PATH=$(pwd)/bin:$PATH
+ $ CAISAR_AUTODETECT_TEST=$(pwd)/bin
$ caisar verify-xgboost ../lib/xgboost/example/california.json ../lib/xgboost/example/california.csv --prover CVC5 2>&1 | ./filter_tmpdir.sh
- result: Unknown
- (unknown)
+ result: Valid