diff --git a/src/verification.ml b/src/verification.ml
index dfac916fcf6c5b22553176fa0a02025d0bf283e1..3139df410cb82ebb58e6f4fccaccee73eaec09e9 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -44,8 +44,8 @@ let () =
   Language.register_onnx_support ();
   Language.register_ovo_support ()
 
-let create_env loadpath =
-  let config = Autodetect.autodetection ~debug:true () in
+let create_env ?(debug = false) loadpath =
+  let config = Autodetect.autodetection ~debug () in
   let config =
     let main = Whyconf.get_main config in
     let dft_memlimit = 4000 (* 4 GB *) in
@@ -204,7 +204,7 @@ let call_prover ~limit config (prover : Whyconf.config_prover) driver env
 let verify ?(debug = false) format loadpath ?memlimit ?timeout prover
   ?dataset_csv file =
   if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
-  let env, config = create_env loadpath in
+  let env, config = create_env ~debug loadpath in
   let steplimit = None in
   let steps = match steplimit with Some 0 -> None | _ -> steplimit in
   let limit =
diff --git a/tests/autodetect.t b/tests/autodetect.t
index abd5d8866a803d2a928163ae5c4ddd19a463a77b..ff2c0b385985bd913d27889c8dd577bbfd4f1dd1 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -20,7 +20,20 @@ Test autodetect
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar config -d
+  $ caisar config -d -vv 2>&1 | ./filter_tmpdir.sh
+  [caisar][DEBUG] Command `config'.
+  [caisar][DEBUG] Automatic detection.
+  <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>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.
+  <autodetect>Found prover SAVer version v1.0, OK.
+  <autodetect>4 prover(s) added
   [caisar] Alt-Ergo 2.4.0
            Marabou 1.0.+
            PyRAT 1.1
diff --git a/tests/marabou.t b/tests/marabou.t
index 3e2b8eb9ae65c6085bd55779a6e9dfb2b449d12d..d0e071ce568abe5d1cffba5f1b5ad25d1aee89bf 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -34,17 +34,6 @@ 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>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.
-  <autodetect>Found prover SAVer version v1.0, OK.
-  <autodetect>4 prover(s) added
   Goal G: Unknown
   ()
   Goal H: Unknown
diff --git a/tests/simple.t b/tests/simple.t
index 55881f4325560f0e1496c6fee28450503c828293..8bc9aa3f18f4e52272066cb5ef738f36baee17d9 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -37,17 +37,6 @@ 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>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.
-  <autodetect>Found prover SAVer version v1.0, OK.
-  <autodetect>4 prover(s) added
   Goal G: Unknown
   ()
   Goal H: Unknown
diff --git a/tests/simple_onnx.t b/tests/simple_onnx.t
index 7deb1576c3c97897a5ceab55d1ddbec625614532..90e92776592749fd819ced349420f7f209202b8a 100644
--- a/tests/simple_onnx.t
+++ b/tests/simple_onnx.t
@@ -29,16 +29,5 @@ 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>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.
-  <autodetect>Found prover SAVer version v1.0, OK.
-  <autodetect>4 prover(s) added
   Goal G: Unknown
   ()
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index 0364904535d9f2c74c994db3ed452cb64fedfc67..2561471424f309a88e24e8b976d50f9f1989951e 100644
--- a/tests/simple_ovo.t
+++ b/tests/simple_ovo.t
@@ -34,15 +34,4 @@ Test verify
   >   goal G: forall a : input_type. 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>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.
-  <autodetect>Found prover SAVer version v1.0, OK.
-  <autodetect>4 prover(s) added
   Goal G: High failure