diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 5e2585eb5612e34cb0af33c9daa4b75c43dc4d0c..f643c3a241957a7f76501f12b18974562b4f3ff6 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -18,7 +18,7 @@ object Settings {
   var useCores : Boolean = false
   var pruneBranches : Boolean = false
   var solverTimeout : Option[Int] = None
-  var luckyTest : Boolean = true
+  //var luckyTest : Boolean = true
   var verifyModel : Boolean = true
   var useQuickCheck : Boolean = false
   var useParallel : Boolean = false
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index afc5fa35d441c099da969c2e5789ea48ea229643..bdba7fb647cc3ba0b30efe2548926ba4ce8cc469 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -35,7 +35,7 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
     "  --cores              Use UNSAT cores in the unrolling/refinement step" + "\n" +
     "  --quickcheck         Use QuickCheck-like random search" + "\n" +
     "  --parallel           Run all solvers in parallel" + "\n" +
-    "  --noLuckyTests       Do not perform additional tests to potentially find models early" + "\n" +
+    //"  --noLuckyTests       Do not perform additional tests to potentially find models early" + "\n" +
     "  --noverifymodel      Do not verify the correctness of models returned by Z3" + "\n" +
     "  --debug=[1-5]        Debug level" + "\n" +
     "  --tags=t1:...        Filter out debug information that are not of one of the given tags" + "\n" +
@@ -63,7 +63,7 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
         case "cores"         =>                     leon.Settings.useCores = true
         case "quickcheck"    =>                     leon.Settings.useQuickCheck = true
         case "parallel"      =>                     leon.Settings.useParallel = true
-        case "noLuckyTests"  =>                     leon.Settings.luckyTest = false
+        //case "noLuckyTests"  =>                     leon.Settings.luckyTest = false
         case "noverifymodel" =>                     leon.Settings.verifyModel = false
         case "imperative"     =>                    leon.Settings.synthesis = false;
                                                     leon.Settings.transformProgram = true;
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 726a7922a59de70142369301a5e57917c4b1ad2e..12953a93b1abf88af4eea0765ce4dfbc3a71032a 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -7,6 +7,10 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
   val name = "Analysis"
   val description = "Leon Verification"
 
+  override def definedOptions = Set(
+    LeonFlagOptionDef("no-luck", "--no-luck", "Disable early model detection in solving loop.")
+  )
+
   def run(ctx: LeonContext)(program: Program) : VerificationReport = {
     new Analysis(program, ctx.reporter).analyse
   }