From 0b7feab9c12ebba8236ba4547453c46dcc5f3b6b Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 28 Apr 2015 20:19:36 +0200
Subject: [PATCH] doc: Also fix CVC4 solvers
---
doc/options.rst | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/doc/options.rst b/doc/options.rst
index f55fa74fe..909bdacd0 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -127,12 +127,14 @@ These options are available by all Leon components:
* ``smt-cvc4-cex``
CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only.
+ Recursive functions are not unrolled, but encoded through the
+ ``define-funs-rec`` construct available in the new SMTLIB-2.5 standard.
Currently, this solver does not handle higher-order functions.
* ``smt-cvc4-proof``
- CVC4 through SMT-LIB, for proofs only. Inductive reasoning happens
- within the solver, through use of the SMTLIB-2.5 standard.
+ CVC4 through SMT-LIB, for proofs only. Functions are encoded as in
+ ``smt-cvc4-cex``.
Currently, this solver does not handle higher-order functions.
* ``smt-z3``
--
GitLab