diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index 4cd05cc65b6ebf65f62a3db3e02f51d14d5f1e1e..51a12618958bc3085de4d76007679822dba63674 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -56,7 +56,7 @@ object SharedOptions extends LeonComponent {
     val parser: String => Set[DebugSection] = setParser[Set[DebugSection]](debugParser)(_).flatten
   }
 
-  val optTimeout = LeonLongOptionDef("timeout", "Set a timeout for each verification/repair (in sec.)", 0L, "t")
+  val optTimeout = LeonLongOptionDef("timeout", "Set a timeout for attempting to prove a verification condition/ repair a function (in sec.)", 0L, "t")
 
   override val definedOptions: Set[LeonOptionDef[Any]] = Set(
     optStrictPhases,
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 06a7fb4c4068722cac573395895cd104c9758e05..4e53b8b9e00b326645bb68daf105f8895afaf671 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -24,7 +24,7 @@ object SolverFactory {
     "smt-cvc4"       -> "CVC4 through SMT-LIB",
     "smt-z3"         -> "Z3 through SMT-LIB",
     "smt-z3-q"       -> "Z3 through SMT-LIB, with quantified encoding",
-    "smt-cvc4-proof" -> "CVC4 through SMT-LIB, in-solver inductive reasonning, for proofs only",
+    "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",
     "enum"           -> "Enumeration-based counter-example-finder"