diff --git a/ovo.opam b/ovo.opam
index 6adaf24e86727f788f917646194c92d5384b7a05..443011ba10741186a42aa200d66e0d79e3685ece 100644
--- a/ovo.opam
+++ b/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}
diff --git a/src/verification.ml b/src/verification.ml
index 2c5f03ec2e397b12ea3dfc74411fcc3cdb56078e..c16475ab20839c8d382000f7bcf1e4342d26f634 100644
--- a/src/verification.ml
+++ b/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 *))
diff --git a/tests/dune b/tests/dune
index f4fdcc24dab63d03a62cde53b9cf75f47e3c1414..663a7daf12887e1aaa7cb23a2d47e3668e9e6f9f 100644
--- a/tests/dune
+++ b/tests/dune
@@ -4,6 +4,7 @@
    TestNetwork.nnet
    TestNetworkONNX.onnx
    TestSVM.ovo
+   test_data.csv
    bin/pyrat.py
    bin/Marabou
    bin/saver
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index 97fc618de368f6487d05ea9b965880d89f574db3..ad3aaafbe2d82f895c32c8d1cf7d729baf7f098e 100644
--- a/tests/simple_ovo.t
+++ b/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
diff --git a/tests/test_data.csv b/tests/test_data.csv
new file mode 100644
index 0000000000000000000000000000000000000000..a48580a3ee25ab5d044f5a725a380701dbe5063a
--- /dev/null
+++ b/tests/test_data.csv
@@ -0,0 +1,2 @@
+# 1 3
+1,0.5,0.5,0.0,