Minor edits in docs. (#8540)

diff --git a/docs/index.rst b/docs/index.rst
index 746b18daccf2e39ae5beb1b35d9539ffdf06eac9..f613198902cb70832c58c92c5ef8874f43fed6da 100644 (file)
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -2,8 +2,9 @@ cvc5 Documentation
 ==================
 
 **cvc5** is an open-source automatic theorem prover for Satisfiability Modulo
-Theories (SMT) problems in a large number of theories and their combination.
-**cvc5** is the successor of `CVC4 <https://cvc4.cs.stanford.edu>`_ and is
+Theories (SMT) problems that supports a large number of theories and their 
+combination.
+It is the successor of `CVC4 <https://cvc4.cs.stanford.edu>`_ and is
 intended to be an open and extensible SMT engine.
 
 This space provides all documentation related to using cvc5.

diff --git a/docs/output-tags.rst b/docs/output-tags.rst
index 689e03ab826cebe2822a36b69d66a5bba2fdf6c4..51bce612a352d9f0f2474359266b833ad8332cfd 100644 (file)
--- a/docs/output-tags.rst
+++ b/docs/output-tags.rst
@@ -2,9 +2,9 @@ Output tags
 ===========
 
 cvc5 supports printing information about certain aspects of the solving process
-that is intended for regular users. These can be enabled using the
+that is intended for regular users. This feature can be enabled using the
 :ref:`output <lbl-option-output>` option.
 
-As of now, the following output tags are supported:
+The following output tags are currently supported:
 
 .. include-build-file:: output_tags_generated.rst

diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst
index 8a3848bd43ca9efbdd1b9201b222776685552ed6..f9d5b338b84e00c4096edd5db15dc5847aa489c8 100644 (file)
--- a/docs/resource-limits.rst
+++ b/docs/resource-limits.rst
@@ -9,7 +9,7 @@ All these options take a single non-negative number as an argument where giving
 The limits configured using :ref:`tlimit <lbl-option-tlimit>` and :ref:`rlimit <lbl-option-rlimit>` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver <cvc5::Solver>` object, respectively.
 In contrast to that, :ref:`tlimit-per <lbl-option-tlimit-per>` and :ref:`rlimit-per <lbl-option-rlimit-per>` apply to every check individually (:cpp:func:`checkSat <cvc5::Solver::checkSat>`, :cpp:func:`checkSatAssuming <cvc5::Solver::checkSatAssuming>`, :cpp:func:`checkEntailed <cvc5::Solver::checkEntailed>`, etc).
 
-Except for the overall time limit (see below), the limits are checked by cvc5 itself and the solver is in a safe state after exhausting a limit.
+Except for the overall time limit (see below), the limits are checked by cvc5 itself. This means that the solver remains in a safe state after a limit has been reached.
 Due to the way cvc5 checks these limits (see below), cvc5 may not precisely honor per-call time limits: if a subroutine requires a long time to finish without spending resources itself, cvc5 only realizes afterwards that the timeout has (long) passed.