diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index d3d65b4f3bf95ed53b8aa2bf0ac6b260fd33f90c..e8b653a5b172615e7c188c4f2d5c82f66c2bc673 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -15,8 +15,7 @@ abstract class LeonOptionDef[+A] {
     else s"--$name=$usageRhs"
   }
   def helpString = {
-    val (hd :: tl) = description.split("\n").toList
-    (f"$usageDesc%-21s $hd" :: ( tl map (" " * 22 + _))).mkString("\n")
+    f"$usageDesc%-22s" + description.replaceAll("\n", "\n" + " " * 22)
   }
 
   private def parseValue(s: String)(implicit reporter: Reporter): A = {
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 72e8c3fb9a4e58d60af43a69d1ff1f71729524f6..e9eb7b6e50307f7cb797e15358f4e7f175ec6cb0 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -51,6 +51,7 @@ object Main {
   lazy val allOptions: Set[LeonOptionDef[Any]] = allComponents.flatMap(_.definedOptions)
 
   def displayHelp(reporter: Reporter, error: Boolean) = {
+    reporter.info("Top-level options:")
     reporter.info("")
 
     for (opt <- (MainComponent.definedOptions ++ SharedOptions.definedOptions).toSeq.sortBy(_.name)) {
@@ -70,6 +71,11 @@ object Main {
     exit(error)
   }
 
+  def displayVersion(reporter: Reporter) = {
+    reporter.info("Leon verification and synthesis tool (http://leon.epfl.ch/)")
+    reporter.info("")
+  }
+
   private def exit(error: Boolean) = sys.exit(if (error) 1 else 0)
 
   def processOptions(args: Seq[String]): LeonContext = {
@@ -133,6 +139,7 @@ object Main {
     val verifyF      = ctx.findOptionOrDefault(optVerify)
 
     if (helpF) {
+      displayVersion(ctx.reporter)
       displayHelp(ctx.reporter, error = false)
     } else {
       val pipeBegin: Pipeline[List[String], Program] =