From 7b3b5861a917b8e91776b6dd287c172770c7b816 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 25 Sep 2019 13:22:53 +0200
Subject: [PATCH] [install] installation of external provers

---
 INSTALL.md | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/INSTALL.md b/INSTALL.md
index 20878b6819b..fa0e709d60b 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -70,6 +70,22 @@ so that we can add it to the Frama-C `depext` package.
     # install Frama-C
     opam install frama-c
 
+### Configuring provers for Frama-C/WP
+
+Frama-C/WP uses the Why-3 platform to run external provers for proving ACSL annotations.
+The Why-3 platform and the Alt-Ergo prover are automatically installed _via_ opam
+when installing Frama-C.
+
+However, CVC4 or Z3 are also very efficient provers to be used alternatively or in combination with Alt-Ergo.
+Actually, you can use any prover supported by Why-3 in combination with Frama-C/WP.
+
+Most provers are available on all platforms, although you shall configure Why-3 after installation
+to make them available for Frama-C/WP:
+
+    ```shell
+    why3 config --detect
+    ```
+
 ### Known working configuration
 
 The following set of packages is known to be a working configuration for
-- 
GitLab