diff --git a/doc/contributing.rst b/doc/contributing.rst
index 2b2ad7231dbca78d55c818e987ffbf48ef5367e1..4cd3c005682b5c344e747901604bfa9e4b853fd9 100644
--- a/doc/contributing.rst
+++ b/doc/contributing.rst
@@ -35,12 +35,14 @@ Setting up a development environment
With an Opam switch
-------------------
-Need to download `ocaml language server <https://github.com/ocaml/ocaml-lsp>`_, `ocamlformat <https://github.com/ocaml-ppx/ocamlformat>`_ v0.25.1 and
-`ocp-indent <https://github.com/OCamlPro/ocp-indent>`_.
+Once an opam switch is setup, one needs to download `ocaml language server <https://github.com/ocaml/ocaml-lsp>`_, `ocamlformat <https://github.com/ocaml-ppx/ocamlformat>`_ v0.25.1 and `ocp-indent <https://github.com/OCamlPro/ocp-indent>`_.
With nix-shell
--------------
-TODO
+
+With nix setup as detailed in :ref:`nix`, typing `nix develop` will create a
+shell environment tailored for CAISAR development. You can build CAISAR by
+following the :ref:`source` instructions.
.. index:: Prover;prover
diff --git a/doc/foreword.rst b/doc/foreword.rst
index 44d718483f5f9f3dda7bc8d12e6803858b321f34..fc1bf68cc4d6caaeaa26d37561427401876541ef 100644
--- a/doc/foreword.rst
+++ b/doc/foreword.rst
@@ -30,17 +30,6 @@ provide both the specification language, called WhyML, and the infrastructure
needed to interoperate with external provers. These are generally called
*provers*, although some of them do not directly provide a logical proof.
-.. _supported-provers:
-
-Supported Provers
------------------
-
-.. toctree::
- :maxdepth: 2
- :caption: Supported Provers:
-
- provers
-
Availability
------------
diff --git a/doc/index.rst b/doc/index.rst
index 5aa4f529d22ca5104e766a9b6c3cbeb701b20c0c..694f329274fa453c6fa500fdf42041a85257dcf1 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -35,6 +35,7 @@ This work has been partly supported by the `Confiance.ai`_ program.
examples
interpretation
contributing
+ provers
genindex
CAISAR website <http://www.caisar-platform.com>
diff --git a/doc/installation.rst b/doc/installation.rst
index 62199f954fef870d5739735ae668254ee4b7b3ae..cb1055b0c444992ad675b71559adb39287ba51c9 100644
--- a/doc/installation.rst
+++ b/doc/installation.rst
@@ -53,6 +53,8 @@ To run the CAISAR Docker image, do the following:
$ docker run -it laiser/caisar:pub sh
+.. _nix:
+
Install through Nix
-------------------
@@ -101,6 +103,8 @@ It will contain the ocaml toolchain already setup and installed, and the ocaml l
$ nix develop
+.. _source:
+
Compile from source
-------------------
diff --git a/doc/provers.rst b/doc/provers.rst
index bfabe39b72d20b707f8ce0295e1495d3093994c2..49d3388c9ec79d14ffdd4fb527ae8c4ecc45e0ba 100644
--- a/doc/provers.rst
+++ b/doc/provers.rst
@@ -1,3 +1,7 @@
+.. _provers:
+
+Supported provers
+*****************
The supported provers are the following:
@@ -31,3 +35,10 @@ SMT solvers
-----------
Standard SAT/SMT solvers that support the SMT-LIBv2 input language.
As of now, only CVC5 had been tested.
+
+
+.. warning ::
+ Marabou and VNN-LIB provers (PyRAT, alpha-beta-CROWN) do not accept strict
+ inequalities. Thus CAISAR treats strict inequalities as non-strict ones. We
+ are aware this is incorrect in general, but it is as of today the common
+ practice for the community.
diff --git a/doc/usage.rst b/doc/usage.rst
index 62e5bd397e61ca6f3724dca14db6d9ebcf6f63b5..07715280450f6182be71f9cb372875b8041d6453 100644
--- a/doc/usage.rst
+++ b/doc/usage.rst
@@ -17,16 +17,15 @@ Command line options
* ``-D name:value`` or ``--define=name:value``: define a declared constant ``name`` with the given value ``value``. Constant must be declared in the theory file.
* ``--dataset=FILE``: Path of a dataset file. To be deprecated.
-* ``-g theory,..,theory:goal,..,goal``: Verify only the ``goal`` in the
- ``theory``. Theory must already be defined in the specification file. It is
- possible to verify all goals for one ``theory`` only using ``theory:*``
+* ``-g [theory]:goal,..,goal`` or ``--goal [theory]:goal,...,goal``: Verify only the ``goal`` in the ``theory``. Theory must already be defined in the specification file. When no theory is provided, verify the specified goals for all theories.
+* ``-t theory`` or ``--theory=theory``: Verify all goals in ``theory``.
* ``-m MEM`` or ``--memlimit=MEM``: Memory limit. ``MEM`` is intended in megabytes
(MB); (GB) and (TB) can also be specified. Default: 4000MB.
* ``-t TIME`` or ``--timelimit=TIME``: Time limit. ``TIME`` is intended in seconds (s); minutes (m) and hours (h) can also be specified.
(MB), (GB) and (TB) can also be specified. Default: 20s.
* ``-p PROVER`` or ``--prover=PROVER``. Prover to use. Support is provided for
the following: Marabou, PyRAT, SAVer, AIMOS, CVC5, nnenum, alpha-beta-CROWN.
- See :ref:`supported-provers` for a detailed description of each prover
+ See :ref:`provers` for a detailed description of each prover
capacity.
* ``--prover-altern=VAL``: alternative prover alternatives to use. Prover
alternatives are prover-specific configurations that help provers to better perform on specific problems. Supported prover alternative are ``ACAS`` for alpha-beta-CROWN and PyRAT.
@@ -60,7 +59,7 @@ CAISAR relies on external provers to work. You must install
them first, then point CAISAR to their location. Please
refer to each prover documentation to install them.
-CAISAR already support several provers, listed in :ref:`supported-provers`.
+CAISAR already support several provers, listed in :ref:`provers`.
Assuming you have installed a prover with an entry in the
``caisar-detection.conf`` file, you can register the prover to CAISAR using the
following command: ``PATH=$PATH:/path/to/solver/executable caisar config -d``.
@@ -79,7 +78,7 @@ documentation to get a first grasp on using WhyML.
Provided a file ``trust.why`` containing a goal to verify, the command ``caisar verify --prover=PROVER trust.why``
will verify the goals using the specified prover. A list of
-supported provers is available in :ref:`supported-provers`. The prover
+supported provers is available in :ref:`provers`. The prover
must already be registered by CAISAR. Currently, only one
prover can be selected at a time; future work will allow
selecting multiple provers and orchestrate verification