[SAVer] Reworked tests.

ovo.opam

@@ -9,7 +9,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst"] {dev}
+  ["dune" "subst" "--root" "."] {dev}
   [
     "dune"
     "build"
@@ -17,7 +17,8 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files=false"
+    "--promote-install-files"
+    "false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}

src/verification.ml

@@ -138,7 +138,7 @@ let call_prover ~limit config (prover : Why3.Whyconf.config_prover) driver env
              = Int.of_string (Re__Core.Group.get g 2)
           then Call_provers.Valid
           else Call_provers.Invalid
-        | None -> assert false
+        | None -> Call_provers.HighFailure
         (* Any other answer than HighFailure should 
          * never happen as we do not define
          * anything in SAVer's driver *))

tests/dune

@@ -4,6 +4,7 @@
    TestNetwork.nnet
    TestNetworkONNX.onnx
    TestSVM.ovo
+   test_data.csv
    bin/pyrat.py
    bin/Marabou
    bin/saver

tests/simple_ovo.t

@@ -20,16 +20,15 @@ Test verify
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
+  $ caisar verify -L . --format whyml --prover=SAVer --dataset-csv=test_data.csv - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
   > theory T
-  >     use TestSVM.AsArray
+  >     use TestSVM.SVM
   >     use ieee_float.Float64
   >     use caisar.IOShape
+  >     use caisar.SVM
   > 
-  >     goal G: forall x1 x2 x3.
-  >        (0.0:t) .< x1 .< (0.5:t) ->
-  >        let (y1,_) = svm_apply x1 x2 x3 in
-  >        (0.0:t) .< y1 .< (0.5:t)
+  >      goal G: forall a : input_type.
+  >      robust_to SVM.svm_apply a (8.0:t)
   > end
   > EOF
   <autodetect>0 prover(s) added
@@ -43,5 +42,4 @@ Test verify
   <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 G: High failure

tests/test_data.csv

+# 1 3
+1,0.5,0.5,0.0,