diff --git a/src/cp/CPPlugin.scala b/src/cp/CPPlugin.scala
index 3c8a1441859de0069129c7f22064a1ce3341ef29..fd0d3b64e1a2862fee6122106895415b2bfbc397 100644
--- a/src/cp/CPPlugin.scala
+++ b/src/cp/CPPlugin.scala
@@ -28,6 +28,7 @@ class CPPlugin(val global: Global) extends Plugin {
     "  -P:constraint-programming:CAV                CAV 2011 settings. In progress." + "\n" +
     "  -P:constraint-programming:prune              (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" +
     "  -P:constraint-programming:cores              (with CAV) Use UNSAT cores in the unrolling/refinement step." + "\n" +
+    "  -P:constraint-programming:noLuckyTests       (with CAV) Do not perform additional tests to potentially find models early." + "\n" +
     "  -P:constraint-programming:scalaEval          (with CAV) Use functions stored in constraints to evaluate models."
   )
 
@@ -47,6 +48,7 @@ class CPPlugin(val global: Global) extends Plugin {
         case "CAV"       =>                      { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
         case "prune"     =>                      purescala.Settings.pruneBranches = true
         case "cores"     =>                      purescala.Settings.useCores = true
+        case "noLuckyTests" =>                   purescala.Settings.luckyTest = false
         case "scalaEval" =>                      cp.Settings.useScalaEvaluator = true
         case s if s.startsWith("unrolling=") =>  purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
         case s if s.startsWith("functions=") =>  purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
diff --git a/src/cp/RuntimeSettings.scala b/src/cp/RuntimeSettings.scala
index 813ebb88470e61db972ff62f307bc1a20d0b91f5..051ea9b9490c8418bad63760099de3ae50fdd95b 100644
--- a/src/cp/RuntimeSettings.scala
+++ b/src/cp/RuntimeSettings.scala
@@ -12,6 +12,7 @@ package cp
   var useCores : Boolean = purescala.Settings.useCores 
   var pruneBranches : Boolean = purescala.Settings.pruneBranches 
   var solverTimeout : Option[Int] = purescala.Settings.solverTimeout 
+  var luckyTest : Boolean = purescala.Settings.luckyTest 
 
   var useScalaEvaluator : Boolean = Settings.useScalaEvaluator
 }
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 08945e8d82f0581c761b7f8db31fa99f90cd8bc1..8180ef78cc41a66ba801062140c09121b35e73d8 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -37,7 +37,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
     "  -P:funcheck:CAV                CAV 2011 settings. In progress." + "\n" +
     "  -P:funcheck:prune              (with CAV) Use additional SMT queries to rule out some unrollings." + "\n" +
     "  -P:funcheck:cores              (with CAV) Use UNSAT cores in the unrolling/refinement step." + "\n" +
-    "  -P:funcheck:lucky              (with CAV) Perform additional tests to potentially find models early."
+    "  -P:funcheck:noLuckyTests       (with CAV) Do not perform additional tests to potentially find models early."
   )
 
   /** Processes the command-line options. */
@@ -59,7 +59,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
         case "CAV"       =>                      { purescala.Settings.experimental = true; purescala.Settings.useInstantiator = false; purescala.Settings.useFairInstantiator = true; purescala.Settings.useBAPA = false; purescala.Settings.zeroInlining = true }
         case "prune"     =>                      purescala.Settings.pruneBranches = true
         case "cores"     =>                      purescala.Settings.useCores = true
-        case "lucky"     =>                      purescala.Settings.luckyTest = true
+        case "noLuckyTests" =>                   purescala.Settings.luckyTest = false
         case s if s.startsWith("unrolling=") =>  purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
         case s if s.startsWith("functions=") =>  purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
         case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index a872ad20ed6d9151ea56257f09884102f75da370..555e07958777e28b3bbde93e1900c5b46fe1b79b 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -21,5 +21,5 @@ object Settings {
   var pruneBranches : Boolean = false
   def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
   var solverTimeout : Option[Int] = None
-  var luckyTest : Boolean = false
+  var luckyTest : Boolean = true
 }