diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala
index 8fbb7c94df116d76fc68be389af35fcf1fce9fb5..8cf1044ef0dcf3429c8df805dc6a51f18fc17a4d 100644
--- a/src/main/scala/leon/datagen/GrammarDataGen.scala
+++ b/src/main/scala/leon/datagen/GrammarDataGen.scala
@@ -11,12 +11,12 @@ import purescala.Extractors._
 import evaluators._
 import bonsai.enumerators._
 
-import synthesis.utils._
+import grammars._
 
 /** Utility functions to generate values of a given type.
   * In fact, it could be used to generate *terms* of a given type,
   * e.g. by passing trees representing variables for the "bounds". */
-class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar[TypeTree] = ExpressionGrammars.ValueGrammar) extends DataGenerator {
+class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar[TypeTree] = ValueGrammar) extends DataGenerator {
   implicit val ctx = evaluator.context
 
   def generate(tpe: TypeTree): Iterator[Expr] = {
diff --git a/src/main/scala/leon/grammars/BaseGrammar.scala b/src/main/scala/leon/grammars/BaseGrammar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f11f937498051eb47c2c522a0faa2a1499545175
--- /dev/null
+++ b/src/main/scala/leon/grammars/BaseGrammar.scala
@@ -0,0 +1,73 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.Expressions._
+import purescala.Constructors._
+
+case object BaseGrammar extends ExpressionGrammar[TypeTree] {
+  def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
+    case BooleanType =>
+      List(
+        terminal(BooleanLiteral(true)),
+        terminal(BooleanLiteral(false)),
+        nonTerminal(List(BooleanType),              { case Seq(a)    => not(a) }),
+        nonTerminal(List(BooleanType, BooleanType), { case Seq(a, b) => and(a, b) }),
+        nonTerminal(List(BooleanType, BooleanType), { case Seq(a, b) => or(a, b) }),
+        nonTerminal(List(Int32Type,   Int32Type),   { case Seq(a, b) => LessThan(a, b) }),
+        nonTerminal(List(Int32Type,   Int32Type),   { case Seq(a, b) => LessEquals(a, b) }),
+        nonTerminal(List(IntegerType, IntegerType), { case Seq(a, b) => LessThan(a, b) }),
+        nonTerminal(List(IntegerType, IntegerType), { case Seq(a, b) => LessEquals(a, b) })
+      )
+    case Int32Type =>
+      List(
+        terminal(IntLiteral(0)),
+        terminal(IntLiteral(1)),
+        nonTerminal(List(Int32Type, Int32Type), { case Seq(a,b) => plus(a, b) }),
+        nonTerminal(List(Int32Type, Int32Type), { case Seq(a,b) => minus(a, b) }),
+        nonTerminal(List(Int32Type, Int32Type), { case Seq(a,b) => times(a, b) })
+      )
+
+    case IntegerType =>
+      List(
+        terminal(InfiniteIntegerLiteral(0)),
+        terminal(InfiniteIntegerLiteral(1)),
+        nonTerminal(List(IntegerType, IntegerType), { case Seq(a,b) => plus(a, b) }),
+        nonTerminal(List(IntegerType, IntegerType), { case Seq(a,b) => minus(a, b) }),
+        nonTerminal(List(IntegerType, IntegerType), { case Seq(a,b) => times(a, b) })
+      )
+
+    case TupleType(stps) =>
+      List(
+        nonTerminal(stps, { sub => Tuple(sub) })
+      )
+
+    case cct: CaseClassType =>
+      List(
+        nonTerminal(cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
+      )
+
+    case act: AbstractClassType =>
+      act.knownCCDescendants.map { cct =>
+        nonTerminal(cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
+      }
+
+    case st @ SetType(base) =>
+      List(
+        nonTerminal(List(base),   { case elems     => FiniteSet(elems.toSet, base) }),
+        nonTerminal(List(st, st), { case Seq(a, b) => SetUnion(a, b) }),
+        nonTerminal(List(st, st), { case Seq(a, b) => SetIntersection(a, b) }),
+        nonTerminal(List(st, st), { case Seq(a, b) => SetDifference(a, b) })
+      )
+
+    case UnitType =>
+      List(
+        terminal(UnitLiteral())
+      )
+
+    case _ =>
+      Nil
+  }
+}
diff --git a/src/main/scala/leon/grammars/DepthBoundedGrammar.scala b/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..65708427e167de7647ae22a7e3df6abb6f83ede0
--- /dev/null
+++ b/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
@@ -0,0 +1,22 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.Expressions._
+
+case class DepthBoundedGrammar[T](g: ExpressionGrammar[Label[T]], bound: Int) extends ExpressionGrammar[Label[T]] {
+  def computeProductions(l: Label[T])(implicit ctx: LeonContext): Seq[Gen] = g.computeProductions(l).flatMap {
+    case gen =>
+      if (l.depth == Some(bound) && gen.subTrees.nonEmpty) {
+        Nil
+      } else if (l.depth.exists(_ > bound)) {
+        Nil
+      } else {
+        List (
+          nonTerminal(gen.subTrees.map(sl => sl.copy(depth = l.depth.map(_+1).orElse(Some(1)))), gen.builder)
+        )
+      }
+  }
+}
diff --git a/src/main/scala/leon/grammars/EmbeddedGrammar.scala b/src/main/scala/leon/grammars/EmbeddedGrammar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bcee19b0118b896468994acbfe80a497f02012fd
--- /dev/null
+++ b/src/main/scala/leon/grammars/EmbeddedGrammar.scala
@@ -0,0 +1,21 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.Expressions._
+import purescala.Constructors._
+
+/**
+ * Embed a grammar Li->Expr within a grammar Lo->Expr
+ * 
+ * We rely on a bijection between Li and Lo labels
+ */
+case class EmbeddedGrammar[Ti <% Typed, To <% Typed](innerGrammar: ExpressionGrammar[Ti], iToo: Ti => To, oToi: To => Ti) extends ExpressionGrammar[To] {
+  def computeProductions(t: To)(implicit ctx: LeonContext): Seq[Gen] = {
+    innerGrammar.computeProductions(oToi(t)).map { innerGen =>
+      nonTerminal(innerGen.subTrees.map(iToo), innerGen.builder)
+    }
+  }
+}
diff --git a/src/main/scala/leon/grammars/Empty.scala b/src/main/scala/leon/grammars/Empty.scala
new file mode 100644
index 0000000000000000000000000000000000000000..56b332309329acb8017ccbb8bdb9f71711e22eb2
--- /dev/null
+++ b/src/main/scala/leon/grammars/Empty.scala
@@ -0,0 +1,10 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+
+case class Empty[T <% Typed]() extends ExpressionGrammar[T] {
+  def computeProductions(t: T)(implicit ctx: LeonContext): Seq[Gen] = Nil
+}
diff --git a/src/main/scala/leon/grammars/EqualityGrammar.scala b/src/main/scala/leon/grammars/EqualityGrammar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e9463a771204d877a4d748c373b6d198e2c2591b
--- /dev/null
+++ b/src/main/scala/leon/grammars/EqualityGrammar.scala
@@ -0,0 +1,20 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.Constructors._
+
+import bonsai._
+
+case class EqualityGrammar(types: Set[TypeTree]) extends ExpressionGrammar[TypeTree] {
+  override def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
+    case BooleanType =>
+      types.toList map { tp =>
+        nonTerminal(List(tp, tp), { case Seq(a, b) => equality(a, b) })
+      }
+
+    case _ => Nil
+  }
+}
diff --git a/src/main/scala/leon/grammars/ExpressionGrammar.scala b/src/main/scala/leon/grammars/ExpressionGrammar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..465904f5db3b4e7289f8ce0b8a13aa86798bf72e
--- /dev/null
+++ b/src/main/scala/leon/grammars/ExpressionGrammar.scala
@@ -0,0 +1,59 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import bonsai._
+
+import purescala.Expressions._
+import purescala.Types._
+import purescala.Common._
+
+import scala.collection.mutable.{HashMap => MutableMap}
+
+abstract class ExpressionGrammar[T <% Typed] {
+  type Gen = Generator[T, Expr]
+
+  private[this] val cache = new MutableMap[T, Seq[Gen]]()
+
+  def terminal(builder: => Expr) = {
+    Generator[T, Expr](Nil, { (subs: Seq[Expr]) => builder })
+  }
+
+  def nonTerminal(subs: Seq[T], builder: (Seq[Expr] => Expr)): Generator[T, Expr] = {
+    Generator[T, Expr](subs, builder)
+  }
+
+  def getProductions(t: T)(implicit ctx: LeonContext): Seq[Gen] = {
+    cache.getOrElse(t, {
+      val res = computeProductions(t)
+      cache += t -> res
+      res
+    })
+  }
+
+  def computeProductions(t: T)(implicit ctx: LeonContext): Seq[Gen]
+
+  def filter(f: Gen => Boolean) = {
+    new ExpressionGrammar[T] {
+      def computeProductions(t: T)(implicit ctx: LeonContext) = ExpressionGrammar.this.computeProductions(t).filter(f)
+    }
+  }
+
+  final def ||(that: ExpressionGrammar[T]): ExpressionGrammar[T] = {
+    Union(Seq(this, that))
+  }
+
+
+  final def printProductions(printer: String => Unit)(implicit ctx: LeonContext) {
+    for ((t, gs) <- cache; g <- gs) {
+      val subs = g.subTrees.map { t =>
+        FreshIdentifier(Console.BOLD+t.asString+Console.RESET, t.getType).toVariable
+      }
+
+      val gen = g.builder(subs).asString
+
+      printer(f"${Console.BOLD}${t.asString}%30s${Console.RESET} ::= $gen")
+    }
+  }
+}
diff --git a/src/main/scala/leon/grammars/FunctionCalls.scala b/src/main/scala/leon/grammars/FunctionCalls.scala
new file mode 100644
index 0000000000000000000000000000000000000000..14f92393934c18804bdb130e9c1617b915a347bd
--- /dev/null
+++ b/src/main/scala/leon/grammars/FunctionCalls.scala
@@ -0,0 +1,79 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.TypeOps._
+import purescala.Definitions._
+import purescala.ExprOps._
+import purescala.DefOps._
+import purescala.Expressions._
+
+case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[TypeTree], exclude: Set[FunDef]) extends ExpressionGrammar[TypeTree] {
+   def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = {
+
+     def getCandidates(fd: FunDef): Seq[TypedFunDef] = {
+       // Prevents recursive calls
+       val cfd = currentFunction
+
+       val isRecursiveCall = (prog.callGraph.transitiveCallers(cfd) + cfd) contains fd
+
+       val isDet = fd.body.exists(isDeterministic)
+
+       if (!isRecursiveCall && isDet) {
+         val free = fd.tparams.map(_.tp)
+
+         canBeSubtypeOf(fd.returnType, free, t, rhsFixed = true) match {
+           case Some(tpsMap) =>
+             val tfd = fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp)))
+
+             if (tpsMap.size < free.size) {
+               /* Some type params remain free, we want to assign them:
+                *
+                * List[T] => Int, for instance, will be found when
+                * requesting Int, but we need to assign T to viable
+                * types. For that we use list of input types as heuristic,
+                * and look for instantiations of T such that input <?:
+                * List[T].
+                */
+               types.distinct.flatMap { (atpe: TypeTree) =>
+                 var finalFree = free.toSet -- tpsMap.keySet
+                 var finalMap = tpsMap
+
+                 for (ptpe <- tfd.params.map(_.getType).distinct) {
+                   canBeSubtypeOf(atpe, finalFree.toSeq, ptpe) match {
+                     case Some(ntpsMap) =>
+                       finalFree --= ntpsMap.keySet
+                       finalMap  ++= ntpsMap
+                     case _ =>
+                   }
+                 }
+
+                 if (finalFree.isEmpty) {
+                   List(fd.typed(free.map(tp => finalMap.getOrElse(tp, tp))))
+                 } else {
+                   Nil
+                 }
+               }
+             } else {
+               /* All type parameters that used to be free are assigned
+                */
+               List(tfd)
+             }
+           case None =>
+             Nil
+         }
+       } else {
+         Nil
+       }
+     }
+
+     val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || (exclude contains tfd.fd)
+     val funcs = visibleFunDefsFromMain(prog).toSeq.sortBy(_.id).flatMap(getCandidates).filterNot(filter)
+
+     funcs.map{ tfd =>
+       nonTerminal(tfd.params.map(_.getType), { sub => FunctionInvocation(tfd, sub) })
+     }
+   }
+  }
diff --git a/src/main/scala/leon/grammars/Grammars.scala b/src/main/scala/leon/grammars/Grammars.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2194aa539afe94dc06182b5acaf12bb669de0612
--- /dev/null
+++ b/src/main/scala/leon/grammars/Grammars.scala
@@ -0,0 +1,30 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Expressions._
+import purescala.Definitions._
+import purescala.Types._
+import purescala.TypeOps._
+
+import synthesis.{SynthesisContext, Problem}
+
+object Grammars {
+
+  def default(prog: Program, inputs: Seq[Expr], currentFunction: FunDef, exclude: Set[FunDef], ws: Expr, pc: Expr): ExpressionGrammar[TypeTree] = {
+    BaseGrammar ||
+    EqualityGrammar(Set(IntegerType, Int32Type, BooleanType) ++ inputs.map { _.getType }) ||
+    OneOf(inputs) ||
+    FunctionCalls(prog, currentFunction, inputs.map(_.getType), exclude) ||
+    SafeRecursiveCalls(prog, ws, pc)
+  }
+
+  def default(sctx: SynthesisContext, p: Problem): ExpressionGrammar[TypeTree] = {
+    default(sctx.program, p.as.map(_.toVariable), sctx.functionContext, sctx.settings.functionsToIgnore,  p.ws, p.pc)
+  }
+
+  def typeDepthBound[T <% Typed](g: ExpressionGrammar[T], b: Int) = {
+    g.filter(g => g.subTrees.forall(t => typeDepth(t.getType) <= b))
+  }
+}
diff --git a/src/main/scala/leon/grammars/Label.scala b/src/main/scala/leon/grammars/Label.scala
new file mode 100644
index 0000000000000000000000000000000000000000..456f184e7edb0e2f28eb9cb5b8830b77bf336aac
--- /dev/null
+++ b/src/main/scala/leon/grammars/Label.scala
@@ -0,0 +1,10 @@
+package leon
+package grammars
+
+import purescala.Types._
+
+case class Label[T](t: TypeTree, l: T, depth: Option[Int] = None) extends Typed {
+  val getType = t
+
+  override def asString(implicit ctx: LeonContext) = t.asString+"#"+l+depth.map(d => "@"+d).getOrElse("")
+}
diff --git a/src/main/scala/leon/grammars/OneOf.scala b/src/main/scala/leon/grammars/OneOf.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0e10c096151c1fdf83d3c7e7f10c4a4a6518215b
--- /dev/null
+++ b/src/main/scala/leon/grammars/OneOf.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.Expressions._
+import purescala.TypeOps._
+import purescala.Constructors._
+
+case class OneOf(inputs: Seq[Expr]) extends ExpressionGrammar[TypeTree] {
+  def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = {
+    inputs.collect {
+      case i if isSubtypeOf(i.getType, t) =>
+        terminal(i)
+    }
+  }
+}
diff --git a/src/main/scala/leon/grammars/Or.scala b/src/main/scala/leon/grammars/Or.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ae0bc96976f1a4d2d349a72060e391686b4cab52
--- /dev/null
+++ b/src/main/scala/leon/grammars/Or.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+
+case class Union[T <% Typed](gs: Seq[ExpressionGrammar[T]]) extends ExpressionGrammar[T] {
+  val subGrammars: Seq[ExpressionGrammar[T]] = gs.flatMap {
+    case u: Union[T] => u.subGrammars
+    case g => Seq(g)
+  }
+
+  def computeProductions(t: T)(implicit ctx: LeonContext): Seq[Gen] =
+    subGrammars.flatMap(_.getProductions(t))
+}
diff --git a/src/main/scala/leon/grammars/SafeRecursiveCalls.scala b/src/main/scala/leon/grammars/SafeRecursiveCalls.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1bbcb0523158ac95713f5a0d4a16f0f35e14edf4
--- /dev/null
+++ b/src/main/scala/leon/grammars/SafeRecursiveCalls.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.Definitions._
+import purescala.ExprOps._
+import purescala.Expressions._
+import synthesis.utils.Helpers._
+
+case class SafeRecursiveCalls(prog: Program, ws: Expr, pc: Expr) extends ExpressionGrammar[TypeTree] {
+  def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = {
+    val calls = terminatingCalls(prog, t, ws, pc)
+
+    calls.map {
+      case (e, free) =>
+        val freeSeq = free.toSeq
+
+        nonTerminal(freeSeq.map(_.getType), { sub => replaceFromIDs(freeSeq.zip(sub).toMap, e) })
+    }
+  }
+}
diff --git a/src/main/scala/leon/grammars/SimilarTo.scala b/src/main/scala/leon/grammars/SimilarTo.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c134546d2af88039d2ef5f9a9a030e331ae80161
--- /dev/null
+++ b/src/main/scala/leon/grammars/SimilarTo.scala
@@ -0,0 +1,174 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.TypeOps._
+import purescala.Extractors._
+import purescala.Definitions._
+import purescala.ExprOps._
+import purescala.DefOps._
+import purescala.Expressions._
+
+import synthesis._
+
+case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[Label[String]] {
+
+  val excludeFCalls = sctx.settings.functionsToIgnore
+
+  val normalGrammar = DepthBoundedGrammar(EmbeddedGrammar(
+      BaseGrammar ||
+      EqualityGrammar(Set(IntegerType, Int32Type, BooleanType) ++ terminals.map { _.getType }) ||
+      OneOf(terminals.toSeq :+ e) ||
+      FunctionCalls(sctx.program, sctx.functionContext, p.as.map(_.getType), excludeFCalls) ||
+      SafeRecursiveCalls(sctx.program, p.ws, p.pc),
+    { (t: TypeTree)      => Label(t, "B", None)},
+    { (l: Label[String]) => l.getType }
+  ), 1)
+
+  type L = Label[String]
+
+  val getNext: () => Int = {
+    var counter = -1
+    () => {
+      counter += 1
+      counter
+    }
+  }
+
+  private[this] var similarCache: Option[Map[L, Seq[Gen]]] = None
+
+  def computeProductions(t: L)(implicit ctx: LeonContext): Seq[Gen] = {
+    t match {
+      case Label(_, "B", _) => normalGrammar.computeProductions(t)
+      case _                =>
+
+        val allSimilar = similarCache.getOrElse {
+          val res = computeSimilar(e).groupBy(_._1).mapValues(_.map(_._2))
+          similarCache = Some(res)
+          res
+        }
+
+        allSimilar.getOrElse(t, Nil)
+    }
+  }
+
+  def computeSimilar(e : Expr)(implicit ctx: LeonContext): Seq[(L, Gen)] = {
+
+    def getLabel(t: TypeTree) = {
+      val tpe = bestRealType(t)
+      val c = getNext()
+      Label(tpe, "G"+c)
+    }
+
+    def isCommutative(e: Expr) = e match {
+      case _: Plus | _: Times => true
+      case _ => false
+    }
+
+    def rec(e: Expr, gl: L): Seq[(L, Gen)] = {
+
+      def gens(e: Expr, gl: L, subs: Seq[Expr], builder: (Seq[Expr] => Expr)): Seq[(L, Gen)] = {
+        val subGls = subs.map { s => getLabel(s.getType) }
+
+        // All the subproductions for sub gl
+        val allSubs = (subs zip subGls).flatMap { case (e, gl) => rec(e, gl) }
+
+        // Inject fix at one place
+        val injectG = for ((sgl, i) <- subGls.zipWithIndex) yield {
+          gl -> nonTerminal(Seq(sgl), { case Seq(ge) => builder(subs.updated(i, ge)) } )
+        }
+
+        val swaps = if (subs.size > 1 && !isCommutative(e)) {
+          (for (i <- 0 until subs.size;
+               j <- i+1 until subs.size) yield {
+
+            if (subs(i).getType == subs(j).getType) {
+              val swapSubs = subs.updated(i, subs(j)).updated(j, subs(i))
+              Some(gl -> terminal(builder(swapSubs)))
+            } else {
+              None
+            }
+          }).flatten
+        } else {
+          Nil
+        }
+
+        allSubs ++ injectG ++ swaps
+      }
+
+      def cegis(gl: L): Seq[(L, Gen)] = {
+        normalGrammar.getProductions(gl).map(gl -> _)
+      }
+
+      def int32Variations(gl: L, e : Expr): Seq[(L, Gen)] = {
+        Seq(
+          gl -> terminal(BVMinus(e, IntLiteral(1))),
+          gl -> terminal(BVPlus (e, IntLiteral(1)))
+        )
+      }
+
+      def intVariations(gl: L, e : Expr): Seq[(L, Gen)] = {
+        Seq(
+          gl -> terminal(Minus(e, InfiniteIntegerLiteral(1))),
+          gl -> terminal(Plus (e, InfiniteIntegerLiteral(1)))
+        )
+      }
+
+      // Find neighbor case classes that are compatible with the arguments:
+      // Turns And(e1, e2) into Or(e1, e2)...
+      def ccVariations(gl: L, cc: CaseClass): Seq[(L, Gen)] = {
+        val CaseClass(cct, args) = cc
+
+        val neighbors = cct.root.knownCCDescendants diff Seq(cct)
+
+        for (scct <- neighbors if scct.fieldsTypes == cct.fieldsTypes) yield {
+          gl -> terminal(CaseClass(scct, args))
+        }
+      }
+
+      val funFilter = (fd: FunDef) => fd.isSynthetic || (excludeFCalls contains fd)
+      val subs: Seq[(L, Gen)] = e match {
+        
+        case _: Terminal | _: Let | _: LetDef | _: MatchExpr =>
+          gens(e, gl, Nil, { _ => e }) ++ cegis(gl)
+
+        case cc @ CaseClass(cct, exprs) =>
+          gens(e, gl, exprs, { case ss => CaseClass(cct, ss) }) ++ ccVariations(gl, cc)
+
+        case FunctionInvocation(TypedFunDef(fd, _), _) if funFilter(fd) =>
+          // We allow only exact call, and/or cegis extensions
+          /*Seq(el -> Generator[L, Expr](Nil, { _ => e })) ++*/ cegis(gl)
+
+        case Operator(subs, builder) =>
+          gens(e, gl, subs, { case ss => builder(ss) })
+      }
+
+      val terminalsMatching = terminals.collect {
+        case IsTyped(term, tpe) if tpe == gl.getType && term != e =>
+          gl -> terminal(term)
+      }
+
+      val variations = e.getType match {
+        case IntegerType => intVariations(gl, e)
+        case Int32Type => int32Variations(gl, e)
+        case _ => Nil
+      }
+
+      subs ++ terminalsMatching ++ variations
+    }
+
+    val gl = getLabel(e.getType)
+
+    val res = rec(e, gl)
+
+    //for ((t, g) <- res) {
+    //  val subs = g.subTrees.map { t => FreshIdentifier(t.asString, t.getType).toVariable}
+    //  val gen = g.builder(subs)
+
+    //  println(f"$t%30s ::= "+gen)
+    //}
+    res
+  }
+}
diff --git a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..697120356afceac724ee6cf7257f96756cff3f60
--- /dev/null
+++ b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
@@ -0,0 +1,38 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.Expressions._
+import purescala.TypeOps._
+
+import leon.utils.SeqUtils.sumTo
+
+case class SizedLabel[T <% Typed](underlying: T, size: Int) extends Typed {
+  val getType = underlying.getType
+
+  override def asString(implicit ctx: LeonContext) = underlying.asString+"|"+size+"|"
+}
+
+case class SizeBoundedGrammar[T <% Typed](g: ExpressionGrammar[T]) extends ExpressionGrammar[SizedLabel[T]] {
+  def computeProductions(sl: SizedLabel[T])(implicit ctx: LeonContext): Seq[Gen] = {
+    if (sl.size <= 0) {
+      Nil
+    } else if (sl.size == 1) {
+      g.getProductions(sl.underlying).filter(_.subTrees.isEmpty).map { gen =>
+        terminal(gen.builder(Seq()))
+      }
+    } else {
+      g.getProductions(sl.underlying).filter(_.subTrees.nonEmpty).flatMap { gen =>
+        val sizes = sumTo(sl.size-1, gen.subTrees.size)
+
+        for (ss <- sizes) yield {
+          val subSizedLabels = (gen.subTrees zip ss) map (s => SizedLabel(s._1, s._2))
+
+          nonTerminal(subSizedLabels, gen.builder)
+        }
+      }
+    }
+  }
+}
diff --git a/src/main/scala/leon/grammars/ValueGrammar.scala b/src/main/scala/leon/grammars/ValueGrammar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2b7bb140b63b110a60d1d97c104329db2dd61eb8
--- /dev/null
+++ b/src/main/scala/leon/grammars/ValueGrammar.scala
@@ -0,0 +1,65 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package grammars
+
+import purescala.Types._
+import purescala.Expressions._
+import purescala.Constructors._
+
+
+case object ValueGrammar extends ExpressionGrammar[TypeTree] {
+  def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
+    case BooleanType =>
+      List(
+        terminal(BooleanLiteral(true)),
+        terminal(BooleanLiteral(false))
+      )
+    case Int32Type =>
+      List(
+        terminal(IntLiteral(0)),
+        terminal(IntLiteral(1)),
+        terminal(IntLiteral(5))
+      )
+    case IntegerType =>
+      List(
+        terminal(InfiniteIntegerLiteral(0)),
+        terminal(InfiniteIntegerLiteral(1)),
+        terminal(InfiniteIntegerLiteral(5))
+      )
+
+    case tp: TypeParameter =>
+      for (ind <- (1 to 3).toList) yield {
+        terminal(GenericValue(tp, ind))
+      }
+
+    case TupleType(stps) =>
+      List(
+        nonTerminal(stps, { sub => Tuple(sub) })
+      )
+
+    case cct: CaseClassType =>
+      List(
+        nonTerminal(cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)})
+      )
+
+    case act: AbstractClassType =>
+      act.knownCCDescendants.map { cct =>
+        nonTerminal(cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)})
+      }
+
+    case st @ SetType(base) =>
+      List(
+        nonTerminal(List(base),       { case elems => FiniteSet(elems.toSet, base) }),
+        nonTerminal(List(base, base), { case elems => FiniteSet(elems.toSet, base) })
+      )
+    
+    case UnitType =>
+      List(
+        terminal(UnitLiteral())
+      )
+
+    case _ =>
+      Nil
+  }
+}
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index fd928deb1b640c1d0e785951ebb07f258dd2479a..c41ae4a01efe2b3d491c556b7e4838bada6cc141 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -14,7 +14,6 @@ import purescala.Extractors.unwrapTuple
 import purescala.ScalaPrinter
 import evaluators._
 import solvers._
