diff --git a/src/main/scala/leon/Printable.scala b/src/main/scala/leon/Printable.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cbe2e8ed93ef52f50b245d0d099375fb9b8e3af8
--- /dev/null
+++ b/src/main/scala/leon/Printable.scala
@@ -0,0 +1,8 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+
+/** A trait for objects that can be pretty-printed given a [[leon.LeonContext]] */
+trait Printable {
+  def asString(implicit ctx: LeonContext): String
+}
diff --git a/src/main/scala/leon/purescala/Printable.scala b/src/main/scala/leon/purescala/Printable.scala
deleted file mode 100644
index 27be035386699e945610cdc7857bbb9b5f8e73d3..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/purescala/Printable.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-package leon
-package purescala
-
-
-trait Printable {
-  def asString(implicit ctx: LeonContext): String
-}
diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala
index e811feaa1dda6886fa9c9ad927c6f552efb7b7a1..fada59c1741604f1ee6629b532c3b6dc8502425b 100644
--- a/src/main/scala/leon/solvers/ADTManager.scala
+++ b/src/main/scala/leon/solvers/ADTManager.scala
@@ -6,12 +6,12 @@ package solvers
 import purescala.Types._
 import purescala.Common._
 
-case class DataType(sym: Identifier, cases: Seq[Constructor]) {
+case class DataType(sym: Identifier, cases: Seq[Constructor]) extends Printable {
   def asString(implicit ctx: LeonContext) = {
     "Datatype: "+sym.asString+"\n"+cases.map(c => " - "+c.asString(ctx)).mkString("\n")
   }
 }
-case class Constructor(sym: Identifier, tpe: TypeTree, fields: Seq[(Identifier, TypeTree)]) {
+case class Constructor(sym: Identifier, tpe: TypeTree, fields: Seq[(Identifier, TypeTree)]) extends Printable {
   def asString(implicit ctx: LeonContext) = {
     sym.asString(ctx)+" ["+tpe.asString(ctx)+"] "+fields.map(f => f._1.asString(ctx)+": "+f._2.asString(ctx)).mkString("(", ", ", ")")
   }
diff --git a/src/main/scala/leon/solvers/Model.scala b/src/main/scala/leon/solvers/Model.scala
index 57f93655f5311655ffd1d479762dac839e750517..59b6c9064336bbe0e808f03dc3afab8493db017d 100644
--- a/src/main/scala/leon/solvers/Model.scala
+++ b/src/main/scala/leon/solvers/Model.scala
@@ -9,7 +9,8 @@ import purescala.Quantification.Domains
 import purescala.ExprOps._
 
 trait AbstractModel[+This <: Model with AbstractModel[This]]
-  extends scala.collection.IterableLike[(Identifier, Expr), This] {
+  extends scala.collection.IterableLike[(Identifier, Expr), This]
+  with Printable {
 
   protected val mapping: Map[Identifier, Expr]
 
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index cb7fe90d280160d03a5b9fbc190a7851b3cd3c1b..1866fc72bb4fcb6e5a45d1fbf21b5768fd3ce104 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -4,7 +4,6 @@ package leon
 package solvers
 package templates
 
-import purescala.Printable
 import purescala.Common._
 import purescala.Expressions._
 import purescala.Types._
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 5c12fd3863da241f09a667133731a9b31182f10f..ee6197774c72d923ed32295b835b41e0217d5d6c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -7,7 +7,6 @@ package z3
 import utils._
 import _root_.z3.scala._
 
-import purescala.Printable
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index bc587339270904f1f7421e088db6ce26a72c4b03..8449d37a51f86bba52f8f8c4ac981d0f73ca2336 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -23,7 +23,7 @@ case class Cost(minSize: Int) extends AnyVal with Ordered[Cost] {
     this.minSize-that.minSize
   }
 
-  def asString: String = {
+  override def toString: String = {
     f"$minSize%3d"
   }
 }
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index ae6e24bbc6b7a678460b4ab109520c3bd36485dd..3340816aa3d572cd9712bfe1ee90bedeff114327 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -4,9 +4,8 @@ package leon
 package synthesis
 
 import purescala.Expressions._
-import leon.utils.ASCIIHelpers._
 
-sealed abstract class Example {
+sealed abstract class Example extends Printable {
   def ins: Seq[Expr]
 
   def asString(implicit ctx: LeonContext) = {
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index f51fe3dd55caac5d23aa74677aebe1890e412840..d59d956e973337b64ba6d19d2f66efde206dcecc 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -21,7 +21,7 @@ import Witnesses._
   * @param phi The formula on `as` and `xs` to satisfy
   * @param xs The list of output identifiers for which we want to compute a function
   */
-case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier], eb: ExamplesBank = ExamplesBank.empty) {
+case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier], eb: ExamplesBank = ExamplesBank.empty) extends Printable {
 
   def inType  = tupleTypeWrap(as.map(_.getType))
   def outType = tupleTypeWrap(xs.map(_.getType))
@@ -35,7 +35,7 @@ case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List
         |   ${pcws.asString} ≺
         |   ⟨ ${phi.asString} ⟩ 
         |   ${if (xs.nonEmpty) xs.map(_.asString).mkString(", ") else "()"}
-        |⟧  """.stripMargin + ebInfo
+        |⟧  $ebInfo""".stripMargin
   }
 
   def withWs(es: Seq[Expr]) = {
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 6f8b3781d4def4037b23788b93f4657ea7b97c2f..f3019de656983b0dad92dda9231d185987e6cecc 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -11,7 +11,7 @@ import purescala.Constructors._
 import rules._
 
 /** A Rule can be applied on a synthesis problem */
-abstract class Rule(val name: String) extends RuleDSL {
+abstract class Rule(val name: String) extends RuleDSL with Printable {
   def instantiateOn(implicit hctx: SearchContext, problem: Problem): Traversable[RuleInstantiation]
 
   val priority: RulePriority = RulePriorityDefault
@@ -78,7 +78,7 @@ object Rules {
 /** When applying this to a [SearchContext] it returns a wrapped stream of solutions or a new list of problems. */
 abstract class RuleInstantiation(val description: String,
                                  val onSuccess: SolutionBuilder = SolutionBuilderCloser())
-                                (implicit val problem: Problem, val rule: Rule) {
+                                (implicit val problem: Problem, val rule: Rule) extends Printable {
 
   def apply(hctx: SearchContext): RuleApplication
 
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 24a518fa938cbecd1bfb3c82e2c3194b33a8f12a..428df1ee6154b9eb93e67a9de7361bbef9e7c2aa 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -14,7 +14,7 @@ import leon.utils.Simplifiers
 
 // Defines a synthesis solution of the form:
 // ⟨ P | T ⟩
-class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrusted: Boolean = true) {
+class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr, val isTrusted: Boolean = true) extends Printable {
 
   def asString(implicit ctx: LeonContext) = {
     "⟨ "+pre.asString+" | "+defs.map(_.asString).mkString(" ")+" "+term.asString+" ⟩" 
diff --git a/src/main/scala/leon/synthesis/graph/Graph.scala b/src/main/scala/leon/synthesis/graph/Graph.scala
index 3bb9fbff92bba0abc29d0a399785023e523e3861..2af026aaa7b4f43e896b8948c639e3970e78fad8 100644
--- a/src/main/scala/leon/synthesis/graph/Graph.scala
+++ b/src/main/scala/leon/synthesis/graph/Graph.scala
@@ -27,7 +27,7 @@ sealed class Graph(problem: Problem) {
   }
 }
 
-sealed abstract class Node(val parent: Option[Node]) {
+sealed abstract class Node(val parent: Option[Node]) extends Printable {
 
   def asString(implicit ctx: LeonContext): String
 
diff --git a/src/main/scala/leon/synthesis/strategies/CostBasedStrategy.scala b/src/main/scala/leon/synthesis/strategies/CostBasedStrategy.scala
index 70ccc90ab0175828a65866f7a5c347c0b2e18dd5..e309593fe7afeca716baa6e99c8a1f34d6d816c7 100644
--- a/src/main/scala/leon/synthesis/strategies/CostBasedStrategy.scala
+++ b/src/main/scala/leon/synthesis/strategies/CostBasedStrategy.scala
@@ -90,5 +90,5 @@ class CostBasedStrategy(ctx: LeonContext, cm: CostModel) extends Strategy {
     recomputeCost(n)
   }
 
-  def debugInfoFor(n: Node) = bestCosts.get(n).map(_.asString).getOrElse("?")
+  def debugInfoFor(n: Node) = bestCosts.get(n).map(_.toString).getOrElse("?")
 }
diff --git a/src/main/scala/leon/utils/FreeableIterator.scala b/src/main/scala/leon/utils/FreeableIterator.scala
index a790b2dbf7a713ea681888fa9719da913140ca5c..b288dcae46e5f19c2ae9f6bf9da99656478825b0 100644
--- a/src/main/scala/leon/utils/FreeableIterator.scala
+++ b/src/main/scala/leon/utils/FreeableIterator.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 package utils