diff --git a/README.md b/README.md
index c88daa7775bbb2dbe8fcb90571e956c6433db2d0..4205bbd99593228e84ebf0e4cbfed730ea1b6f38 100644
--- a/README.md
+++ b/README.md
@@ -2,4 +2,14 @@
 
 ## How to add a solver
 Make sure the solver is added to your systems for tests.
-1. Create a `new_solver.drv` in `config/drivers`
+1. Create a `new_solver.drv` in `config/drivers/`.
+A driver is a serie of whyml modules describing the theories
+the solver will use during its call by why3.
+
+1. Add a new field inside of `config/caisar-detection-data.conf`.
+Here, you only need to define the name of the solver's
+executable as well as the supported versions for CAISAR.
+
+Now, the solver will be recognized by CAISAR. However, in
+order to exploit it, you should write a printer of its
+output in `src/printers/`. TODO
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 1dfea43b4f3c55a47808cae80ef11b1b9d280023..3e256ed4d9d3ea6c4bbf094efa30de7eee7574ed 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -31,11 +31,11 @@ driver = "caisar_drivers/pyrat.drv"
 use_at_auto_level = 1
 
 [ATP saver]
-name = "SAVER"
+name = "SAVer"
 exec = "saver"
-version_switch = "--version"
-version_regexp = "PyRAT \\([0-9.]+\\)"
-version_ok  = "1.1"
-command = "%e --model_path %{nnet-onnx} --property_path %f"
-driver = "caisar_drivers/pyrat.drv"
+version_switch = "2>&1 | grep Usage"
+version_regexp = "\\(\\)"
+version_ok = ""
+command = "%e %{svm} %{data}"
+driver = "caisar_drivers/saver.drv"
 use_at_auto_level = 1
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 5bc8e94f01de6d5103253d670e027d718c7b0ecd..fb0fec24292057818449138350811e08b67d2375 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -15,9 +15,13 @@ Test autodetect
   $ bin/Marabou --version
   1.0.+
 
+  $ bin/saver --version
+  1.0
+
   $ PATH=$(pwd)/bin:$PATH
 
   $ caisar config -d
   [caisar] Alt-Ergo 2.4.0
            Marabou 1.0.+
            PyRAT 1.1
+           SAVER 1.0
diff --git a/tests/bin/saver b/tests/bin/saver
new file mode 100644
index 0000000000000000000000000000000000000000..0f7abafedb4c8fb691b167b2f79565d255ebc588
--- /dev/null
+++ b/tests/bin/saver
@@ -0,0 +1,13 @@
+#!/bin/sh
+
+
+case $1 in
+    --version)
+        echo "1.0"
+        ;;
+    *)
+        echo "NN: $1"
+        echo "Goal:"
+        cat $2
+        echo "Unknown"
+esac
diff --git a/tests/dune b/tests/dune
index d62110c4fc1329e713e41fe0b50289b81bd914a8..b112238264cc9efc495b6d525d2c3e1395284aad 100644
--- a/tests/dune
+++ b/tests/dune
@@ -5,4 +5,5 @@
    TestNetworkONNX.onnx
    bin/pyrat.py
    bin/Marabou
+   bin/saver
 ))
diff --git a/tests/marabou.t b/tests/marabou.t
index 2d7b6bf3f0c60c5b76e36b33c75dae626b543a38..60fc43d73c081c75b9c13098a8fb2a62fdd23961 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -38,11 +38,13 @@ Test verify
   <autodetect>Generating strategies:
   <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
   <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: (saver --version) > $TMPFILE 2>&1
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <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>3 prover(s) added
+  <autodetect>Found prover SAVER version 1.0, OK.
+  <autodetect>4 prover(s) added
   Goal G: Unknown
   ()
   Goal H: Unknown
diff --git a/tests/simple.t b/tests/simple.t
index a49bc1f25761ec39850eca84bacbe4c8ff22f9f4..554906274f27565f42f451afcbd2022431d3d327 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -4,7 +4,7 @@ Test verify
   > echo "2.4.0"
   > EOF
 
-  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou
+  $ chmod u+x bin/alt-ergo bin/pyrat.py bin/Marabou bin/saver
 
   $ bin/alt-ergo
   2.4.0
@@ -15,6 +15,9 @@ Test verify
   $ bin/Marabou --version
   1.0.+
 
+  $ bin/saver --version
+  1.0
+
   $ PATH=$(pwd)/bin:$PATH
 
   $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
@@ -38,11 +41,13 @@ Test verify
   <autodetect>Generating strategies:
   <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
   <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: (saver --version) > $TMPFILE 2>&1
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <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>3 prover(s) added
+  <autodetect>Found prover SAVER version 1.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 7509548805f3310b454be91df2a0387d3d506476..419eb106c7814d4de1d5cdef340fd2389d0f6dbb 100644
--- a/tests/simple_onnx.t
+++ b/tests/simple_onnx.t
@@ -33,10 +33,12 @@ Test verify
   <autodetect>Generating strategies:
   <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
   <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
+  <autodetect>Run: (saver --version) > $TMPFILE 2>&1
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <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>3 prover(s) added
+  <autodetect>Found prover SAVER version 1.0, OK.
+  <autodetect>4 prover(s) added
   Goal G: Unknown
   ()