diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index a0a9c9d92ee78397cce95dd0a52042fa8bc63330..f079399f9995e409b6b72881ef8f81d92c273556 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -25,8 +25,10 @@ abstract class LeonOptionDef[+A] {
     try { parser(s) }
     catch {
       case _ : IllegalArgumentException =>
-        reporter.error(s"Invalid option usage: $usageDesc")
-        Main.displayHelp(reporter, error = true)
+        reporter.fatalError(
+          s"Invalid option usage: --$name\n" +
+          "Try 'leon --help' for more information."
+        )
     }
   }
 
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index f238d4a854bd881c74a3205ef5b727a220e34ae1..db49d0425e39ac888badb90c97aa7c8432d0ee96 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -116,8 +116,10 @@ object Main {
       }
       // Find respective LeonOptionDef, or report an unknown option
       val df = allOptions.find(_. name == name).getOrElse{
-        initReporter.error(s"Unknown option: $name")
-        displayHelp(initReporter, error = true)
+        initReporter.fatalError(
+          s"Unknown option: $name\n" +
+          "Try 'leon --help' for more information."
+        )
       }
       df.parse(value)(initReporter)
     }
diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala
index e8455147a4e8eea9f141ba80fc8362390d4540db..865d5564798dcc5af760177a3ae9f66cf8239485 100644
--- a/src/main/scala/leon/synthesis/rules/CEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGIS.scala
@@ -14,7 +14,7 @@ case object CEGIS extends CEGISLike[TypeTree]("CEGIS") {
       grammar = Grammars.typeDepthBound(Grammars.default(sctx, p), 2), // This limits type depth
       rootLabel = {(tpe: TypeTree) => tpe },
       optimizations = false,
-      maxUnfoldings = 7
+      maxUnfoldings = 5
     )
   }
 }
@@ -26,7 +26,7 @@ case object CEGIS2 extends CEGISLike[TaggedNonTerm[TypeTree]]("CEGIS2") {
       grammar = TaggedGrammar(base),
       rootLabel = TaggedNonTerm(_, Tags.Top, 0, None),
       optimizations = true,
-      maxUnfoldings = 7
+      maxUnfoldings = 5
     )
   }
 }
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 06a89f32332335da53f921aba54c55fdfec4b378..3f12c920759e26dd073167994b31e3a8e60f1bef 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -450,7 +450,6 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
             evaluator.eval(eq, p.as.zip(ins).toMap)
         }
         timers.testForProgram.stop()
-        val l = timers.testForProgram.last
 
         cTreeFd.fullBody = origImpl