Skip to content
Snippets Groups Projects
Commit 0b7feab9 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

doc: Also fix CVC4 solvers

parent 4010df60
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 4 additions and 2 deletions
doc/options.rst
+ 4
− 2
View file @ 0b7feab9
...@@ -127,12 +127,14 @@ These options are available by all Leon components: ...@@ -127,12 +127,14 @@ These options are available by all Leon components:
* ``smt-cvc4-cex`` * ``smt-cvc4-cex``
CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only. 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. Currently, this solver does not handle higher-order functions.
* ``smt-cvc4-proof`` * ``smt-cvc4-proof``
CVC4 through SMT-LIB, for proofs only. Inductive reasoning happens CVC4 through SMT-LIB, for proofs only. Functions are encoded as in
within the solver, through use of the SMTLIB-2.5 standard. ``smt-cvc4-cex``.
Currently, this solver does not handle higher-order functions. Currently, this solver does not handle higher-order functions.
* ``smt-z3`` * ``smt-z3``
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment