diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 9623624af94dc495cbe1edc335ba4cde5fca0197..efaca2093929c7122b8bc6b2aebd432cbe4fec2e 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -28,6 +28,7 @@ object Rules {
     TEGIS,
     GuidedDecomp,
     GuidedCloser,
+    CEGLESS,
     rules.Assert,
     DetupleOutput,
     DetupleInput,
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 98ca2a4b21ac6b13ef0c867f66d22fd9dfee7e66..33b583d394816ccc3a871c4e0f2ca41d48240075 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -33,10 +33,33 @@ case object CEGIS extends CEGISLike("CEGIS") {
   }
 }
 
+case object CEGLESS extends CEGISLike("CEGLESS") {
+  override val maxUnrolings = 2;
+
+  def getGrammar(sctx: SynthesisContext, p: Problem) = {
+    import ExpressionGrammars._
+
+    val TopLevelAnds(clauses) = p.pc
+
+    val guide = sctx.program.library.guide.get
+
+    val guides = clauses.collect {
+      case FunctionInvocation(TypedFunDef(`guide`, _), Seq(expr)) => expr
+    }
+
+    val guidedGrammar = guides.map(SimilarTo(_)).foldLeft[ExpressionGrammar](Empty)(_ || _)
+
+    guidedGrammar || OneOf(p.as.map(_.toVariable))
+  }
+}
+
 
 abstract class CEGISLike(name: String) extends Rule(name) {
+
   def getGrammar(sctx: SynthesisContext, p: Problem): ExpressionGrammar
 
+  val maxUnrolings = 3
+
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
 
     // CEGIS Flags to actiave or de-activate features
@@ -395,7 +418,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
 
         val ndProgram = new NonDeterministicProgram(p, initGuard)
         var unrolings = 1
-        val maxUnrolings = 3
+        val maxUnrolings = CEGISLike.this.maxUnrolings
 
         val exSolverTo  = 2000L
         val cexSolverTo = 2000L
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index be13325bdc41f410c154ea5a18997887e6431be5..3072a6999171bd26c2e536d396d613fbf6569cd8 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -34,7 +34,7 @@ abstract class ExpressionGrammar {
   def computeProductions(t: TypeTree): Seq[Gen]
 
   final def ||(that: ExpressionGrammar): ExpressionGrammar = {
-    ExpressionGrammar.Or(Seq(this, that))
+    ExpressionGrammars.Or(Seq(this, that))
   }
 
   final def printProductions(printer: String => Unit) {
@@ -47,7 +47,8 @@ abstract class ExpressionGrammar {
   }
 }
 
-object ExpressionGrammar {
+object ExpressionGrammars {
+
   case class Or(gs: Seq[ExpressionGrammar]) extends ExpressionGrammar {
     val subGrammars: Seq[ExpressionGrammar] = gs.flatMap {
       case o: Or => o.subGrammars
@@ -57,9 +58,10 @@ object ExpressionGrammar {
     def computeProductions(t: TypeTree): Seq[Gen] =
       subGrammars.flatMap(_.getProductions(t))
   }
-}
 
-object ExpressionGrammars {
+  case object Empty extends ExpressionGrammar {
+    def computeProductions(t: TypeTree): Seq[Gen] = Nil
+  }
 
   case object BaseGrammar extends ExpressionGrammar {
     def computeProductions(t: TypeTree): Seq[Gen] = t match {
@@ -128,23 +130,23 @@ object ExpressionGrammars {
       def rec(e : Expr) : Seq[(TypeTree, Gen)] = {
         val tp = e.getType
         const(e) +: (e match {
-          case t : Terminal =>
+          case _: Terminal | _: Let | _: LetTuple | _: LetDef | _: MatchExpr =>
             Seq()
           case UnaryOperator(sub, builder) => Seq(
             gen( sub.getType, tp, { case Seq(ex) => builder(ex) } )
-          )
+          ) ++ rec(sub)
           case BinaryOperator(sub1, sub2, builder) => Seq(
             gen( sub1.getType, tp, { case Seq(ex) => builder(ex, sub2) } ),
             gen( sub2.getType, tp, { case Seq(ex) => builder(sub1, ex) } )
-          )
+          ) ++ rec(sub1) ++ rec(sub2)
           case NAryOperator(subs, builder) => 
-            for ((sub,index) <- subs.zipWithIndex) yield {
+            (for ((sub,index) <- subs.zipWithIndex) yield {
               gen( sub.getType, tp, { case Seq(ex) => builder(subs updated (index, ex) )} )
-            }
+            }) ++ subs.flatMap(rec)
         })
       }
 
-      collectPreorder(rec)(e).tail // Don't want the expression itself
+      rec(e).tail // Don't want the expression itself
     }
   }
 
diff --git a/src/main/scala/leon/utils/Simplifiers.scala b/src/main/scala/leon/utils/Simplifiers.scala
index 4791d5a07662a10e91f90bc86b0add4b6e2c2fb1..da10dd8f2cfb0743ddc6392f269bfc0708d6135f 100644
--- a/src/main/scala/leon/utils/Simplifiers.scala
+++ b/src/main/scala/leon/utils/Simplifiers.scala
@@ -51,7 +51,6 @@ object Simplifiers {
       simplifyPaths(uninterpretedZ3)(_),
       patternMatchReconstruction _,
       rewriteTuples _,
-      evalGround(ctx, p),
       normalizeExpression _
     )