-import solvers.z3._
 import utils._
 import codegen._
 import verification._
@@ -24,6 +23,7 @@ import synthesis.Witnesses._
 import rules._
 import graph.DotGenerator
 import leon.utils.ASCIIHelpers.title
+import grammars._
 
 import scala.concurrent.duration._
 
@@ -190,7 +190,6 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
   def discoverTests(): ExamplesBank = {
 
     import bonsai.enumerators._
-    import utils.ExpressionGrammars.ValueGrammar
 
     val maxEnumerated = 1000
     val maxValid      = 400
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 5de332b6fd325fac33eedc652743702bb860ddb9..7877e9a34dbcee152f2a439665fa3d3697e64cff 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -11,7 +11,7 @@ import purescala.Common._
 import purescala.Constructors._
 import purescala.Extractors._
 import evaluators._
-import utils.ExpressionGrammars.ValueGrammar
+import grammars._
 import bonsai.enumerators._
 import codegen._
 
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index dd06ad051630e91c764e784a1d8f060b596eccd4..c363bcfa5f738543cd9f6ee7fc4572cf4a69623d 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -12,13 +12,14 @@ import evaluators._
 import codegen.CodeGenParams
 
 import utils._
+import grammars._
 
 import bonsai._
 import bonsai.enumerators._
 
 case object BottomUpTEGIS extends BottomUpTEGISLike[TypeTree]("BU TEGIS") {
   def getGrammar(sctx: SynthesisContext, p: Problem) = {
-    ExpressionGrammars.default(sctx, p)
+    Grammars.default(sctx, p)
   }
 
   def getRootLabel(tpe: TypeTree): TypeTree = tpe
diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala
index 038e9842789c6a0e501451dc5f1bc89ca078db13..1fcf01d52088ea9d4d25d184a673ef8335a8d260 100644
--- a/src/main/scala/leon/synthesis/rules/CEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGIS.scala
@@ -6,13 +6,13 @@ package rules
 
 import purescala.Types._
 
+import grammars._
 import utils._
 
 case object CEGIS extends CEGISLike[TypeTree]("CEGIS") {
   def getParams(sctx: SynthesisContext, p: Problem) = {
-    import ExpressionGrammars._
     CegisParams(
-      grammar = depthBound(default(sctx, p), 2), // This limits type depth
+      grammar = Grammars.typeDepthBound(Grammars.default(sctx, p), 2), // This limits type depth
       rootLabel = {(tpe: TypeTree) => tpe }
     )
   }
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 4f4aec2a599ca885100eb9b396d8adf9d9dddaa8..4a377acd239ace5c6180625a36563584ec88a584 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -6,6 +6,7 @@ package rules
 
 import leon.utils.SeqUtils
 import solvers._
+import grammars._
 
 import purescala.Expressions._
 import purescala.Common._
@@ -22,8 +23,6 @@ import datagen._
 import codegen.CodeGenParams
 
 import utils._
-import utils.ExpressionGrammars.{SizeBoundedGrammar, SizedLabel}
-import bonsai.Generator
 
 abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
@@ -79,8 +78,8 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
       def countAlternatives(l: SizedLabel[T]): Int = {
         if (!(nAltsCache contains l)) {
-          val count = grammar.getProductions(l).map {
-            case Generator(subTrees, _) => subTrees.map(countAlternatives).product
+          val count = grammar.getProductions(l).map { gen =>
+            gen.subTrees.map(countAlternatives).product
           }.sum
           nAltsCache += l -> count
         }
@@ -705,7 +704,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
           new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, nTests, 3000)
         } else {
           val evaluator = new DualEvaluator(sctx.context, sctx.program, CodeGenParams.default)
-          new GrammarDataGen(evaluator, ExpressionGrammars.ValueGrammar).generateFor(p.as, p.pc, nTests, 1000)
+          new GrammarDataGen(evaluator, ValueGrammar).generateFor(p.as, p.pc, nTests, 1000)
         }
 
         val cachedInputIterator = new Iterator[Example] {
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index c19a4203ea21207fc34e6d7a073610d36c375968..6b0bbdd15e257841026da4f64cf8e0857f8ed1c7 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -8,7 +8,7 @@ import purescala.ExprOps._
 import purescala.Types._
 import purescala.Extractors._
 import utils._
-import utils.ExpressionGrammars._
+import grammars._
 import Witnesses._
 
 case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
diff --git a/src/main/scala/leon/synthesis/rules/TEGIS.scala b/src/main/scala/leon/synthesis/rules/TEGIS.scala
index ad534efe7a1726917192760b9f3c846d352ae518..d7ec34617ee7dc50745c3b6839511e2c00a6037e 100644
--- a/src/main/scala/leon/synthesis/rules/TEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGIS.scala
@@ -5,12 +5,13 @@ package synthesis
 package rules
 
 import purescala.Types._
+import grammars._
 import utils._
 
 case object TEGIS extends TEGISLike[TypeTree]("TEGIS") {
   def getParams(sctx: SynthesisContext, p: Problem) = {
     TegisParams(
-      grammar = ExpressionGrammars.default(sctx, p),
+      grammar = Grammars.default(sctx, p),
       rootLabel = {(tpe: TypeTree) => tpe }
     )
   }
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 29fc0bcb9a1c7a5972a50981af05e776c08c3787..2fe03e7af328656495e19f2a816197b601873325 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -13,6 +13,8 @@ import codegen.CodeGenParams
 
 import utils._
 
+import grammars._
+
 import bonsai.enumerators._
 
 abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
diff --git a/src/main/scala/leon/synthesis/rules/TEGLESS.scala b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
index 72751001195a794dc520e65605c47c7aebf8d8c2..d8de10cbb952b764916386f9accdca98129f2c71 100644
--- a/src/main/scala/leon/synthesis/rules/TEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
@@ -7,8 +7,8 @@ package rules
 import purescala.Types._
 import purescala.Extractors._
 import utils._
-import utils.ExpressionGrammars._
 import Witnesses._
+import grammars._
 
 case object TEGLESS extends TEGISLike[Label[String]]("TEGLESS") {
   def getParams(sctx: SynthesisContext, p: Problem) = {
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
deleted file mode 100644
index bcd5dfb03052d89eced8905ac31f3352a39c3c2a..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ /dev/null
@@ -1,524 +0,0 @@
-/* Copyright 2009-2015 EPFL, Lausanne */
-
-package leon
-package synthesis
-package utils
-
-import bonsai._
-
-import Helpers._
-
-import leon.utils.SeqUtils.sumTo
-
-import purescala.Expressions.{Or => LeonOr, _}
-import purescala.Common._
-import purescala.Definitions._
-import purescala.Types._
-import purescala.ExprOps._
-import purescala.TypeOps._
-import purescala.Extractors._
-import purescala.Constructors._
-import purescala.ScalaPrinter
-
-import scala.language.implicitConversions
-
-import scala.collection.mutable.{HashMap => MutableMap}
-
-abstract class ExpressionGrammar[T <% Typed] {
-  type Gen = Generator[T, Expr]
-
-  private[this] val cache = new MutableMap[T, Seq[Gen]]()
-
-  def getProductions(t: T)(implicit ctx: LeonContext): Seq[Gen] = {
-    cache.getOrElse(t, {
-      val res = computeProductions(t)
-      cache += t -> res
-      res
-    })
-  }
-
-  def computeProductions(t: T)(implicit ctx: LeonContext): Seq[Gen]
-
-  def filter(f: Gen => Boolean) = {
-    new ExpressionGrammar[T] {
-      def computeProductions(t: T)(implicit ctx: LeonContext) = ExpressionGrammar.this.computeProductions(t).filter(f)
-    }
-  }
-
-  final def ||(that: ExpressionGrammar[T]): ExpressionGrammar[T] = {
-    ExpressionGrammars.Or(Seq(this, that))
-  }
-
-
-  final def printProductions(printer: String => Unit)(implicit ctx: LeonContext) {
-    for ((t, gs) <- cache; g <- gs) {
-      val subs = g.subTrees.map { t => FreshIdentifier(Console.BOLD+t.asString+Console.RESET, t.getType).toVariable}
-      val gen = g.builder(subs).asString
-
-      printer(f"${Console.BOLD}${t.asString}%30s${Console.RESET} ::= $gen")
-    }
-  }
-}
-
-object ExpressionGrammars {
-
-  case class Or[T <% Typed](gs: Seq[ExpressionGrammar[T]]) extends ExpressionGrammar[T] {
-    val subGrammars: Seq[ExpressionGrammar[T]] = gs.flatMap {
-      case o: Or[T] => o.subGrammars
-      case g => Seq(g)
-    }
-
-    def computeProductions(t: T)(implicit ctx: LeonContext): Seq[Gen] =
-      subGrammars.flatMap(_.getProductions(t))
-  }
-
-  case class Empty[T <% Typed]() extends ExpressionGrammar[T] {
-    def computeProductions(t: T)(implicit ctx: LeonContext): Seq[Gen] = Nil
-  }
-
-  case object BaseGrammar extends ExpressionGrammar[TypeTree] {
-    def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
-      case BooleanType =>
-        List(
-          Generator(Nil, { _ => BooleanLiteral(true) }),
-          Generator(Nil, { _ => BooleanLiteral(false) }),
-          Generator(List(BooleanType),              { case Seq(a)    => not(a) }),
-          Generator(List(BooleanType, BooleanType), { case Seq(a, b) => and(a, b) }),
-          Generator(List(BooleanType, BooleanType), { case Seq(a, b) => or(a, b) }),
-          Generator(List(Int32Type,   Int32Type),   { case Seq(a, b) => LessThan(a, b) }),
-          Generator(List(Int32Type,   Int32Type),   { case Seq(a, b) => LessEquals(a, b) }),
-          Generator(List(IntegerType, IntegerType), { case Seq(a, b) => LessThan(a, b) }),
-          Generator(List(IntegerType, IntegerType), { case Seq(a, b) => LessEquals(a, b) })
-        )
-      case Int32Type =>
-        List(
-          Generator(Nil, { _ => IntLiteral(0) }),
-          Generator(Nil, { _ => IntLiteral(1) }),
-          Generator(List(Int32Type, Int32Type), { case Seq(a,b) => plus(a, b) }),
-          Generator(List(Int32Type, Int32Type), { case Seq(a,b) => minus(a, b) }),
-          Generator(List(Int32Type, Int32Type), { case Seq(a,b) => times(a, b) })
-        )
-
-      case IntegerType =>
-        List(
-          Generator(Nil, { _ => InfiniteIntegerLiteral(0) }),
-          Generator(Nil, { _ => InfiniteIntegerLiteral(1) }),
-          Generator(List(IntegerType, IntegerType), { case Seq(a,b) => plus(a, b) }),
-          Generator(List(IntegerType, IntegerType), { case Seq(a,b) => minus(a, b) }),
-          Generator(List(IntegerType, IntegerType), { case Seq(a,b) => times(a, b) })
-        )
-
-      case TupleType(stps) =>
-        List(Generator(stps, { sub => Tuple(sub) }))
-
-      case cct: CaseClassType =>
-        List(
-          Generator(cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
-        )
-
-      case act: AbstractClassType =>
-        act.knownCCDescendants.map { cct =>
-          Generator[TypeTree, Expr](cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
-        }
-
-      case st @ SetType(base) =>
-        List(
-          Generator(List(base),   { case elems     => FiniteSet(elems.toSet, base) }),
-          Generator(List(st, st), { case Seq(a, b) => SetUnion(a, b) }),
-          Generator(List(st, st), { case Seq(a, b) => SetIntersection(a, b) }),
-          Generator(List(st, st), { case Seq(a, b) => SetDifference(a, b) })
-        )
-
-      case UnitType =>
-        List( Generator(Nil, { case _ => UnitLiteral() }) )
-
-      case _ =>
-        Nil
-    }
-  }
-
-  case class EqualityGrammar(types: Set[TypeTree]) extends ExpressionGrammar[TypeTree] {
-    override def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
-      case BooleanType =>
-        types.toList map { tp =>
-          Generator[TypeTree, Expr](List(tp, tp), { case Seq(a, b) => equality(a, b) })
-        }
-
-      case _ => Nil
-    }
-  }
-
-  case object ValueGrammar extends ExpressionGrammar[TypeTree] {
-    def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = t match {
-      case BooleanType =>
-        List(
-          Generator(Nil, { _ => BooleanLiteral(true) }),
-          Generator(Nil, { _ => BooleanLiteral(false) })
-        )
-      case Int32Type =>
-        List(
-          Generator(Nil, { _ => IntLiteral(0) }),
-          Generator(Nil, { _ => IntLiteral(1) }),
-          Generator(Nil, { _ => IntLiteral(5) })
-        )
-      case IntegerType =>
-        List(
-          Generator(Nil, { _ => InfiniteIntegerLiteral(0) }),
-          Generator(Nil, { _ => InfiniteIntegerLiteral(1) }),
-          Generator(Nil, { _ => InfiniteIntegerLiteral(5) })
-        )
-
-      case tp@TypeParameter(_) =>
-        for (ind <- (1 to 3).toList) yield
-          Generator[TypeTree, Expr](Nil, { _ => GenericValue(tp, ind) } )
-
-      case TupleType(stps) =>
-        List(Generator(stps, { sub => Tuple(sub) }))
-
-      case cct: CaseClassType =>
-        List(
-          Generator(cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
-        )
-
-      case act: AbstractClassType =>
-        act.knownCCDescendants.map { cct =>
-          Generator[TypeTree, Expr](cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
-        }
-
-      case st @ SetType(base) =>
-        List(
-          Generator(List(base),       { case elems => FiniteSet(elems.toSet, base) }),
-          Generator(List(base, base), { case elems => FiniteSet(elems.toSet, base) })
-        )
-      
-      case UnitType =>
-        List( Generator(Nil, { case _ => UnitLiteral() }) )
-
-      case _ =>
-        Nil
-    }
-  }
-
-  case class OneOf(inputs: Seq[Expr]) extends ExpressionGrammar[TypeTree] {
-    def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = {
-      inputs.collect {
-        case i if isSubtypeOf(i.getType, t) => Generator[TypeTree, Expr](Nil, { _ => i })
-      }
-    }
-  }
-
-  case class Label[T](t: TypeTree, l: T, depth: Option[Int] = None) extends Typed {
-    val getType = t
-
-    override def asString(implicit ctx: LeonContext) = t.asString+"#"+l+depth.map(d => "@"+d).getOrElse("")
-  }
-
-  case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[Label[String]] {
-
-    val excludeFCalls = sctx.settings.functionsToIgnore
-
-    val normalGrammar = BoundedGrammar(EmbeddedGrammar(
-        BaseGrammar ||
-        EqualityGrammar(Set(IntegerType, Int32Type, BooleanType) ++ terminals.map { _.getType }) ||
-        OneOf(terminals.toSeq :+ e) ||
-        FunctionCalls(sctx.program, sctx.functionContext, p.as.map(_.getType), excludeFCalls) ||
-        SafeRecCalls(sctx.program, p.ws, p.pc),
-      { (t: TypeTree)      => Label(t, "B", None)},
-      { (l: Label[String]) => l.getType }
-    ), 1)
-
-    type L = Label[String]
-
-    val getNext: () => Int = {
-      var counter = -1
-      () => {
-        counter += 1
-        counter
-      }
-    }
-
-    private[this] var similarCache: Option[Map[L, Seq[Gen]]] = None
-
-    def computeProductions(t: L)(implicit ctx: LeonContext): Seq[Gen] = {
-      t match {
-        case Label(_, "B", _) => normalGrammar.computeProductions(t)
-        case _                =>
-
-          val allSimilar = similarCache.getOrElse {
-            val res = computeSimilar(e).groupBy(_._1).mapValues(_.map(_._2))
-            similarCache = Some(res)
-            res
-          }
-
-          allSimilar.getOrElse(t, Nil)
-      }
-    }
-
-    def computeSimilar(e : Expr)(implicit ctx: LeonContext): Seq[(L, Gen)] = {
-
-      def getLabel(t: TypeTree) = {
-        val tpe = bestRealType(t)
-        val c = getNext()
-        Label(tpe, "G"+c)
-      }
-
-      def isCommutative(e: Expr) = e match {
-        case _: Plus | _: Times => true
-        case _ => false
-      }
-
-      def rec(e: Expr, gl: L): Seq[(L, Gen)] = {
-
-        def gens(e: Expr, gl: L, subs: Seq[Expr], builder: (Seq[Expr] => Expr)): Seq[(L, Gen)] = {
-          val subGls = subs.map { s => getLabel(s.getType) }
-
-          // All the subproductions for sub gl
-          val allSubs = (subs zip subGls).flatMap { case (e, gl) => rec(e, gl) }
-
-          // Inject fix at one place
-          val injectG = for ((sgl, i) <- subGls.zipWithIndex) yield {
-            gl -> Generator[L, Expr](Seq(sgl), { case Seq(ge) => builder(subs.updated(i, ge)) } )
-          }
-
-          val swaps = if (subs.size > 1 && !isCommutative(e)) {
-            (for (i <- 0 until subs.size;
-                 j <- i+1 until subs.size) yield {
-
-              if (subs(i).getType == subs(j).getType) {
-                val swapSubs = subs.updated(i, subs(j)).updated(j, subs(i))
-                Some(gl -> Generator[L, Expr](Seq(), { _ => builder(swapSubs) }))
-              } else {
-                None
-              }
-            }).flatten
-          } else {
-            Nil
-          }
-
-          allSubs ++ injectG ++ swaps
-        }
-
-        def cegis(gl: L): Seq[(L, Gen)] = {
-          normalGrammar.getProductions(gl).map(gl -> _)
-        }
-
-        def int32Variations(gl: L, e : Expr): Seq[(L, Gen)] = {
-          Seq(
-            gl -> Generator(Nil, { _ => BVMinus(e, IntLiteral(1))} ),
-            gl -> Generator(Nil, { _ => BVPlus (e, IntLiteral(1))} )
-          )
-        }
-
-        def intVariations(gl: L, e : Expr): Seq[(L, Gen)] = {
-          Seq(
-            gl -> Generator(Nil, { _ => Minus(e, InfiniteIntegerLiteral(1))} ),
-            gl -> Generator(Nil, { _ => Plus (e, InfiniteIntegerLiteral(1))} )
-          )
-        }
-
-        // Find neighbor case classes that are compatible with the arguments:
-        // Turns And(e1, e2) into Or(e1, e2)...
-        def ccVariations(gl: L, cc: CaseClass): Seq[(L, Gen)] = {
-          val CaseClass(cct, args) = cc
-
-          val neighbors = cct.root.knownCCDescendants diff Seq(cct)
-
-          for (scct <- neighbors if scct.fieldsTypes == cct.fieldsTypes) yield {
-            gl -> Generator[L, Expr](Nil, { _ => CaseClass(scct, args) })
-          }
-        }
-
-        val funFilter = (fd: FunDef) => fd.isSynthetic || (excludeFCalls contains fd)
-        val subs: Seq[(L, Gen)] = e match {
-          
-          case _: Terminal | _: Let | _: LetDef | _: MatchExpr =>
-            gens(e, gl, Nil, { _ => e }) ++ cegis(gl)
-
-          case cc @ CaseClass(cct, exprs) =>
-            gens(e, gl, exprs, { case ss => CaseClass(cct, ss) }) ++ ccVariations(gl, cc)
-
-          case FunctionInvocation(TypedFunDef(fd, _), _) if funFilter(fd) =>
-            // We allow only exact call, and/or cegis extensions
-            /*Seq(el -> Generator[L, Expr](Nil, { _ => e })) ++*/ cegis(gl)
-
-          case Operator(subs, builder) =>
-            gens(e, gl, subs, { case ss => builder(ss) })
-        }
-
-        val terminalsMatching = terminals.collect {
-          case IsTyped(term, tpe) if tpe == gl.getType && term != e =>
-            gl -> Generator[L, Expr](Nil, { _ => term })
-        }
-
-        val variations = e.getType match {
-          case IntegerType => intVariations(gl, e)
-          case Int32Type => int32Variations(gl, e)
-          case _ => Nil
-        }
-
-        subs ++ terminalsMatching ++ variations
-      }
-
-      val gl = getLabel(e.getType)
-
-      val res = rec(e, gl)
-
-      //for ((t, g) <- res) {
-      //  val subs = g.subTrees.map { t => FreshIdentifier(t.asString, t.getType).toVariable}
-      //  val gen = g.builder(subs)
-
-      //  println(f"$t%30s ::= "+gen)
-      //}
-      res
-    }
-  }
-
-  case class FunctionCalls(prog: Program, currentFunction: FunDef, types: Seq[TypeTree], exclude: Set[FunDef]) extends ExpressionGrammar[TypeTree] {
-   def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = {
-
-     def getCandidates(fd: FunDef): Seq[TypedFunDef] = {
-       // Prevents recursive calls
-       val cfd = currentFunction
-
-       val isRecursiveCall = (prog.callGraph.transitiveCallers(cfd) + cfd) contains fd
-
-       val isDet = fd.body.exists(isDeterministic)
-
-       if (!isRecursiveCall && isDet) {
-         val free = fd.tparams.map(_.tp)
-
-         canBeSubtypeOf(fd.returnType, free, t, rhsFixed = true) match {
-           case Some(tpsMap) =>
-             val tfd = fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp)))
-
-             if (tpsMap.size < free.size) {
-               /* Some type params remain free, we want to assign them:
-                *
-                * List[T] => Int, for instance, will be found when
-                * requesting Int, but we need to assign T to viable
-                * types. For that we use list of input types as heuristic,
-                * and look for instantiations of T such that input <?:
-                * List[T].
-                */
-               types.distinct.flatMap { (atpe: TypeTree) =>
-                 var finalFree = free.toSet -- tpsMap.keySet
-                 var finalMap = tpsMap
-
-                 for (ptpe <- tfd.params.map(_.getType).distinct) {
-                   canBeSubtypeOf(atpe, finalFree.toSeq, ptpe) match {
-                     case Some(ntpsMap) =>
-                       finalFree --= ntpsMap.keySet
-                       finalMap  ++= ntpsMap
-                     case _ =>
-                   }
-                 }
-
-                 if (finalFree.isEmpty) {
-                   List(fd.typed(free.map(tp => finalMap.getOrElse(tp, tp))))
-                 } else {
-                   Nil
-                 }
-               }
-             } else {
-               /* All type parameters that used to be free are assigned
-                */
-               List(tfd)
-             }
-           case None =>
-             Nil
-         }
-       } else {
-         Nil
-       }
-     }
-
-     val filter = (tfd:TypedFunDef) => tfd.fd.isSynthetic || (exclude contains tfd.fd)
-     val funcs = functionsAvailable(prog).toSeq.flatMap(getCandidates).filterNot(filter)
-
-     funcs.map{ tfd =>
-       Generator[TypeTree, Expr](tfd.params.map(_.getType), { sub => FunctionInvocation(tfd, sub) })
-     }
-   }
-  }
-
-  case class SizedLabel[T <% Typed](underlying: T, size: Int) extends Typed {
-    val getType = underlying.getType
-
-    override def asString(implicit ctx: LeonContext) = underlying.asString+"|"+size+"|"
-  }
-
-  case class SizeBoundedGrammar[T <% Typed](g: ExpressionGrammar[T]) extends ExpressionGrammar[SizedLabel[T]] {
-    def computeProductions(sl: SizedLabel[T])(implicit ctx: LeonContext): Seq[Gen] = {
-      if (sl.size <= 0) {
-        Nil
-      } else if (sl.size == 1) {
-        g.getProductions(sl.underlying).filter(_.subTrees.isEmpty).map {
-          case Generator(subTrees, builder) =>
-            Generator[SizedLabel[T], Expr](Nil, builder)
-        }
-      } else {
-        g.getProductions(sl.underlying).filter(_.subTrees.nonEmpty).flatMap {
-          case Generator(subTrees, builder) =>
-            val sizes = sumTo(sl.size-1, subTrees.size)
-
-            for (ss <- sizes) yield {
-              val subSizedLabels = (subTrees zip ss) map (s => SizedLabel(s._1, s._2))
-
-              Generator[SizedLabel[T], Expr](subSizedLabels, builder)
-            }
-        }
-      }
-    }
-  }
-
-  case class BoundedGrammar[T](g: ExpressionGrammar[Label[T]], bound: Int) extends ExpressionGrammar[Label[T]] {
-    def computeProductions(l: Label[T])(implicit ctx: LeonContext): Seq[Gen] = g.computeProductions(l).flatMap {
-      case g: Generator[Label[T], Expr] =>
-        if (l.depth == Some(bound) && g.subTrees.nonEmpty) {
-          None
-        } else if (l.depth.exists(_ > bound)) {
-          None
-        } else {
-          Some(Generator(g.subTrees.map(sl => sl.copy(depth = l.depth.map(_+1).orElse(Some(1)))), g.builder))
-        }
-    }
-
-  }
-
-  case class EmbeddedGrammar[Ti <% Typed, To <% Typed](g: ExpressionGrammar[Ti], iToo: Ti => To, oToi: To => Ti) extends ExpressionGrammar[To] {
-    def computeProductions(t: To)(implicit ctx: LeonContext): Seq[Gen] = g.computeProductions(oToi(t)).map {
-      case g : Generator[Ti, Expr] =>
-        Generator(g.subTrees.map(iToo), g.builder)
-    }
-  }
-
-  case class SafeRecCalls(prog: Program, ws: Expr, pc: Expr) extends ExpressionGrammar[TypeTree] {
-    def computeProductions(t: TypeTree)(implicit ctx: LeonContext): Seq[Gen] = {
-      val calls = terminatingCalls(prog, t, ws, pc)
-
-      calls.map {
-        case (e, free) =>
-          val freeSeq = free.toSeq
-          Generator[TypeTree, Expr](freeSeq.map(_.getType), { sub =>
-            replaceFromIDs(freeSeq.zip(sub).toMap, e)
-          })
-      }
-    }
-  }
-
-  def default(prog: Program, inputs: Seq[Expr], currentFunction: FunDef, exclude: Set[FunDef], ws: Expr, pc: Expr): ExpressionGrammar[TypeTree] = {
-    BaseGrammar ||
-    EqualityGrammar(Set(IntegerType, Int32Type, BooleanType) ++ inputs.map { _.getType }) ||
-    OneOf(inputs) ||
-    FunctionCalls(prog, currentFunction, inputs.map(_.getType), exclude) ||
-    SafeRecCalls(prog, ws, pc)
-  }
-
-  def default(sctx: SynthesisContext, p: Problem): ExpressionGrammar[TypeTree] = {
-    default(sctx.program, p.as.map(_.toVariable), sctx.functionContext, sctx.settings.functionsToIgnore,  p.ws, p.pc)
-  }
-
-  def depthBound[T <% Typed](g: ExpressionGrammar[T], b: Int) = {
-    g.filter(g => g.subTrees.forall(t => typeDepth(t.getType) <= b))
-  }
-}