diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index e10036a3615a773a57b0721c08b20f8fb3848c2e..38206418d10e0a6c83e7dfea968ef7709d92bb9f 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -11,7 +11,7 @@ import Definitions.Program
 object Common {
 
 
-  abstract class Tree extends Positioned with Serializable {
+  abstract class Tree extends Positioned with Serializable with Printable {
     def copiedFrom(o: Tree): this.type = {
       setPos(o)
       this
diff --git a/src/main/scala/leon/purescala/Printable.scala b/src/main/scala/leon/purescala/Printable.scala
new file mode 100644
index 0000000000000000000000000000000000000000..27be035386699e945610cdc7857bbb9b5f8e73d3
--- /dev/null
+++ b/src/main/scala/leon/purescala/Printable.scala
@@ -0,0 +1,7 @@
+package leon
+package purescala
+
+
+trait Printable {
+  def asString(implicit ctx: LeonContext): String
+}
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index b780cfb696bfa5da28f06a4e85a2671a009b1e33..d39fda3338fbeab4dfa9c453a58afa6298bb6ccd 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -12,11 +12,9 @@ import TypeOps._
 
 object Types {
 
-  trait Typed {
+  trait Typed extends Printable {
     val getType: TypeTree
     def isTyped : Boolean = getType != Untyped
-
-    def asString(implicit ctx: LeonContext): String
   }
 
   class TypeErrorException(msg: String) extends Exception(msg)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index b3365ba2835e0232dcb57545b5ba85b87cdd2d5d..26fb3d9a1e39204bf7a047a44983ebad8f2053ae 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -494,6 +494,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
       case BVUMinus(u) => FixedSizeBitVectors.Neg(toSMT(u))
       case BVNot(u) => FixedSizeBitVectors.Not(toSMT(u))
       case Assert(a,_, b) => toSMT(IfExpr(a, b, Error(b.getType, "assertion failed")))
+
       case Equals(a,b) => Core.Equals(toSMT(a), toSMT(b))
       case Implies(a,b) => Core.Implies(toSMT(a), toSMT(b))
       case Plus(a,b) => Ints.Add(toSMT(a), toSMT(b))
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index 95a9e47cec1e606fbd6ca0b399f777779db86cf2..07bc7de6dae3d4e741a901889b9f27e6cfcb41ba 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -4,12 +4,13 @@ package leon
 package solvers
 package templates
 
+import purescala.Printable
 import purescala.Common._
 import purescala.Expressions._
 import purescala.Types._
 import utils._
 
-class UnrollingBank[T](ctx: LeonContext, templateGenerator: TemplateGenerator[T]) extends IncrementalState {
+class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: TemplateGenerator[T]) extends IncrementalState {
   implicit val debugSection = utils.DebugSectionSolver
   implicit val ctx0 = ctx
   val reporter = ctx.reporter
@@ -194,7 +195,7 @@ class UnrollingBank[T](ctx: LeonContext, templateGenerator: TemplateGenerator[T]
 
     reporter.debug("Generating clauses for: " + expr.asString)
     for (cls <- clauses) {
-      reporter.debug("  . " + cls)
+      reporter.debug("  . " + cls.asString(ctx))
     }
 
     clauses
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 5a42c60c49629056b65e560e4bffe37be0b3c2f2..eef9ffb9071d1291831e41a69105e4884168a6aa 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -7,6 +7,7 @@ package z3
 import utils._
 import _root_.z3.scala._
 
+import purescala.Printable
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
@@ -122,6 +123,10 @@ class FairZ3Solver(val context: LeonContext, val program: Program)
     }
   }
 
+  implicit val z3Printable = (z3: Z3AST) => new Printable {
+    def asString(implicit ctx: LeonContext) = z3.toString
+  }
+
   val templateGenerator = new TemplateGenerator(new TemplateEncoder[Z3AST] {
     def encodeId(id: Identifier): Z3AST = {
       idToFreshZ3Id(id)