diff --git a/doc/limitations.rst b/doc/limitations.rst index 88ea422365e6907f0b7ec15d556cb29e48ce4dbd..374225b0bc4a952b52c87bddd465f9d0bc5f8975 100644 --- a/doc/limitations.rst +++ b/doc/limitations.rst @@ -51,6 +51,7 @@ By default Leon assumes that unbounded data types can be arbitrarily large and that all well-founded recursive functions have enough stack space to finish their computation. Thus a verified program may crash at run-time due to: + * stack overflow * heap overflow diff --git a/doc/options.rst b/doc/options.rst index 909bdacd0cdf1e0f0887a98e2db390427396cb00..96dfcb94fe1f2df9c5e4d4d0348de0b5b834a6ff 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -14,7 +14,7 @@ you can do it by using a single dash ``-``. For example, ``-Ybrowse:typer``. The rest of this section presents all command-line options that Leon recognizes. Choosing which Leon feature to use ---------------------------- +---------------------------------- The first group of options determine which feature of Leon will be used. These options are mutually exclusive. By default, ``--verify`` is chosen.