diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index a62abbfff70efbb37ff9aa4716bda3906694ae55..d3d65b4f3bf95ed53b8aa2bf0ac6b260fd33f90c 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -14,8 +14,10 @@ abstract class LeonOptionDef[+A] {
     if (usageRhs.isEmpty) s"--$name"
     else s"--$name=$usageRhs"
   }
-  def usageDescs = usageDesc.split("\n").toList
-  def helpString = f"${usageDesc}%-21s ${description}"
+  def helpString = {
+    val (hd :: tl) = description.split("\n").toList
+    (f"$usageDesc%-21s $hd" :: ( tl map (" " * 22 + _))).mkString("\n")
+  }
 
   private def parseValue(s: String)(implicit reporter: Reporter): A = {
     try { parser(s) }
@@ -83,10 +85,10 @@ object OptionParsers {
     case _  => throw new IllegalArgumentException
   }
   def seqParser[A](base: OptionParser[A]): OptionParser[Seq[A]] = s => {
-    s.split(",").map(base)
+    s.split(",").filter(_.nonEmpty).map(base)
   }
   def setParser[A](base: OptionParser[A]): OptionParser[Set[A]] = s => {
-    s.split(",").map(base).toSet
+    s.split(",").filter(_.nonEmpty).map(base).toSet
   }
 
 }
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 153a28a763fc0f5c99db021afefb5339134a36ec..17f431413f77fabeb2ad1ad58fb7b75c06678d16 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -54,12 +54,7 @@ object Main {
     reporter.info("")
 
     for (opt <- (MainComponent.definedOptions ++ SharedOptions.definedOptions).toSeq.sortBy(_.name)) {
-      val (uhead :: utail) = opt.usageDescs
-      reporter.info(f"${opt.usageDesc}%-20s ${uhead}")
-      for(u <- utail) {
-        reporter.info(f"${""}%-20s ${u}")
-      }
-
+      reporter.info(opt.helpString)
     }
     reporter.info("")
     reporter.info("Additional options, by component:")
diff --git a/src/main/scala/leon/SharedOptions.scala b/src/main/scala/leon/SharedOptions.scala
index 41dfe68dfe6b2a9d9834d474547a63a3a1ced7f6..a5e7e66350ab351003db479bc19214ce9dc02e8a 100644
--- a/src/main/scala/leon/SharedOptions.scala
+++ b/src/main/scala/leon/SharedOptions.scala
@@ -22,7 +22,7 @@ object SharedOptions extends LeonComponent {
 
   case object SelectedSolvers extends LeonOptionDef[Set[String]] {
     val name = "solvers"
-    val description = "Use solvers s1, s2, ... in parallel (default: fairz3)"
+    val description = "Use solvers s1, s2,...\n" + solvers.SolverFactory.availableSolversPretty
     val default = Set("fairz3")
     val parser = setParser(stringParser)
     val usageRhs = "s1,s2,..."
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index c897fc259fcace479f005957934323eceb60f0f7..21a56c5b40f31119598488a8fc4df9c4bc04ce31 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -29,6 +29,11 @@ object SolverFactory {
     "unrollz3"       -> "Native Z3 with leon-templates for unfolding",
     "enum"           -> "Enumeration-based counter-example-finder"
   )
+  
+  val availableSolversPretty = "Available: " +
+    solvers.SolverFactory.definedSolvers.toSeq.sortBy(_._1).map {
+      case (name, desc) =>  f"\n  $name%-14s : $desc"
+    }.mkString("")
 
   def getFromSettings(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
     getFromName(ctx, program)(ctx.findOptionOrDefault(SharedOptions.SelectedSolvers).toSeq : _*)
@@ -71,7 +76,7 @@ object SolverFactory {
     }
 
     def showSolvers() = {
-      ctx.reporter.error("Available:\n" + definedSolvers.map {"  - " + _}.mkString("\n"))
+      ctx.reporter.error(availableSolversPretty)
       ctx.reporter.fatalError("Aborting Leon...")
     }