diff --git a/doc/options.rst b/doc/options.rst
index 96dfcb94fe1f2df9c5e4d4d0348de0b5b834a6ff..368526aeeb4b10bbdc042c3852cbf39f2b498a42 100644
--- a/doc/options.rst
+++ b/doc/options.rst
@@ -161,6 +161,10 @@ These options are available by all Leon components:
   * ``unrollz3``
     
     Native Z3, but inductive reasoning happens within Leon (similarly to ``smt-z3``).
+
+  * ``ground``
+
+    Only solves ground verification conditions (without variables) by evaluating them.
   
 * ``--strict``
 
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 42479fa01528baea2e658184a81dc40c631740ca..64cf6e3d771c5f323cd00e14e76844a8ced1bdde 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -37,7 +37,7 @@ object SolverFactory {
     "smt-cvc4-proof" -> "CVC4 through SMT-LIB, in-solver inductive reasoning, for proofs only",
     "smt-cvc4-cex"   -> "CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only",
     "unrollz3"       -> "Native Z3 with leon-templates for unfolding",
-    "ground"         -> "Only solves ground terms by evaluating them",
+    "ground"         -> "Only solves ground verification conditions by evaluating them",
     "enum"           -> "Enumeration-based counter-example-finder"
   )