Merge branch 'fix/michele/debug-autodetect-in-verification' into 'master'

Do not set debug flag for autodetection in each verification

See merge request laiser/caisar!35

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 =

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

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

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

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
   ()

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