diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 5be1d35373166613fae809b8a1f5a151321debac..b1840d8d81ce4cf2067be45bfd75b6dc0aeb0c8d 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -153,6 +153,14 @@ object Main {
     val verifyF      = ctx.findOptionOrDefault(optVerify)
     val evalF        = ctx.findOptionOrDefault(optEval)
 
+    def debugTrees(title: String): LeonPhase[Program, Program] = {
+      if (ctx.reporter.isDebugEnabled(DebugSectionTrees)) {
+        PrintTreePhase(title)
+      } else {
+        NoopPhase[Program]
+      }
+    }
+
     if (helpF) {
       displayVersion(ctx.reporter)
       displayHelp(ctx.reporter, error = false)
@@ -160,11 +168,15 @@ object Main {
       val pipeBegin: Pipeline[List[String], Program] =
         if (xlangF)
           ExtractionPhase andThen
-            PreprocessingPhase
+          debugTrees("Program after extraction") andThen
+          PreprocessingPhase andThen
+          debugTrees("Program after pre-processing")
         else
           ExtractionPhase andThen
-            PreprocessingPhase andThen
-            xlang.NoXLangFeaturesChecking
+          debugTrees("Program after extraction") andThen
+          PreprocessingPhase andThen
+          debugTrees("Program after pre-processing")
+          xlang.NoXLangFeaturesChecking
 
       val pipeProcess: Pipeline[Program, Any] = {
         if (noopF) RestoreMethods andThen FileOutputPhase
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 52fedd3a83a7ad007665c99cb265c74df47b9ea0..b326f51465d56cfc2f7e5745f8cc77d5261efdc1 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -69,14 +69,18 @@ abstract class Reporter(val debugSections: Set[DebugSection]) {
   // Debugging
   private val debugMask = debugSections.foldLeft(0){ _ | _.mask }
 
+  def isDebugEnabled(implicit section: DebugSection): Boolean = {
+    (debugMask & section.mask) == section.mask
+  }
+
   def ifDebug(body: (Any => Unit) => Any)(implicit section: DebugSection) = {
-    if ((debugMask & section.mask) == section.mask) {
+    if (isDebugEnabled) {
       body( { (msg: Any) => emit(account(Message(DEBUG(section), NoPosition, msg))) } )
     }
   }
 
   def whenDebug(section: DebugSection)(body: (Any => Unit) => Any) {
-    if ((debugMask & section.mask) == section.mask) {
+    if (isDebugEnabled(section)) {
       body( { (msg: Any) => emit(account(Message(DEBUG(section), NoPosition, msg))) } )
     }
   }
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index c4131034a5c215890de58a4042f9dff945f969ec..80a6691a15f1348e089f7a80d61b974f84ca8742 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -6,6 +6,8 @@ package frontends.scalac
 import purescala.Definitions.Program
 import purescala.Common.FreshIdentifier
 
+import purescala.ScalaPrinter
+
 import utils._
 
 import scala.tools.nsc.{Settings,CompilerCommand}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
index 71bec02b1284bbd462188120a5e0ffe6210ff127..0f51eb6ed97fd8615a42b7ce18c625d89f35989d 100644
--- a/src/main/scala/leon/utils/PreprocessingPhase.scala
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -4,6 +4,7 @@ package leon
 package utils
 
 import purescala.Definitions.Program
+import purescala.ScalaPrinter
 
 import purescala.{MethodLifting, CompleteAbstractDefinitions}
 import synthesis.{ConvertWithOracle, ConvertHoles}
@@ -25,6 +26,7 @@ object PreprocessingPhase extends TransformationPhase {
       CompleteAbstractDefinitions   andThen
       InjectAsserts
 
+
     phases.run(ctx)(p)
   }
 }
diff --git a/src/main/scala/leon/utils/PrintTreePhase.scala b/src/main/scala/leon/utils/PrintTreePhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c28a90722da8ad9e93421aa1828754b7aa9a8138
--- /dev/null
+++ b/src/main/scala/leon/utils/PrintTreePhase.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon
+package utils
+
+
+import purescala.Definitions.Program
+
+case class PrintTreePhase(title: String) extends UnitPhase[Program] {
+
+  val name = "Print program"
+  val description = "Display: "+title
+
+  def apply(ctx: LeonContext, p: Program) {
+    ctx.reporter.info(ASCIIHelpers.title(title))
+    ctx.reporter.info(p.asString(ctx))
+  }
+}