diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 90e222933bb9c8ce647fb7267b204e75fa436c53..db23f2a6ace4ca8d9e0a3bbc5e85dc2a4e6377f0 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -3,6 +3,7 @@
 package leon
 
 import leon.utils._
+import leon.verification.VerificationReport
 
 object Main {
 
@@ -11,7 +12,7 @@ object Main {
       frontends.scalac.ExtractionPhase,
       frontends.scalac.ClassgenPhase,
       utils.TypingPhase,
-      FileOutputPhase,
+      utils.FileOutputPhase,
       purescala.RestoreMethods,
       xlang.ArrayTransformation,
       xlang.EpsilonElimination,
@@ -192,14 +193,18 @@ object Main {
           ExtractionPhase andThen
           new PreprocessingPhase(xlangF)
 
-      val verification = if (xlangF) VerificationPhase andThen FixReportLabels else VerificationPhase
+      val verification =
+        VerificationPhase andThen
+        (if (xlangF) FixReportLabels else NoopPhase[VerificationReport]()) andThen
+        PrintReportPhase
+      val termination  = TerminationPhase andThen PrintReportPhase
 
       val pipeProcess: Pipeline[Program, Any] = {
         if (noopF) RestoreMethods andThen FileOutputPhase
         else if (synthesisF) SynthesisPhase
         else if (repairF) RepairPhase
-        else if (analysisF) Pipeline.both(verification, TerminationPhase)
-        else if (terminationF) TerminationPhase
+        else if (analysisF) Pipeline.both(verification, termination)
+        else if (terminationF) termination
         else if (isabelleF) IsabellePhase
         else if (evalF) EvaluationPhase
         else if (inferInvF) InferInvariantsPhase
@@ -264,23 +269,7 @@ object Main {
       val timer = ctx.timers.total.start()
 
       // Run pipeline
-      val ctx2 = pipeline.run(ctx, args.toList) match {
-        case (ctx2, (vReport: verification.VerificationReport, tReport: termination.TerminationReport)) =>
-          ctx2.reporter.info(vReport.summaryString)
-          ctx2.reporter.info(tReport.summaryString)
-          ctx2
-
-        case (ctx2, report: verification.VerificationReport) =>
-          ctx2.reporter.info(report.summaryString)
-          ctx2
-
-        case (ctx2, report: termination.TerminationReport) =>
-          ctx2.reporter.info(report.summaryString)
-          ctx2
-
-        case (ctx2, _) =>
-          ctx2
-      }
+      val (ctx2, _) = pipeline.run(ctx, args.toList)
 
       timer.stop()
 
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index 7a10fe411a8e17c5d91022785552f8615328c045..c7fc3a0b3d7a870b7730022da35e7c3fa3f7483d 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -4,9 +4,10 @@ package leon
 package termination
 
 import purescala.Definitions._
+import utils.Report
 import utils.ASCIIHelpers._
 
-case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) {
+case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
 
   def summaryString : String = {
     var t = Table("Termination summary")
diff --git a/src/main/scala/leon/utils/PrintReportPhase.scala b/src/main/scala/leon/utils/PrintReportPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cf19df7575fd299254315eabcd3fdca4bd5fb568
--- /dev/null
+++ b/src/main/scala/leon/utils/PrintReportPhase.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package utils
+
+/** Pretty-prints a [[Report]] */
+case object PrintReportPhase extends UnitPhase[Report] {
+
+  override val description: String = "Print a Leon report"
+  override val name: String = "PrintReport"
+
+  override def apply(ctx: LeonContext, rep: Report): Unit = {
+    ctx.reporter.info(rep.summaryString)
+  }
+
+}
diff --git a/src/main/scala/leon/utils/Report.scala b/src/main/scala/leon/utils/Report.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4e4a64dbe749f4cbf61f8036709936bbf68dd88e
--- /dev/null
+++ b/src/main/scala/leon/utils/Report.scala
@@ -0,0 +1,8 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.utils
+
+/** Represents a pretty-printable report */
+abstract class Report {
+  def summaryString: String
+}
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 847a23a2a3348f6961b596f5443f0a7b7d336c74..374122f72781e4e0c24ee05e6a96fa18cfed5be5 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -4,8 +4,9 @@ package leon
 package verification
 
 import purescala.Definitions.Program
+import utils.Report
 
-case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {
+case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) extends Report {
   val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
     case (vc, or) => (vc, or.getOrElse(VCResult.unknown))
   }