diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index 12fd6299e9762222eb0c94f5c18a8b539e23a377..5d2e203f03e81193272da0000c8d6d5e73749313 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -561,6 +561,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
               solver1.assertCnstr(clause)
               solver2.assertCnstr(clause)
+
+              if (clauses.isEmpty) {
+                unfolding = maxUnfoldings
+              }
             }
 
             // Compute all programs that have not been excluded yet
diff --git a/src/main/scala/leon/synthesis/rules/Cegless.scala b/src/main/scala/leon/synthesis/rules/Cegless.scala
index 4d8ebb86c6ceeab9226936755c5e64c00fdaa8ba..d5fbb2619376d24fd995865ce2851448dc3b7758 100644
--- a/src/main/scala/leon/synthesis/rules/Cegless.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegless.scala
@@ -13,7 +13,7 @@ import utils._
 import utils.ExpressionGrammars._
 
 case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
-  override val maxUnfoldings = 3;
+  override val maxUnfoldings = 1000;
 
   def getGrammar(sctx: SynthesisContext, p: Problem) = {