diff --git a/src/main/scala/leon/grammars/DepthBoundedGrammar.scala b/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
index 7ec864e03a32511f05be3361d1233bdb436109dc..fc999be644bf2c4a7a20a73403cf7b1001bb9b68 100644
--- a/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
+++ b/src/main/scala/leon/grammars/DepthBoundedGrammar.scala
@@ -3,8 +3,8 @@
 package leon
 package grammars
 
-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 class DepthBoundedGrammar[T](g: ExpressionGrammar[NonTerminal[T]], bound: Int) extends ExpressionGrammar[NonTerminal[T]] {
+  def computeProductions(l: NonTerminal[T])(implicit ctx: LeonContext): Seq[Gen] = g.computeProductions(l).flatMap {
     case gen =>
       if (l.depth == Some(bound) && gen.subTrees.nonEmpty) {
         Nil
diff --git a/src/main/scala/leon/grammars/EmbeddedGrammar.scala b/src/main/scala/leon/grammars/EmbeddedGrammar.scala
index bcee19b0118b896468994acbfe80a497f02012fd..8dcbc6ec10f9aa42895e5f876cdd4d72479de229 100644
--- a/src/main/scala/leon/grammars/EmbeddedGrammar.scala
+++ b/src/main/scala/leon/grammars/EmbeddedGrammar.scala
@@ -12,7 +12,7 @@ import purescala.Constructors._
  * 
  * 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] {
+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
index 56b332309329acb8017ccbb8bdb9f71711e22eb2..70ebddc98f21fc872aef8635fe36de7e9ba9bbce 100644
--- a/src/main/scala/leon/grammars/Empty.scala
+++ b/src/main/scala/leon/grammars/Empty.scala
@@ -3,8 +3,8 @@
 package leon
 package grammars
 
-import purescala.Types._
+import purescala.Types.Typed
 
-case class Empty[T <% Typed]() extends ExpressionGrammar[T] {
+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/ExpressionGrammar.scala b/src/main/scala/leon/grammars/ExpressionGrammar.scala
index 465904f5db3b4e7289f8ce0b8a13aa86798bf72e..01a3524d18b24e35f6912fdae034f4988fb7779e 100644
--- a/src/main/scala/leon/grammars/ExpressionGrammar.scala
+++ b/src/main/scala/leon/grammars/ExpressionGrammar.scala
@@ -11,7 +11,7 @@ import purescala.Common._
 
 import scala.collection.mutable.{HashMap => MutableMap}
 
-abstract class ExpressionGrammar[T <% Typed] {
+abstract class ExpressionGrammar[T <: Typed] {
   type Gen = Generator[T, Expr]
 
   private[this] val cache = new MutableMap[T, Seq[Gen]]()
diff --git a/src/main/scala/leon/grammars/Grammars.scala b/src/main/scala/leon/grammars/Grammars.scala
index 2194aa539afe94dc06182b5acaf12bb669de0612..23b1dd5a14cfeb82dd4555832e777597615b337e 100644
--- a/src/main/scala/leon/grammars/Grammars.scala
+++ b/src/main/scala/leon/grammars/Grammars.scala
@@ -24,7 +24,7 @@ object Grammars {
     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) = {
+  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/NonTerminal.scala
similarity index 71%
rename from src/main/scala/leon/grammars/Label.scala
rename to src/main/scala/leon/grammars/NonTerminal.scala
index aaaaccf308d4f60883ac79c46ef92b140426227a..7492ffac5c17df326084f846857c6ac3bebe1775 100644
--- a/src/main/scala/leon/grammars/Label.scala
+++ b/src/main/scala/leon/grammars/NonTerminal.scala
@@ -5,7 +5,7 @@ package grammars
 
 import purescala.Types._
 
-case class Label[T](t: TypeTree, l: T, depth: Option[Int] = None) extends Typed {
+case class NonTerminal[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/Or.scala b/src/main/scala/leon/grammars/Or.scala
index ae0bc96976f1a4d2d349a72060e391686b4cab52..e691a245984eaeb11277b9278505b49cf623fed3 100644
--- a/src/main/scala/leon/grammars/Or.scala
+++ b/src/main/scala/leon/grammars/Or.scala
@@ -5,7 +5,7 @@ package grammars
 
 import purescala.Types._
 
-case class Union[T <% Typed](gs: Seq[ExpressionGrammar[T]]) extends ExpressionGrammar[T] {
+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)
diff --git a/src/main/scala/leon/grammars/SimilarTo.scala b/src/main/scala/leon/grammars/SimilarTo.scala
index c134546d2af88039d2ef5f9a9a030e331ae80161..77e912792965d860fc934eb016370c8f2b57fd8f 100644
--- a/src/main/scala/leon/grammars/SimilarTo.scala
+++ b/src/main/scala/leon/grammars/SimilarTo.scala
@@ -13,7 +13,7 @@ import purescala.Expressions._
 
 import synthesis._
 
-case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[Label[String]] {
+case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisContext, p: Problem) extends ExpressionGrammar[NonTerminal[String]] {
 
   val excludeFCalls = sctx.settings.functionsToIgnore
 
@@ -23,11 +23,11 @@ case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisConte
       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 }
+    { (t: TypeTree)      => NonTerminal(t, "B", None)},
+    { (l: NonTerminal[String]) => l.getType }
   ), 1)
 
-  type L = Label[String]
+  type L = NonTerminal[String]
 
   val getNext: () => Int = {
     var counter = -1
@@ -41,7 +41,7 @@ case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisConte
 
   def computeProductions(t: L)(implicit ctx: LeonContext): Seq[Gen] = {
     t match {
-      case Label(_, "B", _) => normalGrammar.computeProductions(t)
+      case NonTerminal(_, "B", _) => normalGrammar.computeProductions(t)
       case _                =>
 
         val allSimilar = similarCache.getOrElse {
@@ -59,7 +59,7 @@ case class SimilarTo(e: Expr, terminals: Set[Expr] = Set(), sctx: SynthesisConte
     def getLabel(t: TypeTree) = {
       val tpe = bestRealType(t)
       val c = getNext()
-      Label(tpe, "G"+c)
+      NonTerminal(tpe, "G"+c)
     }
 
     def isCommutative(e: Expr) = e match {
diff --git a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
index 8756b136abf0f6bbffe6721bb3439aebc76a0a6b..1b25e30f61aa74598feb255366fe10a153bc9e30 100644
--- a/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
+++ b/src/main/scala/leon/grammars/SizeBoundedGrammar.scala
@@ -6,13 +6,13 @@ package grammars
 import purescala.Types._
 import leon.utils.SeqUtils.sumTo
 
-case class SizedLabel[T <% Typed](underlying: T, size: Int) extends Typed {
+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]] {
+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
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 3d39ae7e7e99e45b344859d46496c31baa17ad8c..c975fd2d37e7563137d9b1fd4cbe0f2cbb7892f4 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -137,6 +137,8 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
   private val freeVars    = new IncrementalSet[Identifier]()
   private val constraints = new IncrementalSeq[Expr]()
 
+  val tr = implicitly[Z3AST => Printable]
+
   val unrollingBank = new UnrollingBank(context, templateGenerator)
 
   private val incrementals: List[IncrementalState] = List(
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index 990be35e1801b5145997ec3da71471a504febec5..97b810ac367de8e0843ffb78a50f61f694966d43 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -26,7 +26,7 @@ case object BottomUpTEGIS extends BottomUpTEGISLike[TypeTree]("BU TEGIS") {
   def getRootLabel(tpe: TypeTree): TypeTree = tpe
 }
 
-abstract class BottomUpTEGISLike[T <% Typed](name: String) extends Rule(name) {
+abstract class BottomUpTEGISLike[T <: Typed](name: String) extends Rule(name) {
   def getGrammar(sctx: SynthesisContext, p: Problem): ExpressionGrammar[T]
 
   def getRootLabel(tpe: TypeTree): T
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 4824d3e536a86cad18a800468c53433a2f5dc4dc..d577f7f9fe1f260f4af9ca4d3cb20ca868e37fcc 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -22,7 +22,7 @@ import evaluators._
 import datagen._
 import codegen.CodeGenParams
 
-abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
+abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
 
   case class CegisParams(
     grammar: ExpressionGrammar[T],
diff --git a/src/main/scala/leon/synthesis/rules/CEGLESS.scala b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
index 6b0bbdd15e257841026da4f64cf8e0857f8ed1c7..e2e8c9fabc04cddea941b5b807a2df89f9742862 100644
--- a/src/main/scala/leon/synthesis/rules/CEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGLESS.scala
@@ -11,7 +11,7 @@ import utils._
 import grammars._
 import Witnesses._
 
-case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
+case object CEGLESS extends CEGISLike[NonTerminal[String]]("CEGLESS") {
   def getParams(sctx: SynthesisContext, p: Problem) = {
     val TopLevelAnds(clauses) = p.ws
 
@@ -30,11 +30,11 @@ case object CEGLESS extends CEGISLike[Label[String]]("CEGLESS") {
       }
     }
 
-    val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _)
+    val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[NonTerminal[String]]](Empty())(_ || _)
 
     CegisParams(
       grammar = guidedGrammar,
-      rootLabel = { (tpe: TypeTree) => Label(tpe, "G0") },
+      rootLabel = { (tpe: TypeTree) => NonTerminal(tpe, "G0") },
       maxUnfoldings = (0 +: guides.map(depth(_) + 1)).max
     )
   }
diff --git a/src/main/scala/leon/synthesis/rules/TEGISLike.scala b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
index 2e9da57ce9cc10fc9ea792751605cb7e3c10193c..164e396be5f77ea109828921b5f3157d8c85fa43 100644
--- a/src/main/scala/leon/synthesis/rules/TEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGISLike.scala
@@ -17,7 +17,7 @@ import scala.collection.mutable.{HashMap => MutableMap}
 
 import bonsai.enumerators._
 
-abstract class TEGISLike[T <% Typed](name: String) extends Rule(name) {
+abstract class TEGISLike[T <: Typed](name: String) extends Rule(name) {
   case class TegisParams(
     grammar: ExpressionGrammar[T],
     rootLabel: TypeTree => T,
diff --git a/src/main/scala/leon/synthesis/rules/TEGLESS.scala b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
index d8de10cbb952b764916386f9accdca98129f2c71..f56b26b26d859566c77c91f484deac41930f2aa7 100644
--- a/src/main/scala/leon/synthesis/rules/TEGLESS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGLESS.scala
@@ -10,7 +10,7 @@ import utils._
 import Witnesses._
 import grammars._
 
-case object TEGLESS extends TEGISLike[Label[String]]("TEGLESS") {
+case object TEGLESS extends TEGISLike[NonTerminal[String]]("TEGLESS") {
   def getParams(sctx: SynthesisContext, p: Problem) = {
 
     val TopLevelAnds(clauses) = p.ws
@@ -28,11 +28,11 @@ case object TEGLESS extends TEGISLike[Label[String]]("TEGLESS") {
       }
     }
 
-    val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[Label[String]]](Empty())(_ || _)
+    val guidedGrammar = guides.map(SimilarTo(_, inputs.toSet, sctx, p)).foldLeft[ExpressionGrammar[NonTerminal[String]]](Empty())(_ || _)
 
     TegisParams(
       grammar = guidedGrammar,
-      rootLabel = { (tpe: TypeTree) => Label(tpe, "G0") }
+      rootLabel = { (tpe: TypeTree) => NonTerminal(tpe, "G0") }
     )
   }
 }