diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index a0ed2936a5f9c27e525fef16a08b772a05e4d427..47b14d99bb9b175965efb088053a5cbd74c3221b 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -22,9 +22,9 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
       evaluator.eval(functionInvocation(fd, ts.ins))
     }
 
-    val outInfo = (invalids.collect {
+    val outInfo = invalids.collect {
       case InOutExample(ins, outs) => ins -> outs
-    }).toMap
+    }.toMap
 
     val callGraph = evaluator.fullCallGraph
 
@@ -50,15 +50,15 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
 
   def union(that: ExamplesBank) = {
     ExamplesBank(
-      distinctIns((this.valids union that.valids)),
-      distinctIns((this.invalids union that.invalids))
+      distinctIns(this.valids union that.valids),
+      distinctIns(this.invalids union that.invalids)
     )
   }
 
   private def distinctIns(s: Seq[Example]): Seq[Example] = {
-    val insOuts = (s.collect {
+    val insOuts = s.collect {
       case InOutExample(ins, outs) => ins -> outs
-    }).toMap
+    }.toMap
 
     s.map(_.ins).distinct.map {
       case ins =>
diff --git a/src/main/scala/leon/termination/ProcessingPipeline.scala b/src/main/scala/leon/termination/ProcessingPipeline.scala
index 0dbdb9bd0523d5eaeb8831bbf9fc62d7cb3a7359..6e7da22ced93354dace7319a0dea0c4613c440f0 100644
--- a/src/main/scala/leon/termination/ProcessingPipeline.scala
+++ b/src/main/scala/leon/termination/ProcessingPipeline.scala
@@ -213,5 +213,3 @@ abstract class ProcessingPipeline(context: LeonContext, initProgram: Program) ex
     }
   }
 }
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index a9f7ef77b616a8a08e0b438a162b385135deee50..fbfcde51ea4c1f503313707e7132a6f38cd24c30 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -30,6 +30,6 @@ object TerminationPhase extends LeonPhase[Program,TerminationReport] {
     }
     val endTime = System.currentTimeMillis
 
-    new TerminationReport(results, (endTime - startTime).toDouble / 1000.0d)
+    new TerminationReport(ctx, results, (endTime - startTime).toDouble / 1000.0d)
   }
 }
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index f9dbb49a7e3498d5c507b71c9e44c6890d446b7d..57c3c03aebc3f0543cad09e84352106867c178c6 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -4,28 +4,38 @@ package leon
 package termination
 
 import purescala.Definitions._
+import utils.ASCIIHelpers._
+
+case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) {
 
-case class TerminationReport(results : Seq[(FunDef,TerminationGuarantee)], time : Double) {
   def summaryString : String = {
-    val sb = new StringBuilder
-    sb.append("─────────────────────\n")
-    sb.append(" Termination summary \n")
-    sb.append("─────────────────────\n\n")
-    for((fd,g) <- results) {
-      val result = if (g.isGuaranteed) "\u2713" else "\u2717"
-      val toPrint = g match {
-        case LoopsGivenInputs(reason, args) =>
-          "Non-terminating for call: " + args.mkString(fd.id+"(", ",", ")")
-        case CallsNonTerminating(funDefs) =>
-          "Calls non-terminating functions " + funDefs.map(_.id).mkString(",")
-        case Terminates(reason) =>
-          "Terminates (" + reason + ")"
-        case _ => g.toString
+    var t = Table("Termination summary")
+
+    for ((fd, g) <- results) t += Row(Seq(
+      Cell(fd.id.asString(ctx)),
+      Cell {
+        val result = if (g.isGuaranteed) "\u2713" else "\u2717"
+        val verdict = g match {
+          case LoopsGivenInputs(reason, args) =>
+            "Non-terminating for call: " + args.mkString(fd.id + "(", ",", ")")
+          case CallsNonTerminating(funDefs) =>
+            "Calls non-terminating functions " + funDefs.map(_.id).mkString(",")
+          case Terminates(reason) =>
+            "Terminates (" + reason + ")"
+          case _ => g.toString
+        }
+        s"$result $verdict"
       }
-      sb.append(f"- ${fd.id.name}%-30s $result $toPrint%-30s\n")
-    }
-    sb.append(f"\n[Analysis time: $time%7.3f]\n")
-    sb.toString
+    ))
+
+    t += Separator
+
+    t += Row(Seq(Cell(
+      f"Analysis time: $time%7.3f",
+      spanning = 2
+    )))
+
+    t.render
   }
 
   def evaluationString : String = {
diff --git a/src/main/scala/leon/utils/ASCIIHelpers.scala b/src/main/scala/leon/utils/ASCIIHelpers.scala
index 4cf63fe2235e59e061d37ebed7f7d5341eab9af1..a2750e42340356f890b6f4822ba3d2f2d3f42643 100644
--- a/src/main/scala/leon/utils/ASCIIHelpers.scala
+++ b/src/main/scala/leon/utils/ASCIIHelpers.scala
@@ -8,7 +8,7 @@ object ASCIIHelpers {
     def ++(rs: Iterable[TableRow]): Table = copy(rows = rows ++ rs)
 
 
-    def computeColumnSizes = {
+    private def computeColumnSizes = {
       // First check constraints
       var constraints = Map[(Int, Int), Int]()
 
@@ -121,7 +121,6 @@ object ASCIIHelpers {
   case object Left extends Alignment
   case object Right extends Alignment
 
-
   case class Cell(v: Any, spanning: Int = 1, align: Alignment = Left) {
     require(spanning >= 1)
 
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 43f6aacb8fdb6c5ffc62407af889babed02b175e..18ae32c8952eea57c46dfeb5698bd2a62430646d 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -3,12 +3,9 @@
 package leon
 package verification
 
-import VCKinds._
-import VCStatus._
+import purescala.Definitions.Program
 
-import purescala.Definitions.{FunDef, Program}
-
-case class VerificationReport(val program: Program, val results: Map[VC, Option[VCResult]]) {
+case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {
 
   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))