diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 66a54ec4cfb1b89be398731d182e1160dbcf6dcb..04df65e6d6cae81c9def1c08adcbb0fc509e8eff 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -149,6 +149,7 @@ object Main {
     val synthesisF   = ctx.findOptionOrDefault(optSynthesis)
     val xlangF       = ctx.findOptionOrDefault(optXLang)
     val repairF      = ctx.findOptionOrDefault(optRepair)
+    val analysisF    = ctx.findOption(optVerify).isDefined && ctx.findOption(optTermination).isDefined
     val terminationF = ctx.findOptionOrDefault(optTermination)
     val verifyF      = ctx.findOptionOrDefault(optVerify)
     val evalF        = ctx.findOption(SharedOptions.optEval)
@@ -182,6 +183,7 @@ object Main {
         if (noopF) RestoreMethods andThen FileOutputPhase
         else if (synthesisF) SynthesisPhase
         else if (repairF) RepairPhase
+        else if (analysisF) Pipeline.both(FunctionClosure andThen AnalysisPhase, TerminationPhase)
         else if (terminationF) TerminationPhase
         else if (xlangF) XLangAnalysisPhase
         else if (evalF.isDefined) EvaluationPhase
@@ -246,6 +248,10 @@ object Main {
 
       // Run pipeline
       pipeline.run(ctx)(args.toList) match {
+        case (vReport: verification.VerificationReport, tReport: termination.TerminationReport) =>
+          ctx.reporter.info(vReport.summaryString)
+          ctx.reporter.info(tReport.summaryString)
+        
         case report: verification.VerificationReport =>
           ctx.reporter.info(report.summaryString)
 
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index e4f93fcfa25809c8d373a54abe6f442b6171ec0f..3e3c8a915b2084c5b6563028d9e5033639585833 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -15,3 +15,16 @@ abstract class Pipeline[-F, +T] {
 
   def run(ctx: LeonContext)(v: F): T
 }
+
+object Pipeline {
+  
+  def both[T, R1, R2](f1: Pipeline[T, R1], f2: Pipeline[T, R2]): Pipeline[T, (R1, R2)] = new Pipeline[T, (R1, R2)] {
+    def run(ctx : LeonContext)(t : T): (R1, R2) = {
+      val r1 = f1.run(ctx)(t)
+      // don't check for SharedOptions.optStrictPhases because f2 does not depend on the result of f1
+      val r2 = f2.run(ctx)(t)
+      (r1, r2)
+    }
+  }
+  
+}