diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index 13835141137d6ce158071c305dcfe673613cbbd9..904c8cbc84350b19e1b9af886d5daa24b200d5dd 100644
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
@@ -346,7 +346,7 @@ We can then verify the resulting verification problem as before:
 
 It is interesting to remark that, since Marabou does not support disjunctive
 formulas, CAISAR first splits a disjunctive goal formula into conjunctive
-sub-goals, then calls Marabou on each sub-goals, and finally post-processes the
+sub-goals, then calls Marabou on each sub-goal, and finally post-processes the
 sub-results to provide the final result corresponding to the original goal
 formula.
 
diff --git a/doc/foreword.rst b/doc/foreword.rst
index a1460457f0ebada8de7fc1d8b93ad9d8a38d34be..e51ff15f9303c64295cff046bbbdfcd7ef63b70f 100644
--- a/doc/foreword.rst
+++ b/doc/foreword.rst
@@ -29,7 +29,7 @@ The supported provers are the following:
   vector machine verifier based on abstract interpretation,
 * `nnenum <https://github.com/stanleybak/nnenum>`_ a neural network verifier
   that combines abstract interpretation and linear programming techniques,
-* *Classic* SAT/SMT solvers that support the SMT-LIBv2 input language.
+* Standard SAT/SMT solvers that support the SMT-LIBv2 input language.
 
 CAISAR aims to be component-agnostic: it can model and assess the
 trustworthiness of artificial intelligence system that potentially mixes both