diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index d5b07f276264c548e9b31a295ca1efdd101e0871..a7802c490efb494f419e8158439d3c8dbe848f3f 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -30,6 +30,6 @@ object TerminationPhase extends SimpleLeonPhase[Program, TerminationReport] {
     }
     val endTime = System.currentTimeMillis
 
-    new TerminationReport(ctx, results, (endTime - startTime).toDouble / 1000.0d)
+    new TerminationReport(ctx, tc.program, 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 c7fc3a0b3d7a870b7730022da35e7c3fa3f7483d..47ef92268834a47ab584720f7169989def23531b 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -6,8 +6,10 @@ package termination
 import purescala.Definitions._
 import utils.Report
 import utils.ASCIIHelpers._
+import leon.purescala.PrettyPrinter
+import leon.purescala.SelfPrettyPrinter
 
-case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
+case class TerminationReport(ctx: LeonContext, program: Program, results : Seq[(FunDef,TerminationGuarantee)], time : Double) extends Report {
 
   def summaryString : String = {
     var t = Table("Termination summary")
@@ -18,7 +20,10 @@ case class TerminationReport(ctx: LeonContext, results : Seq[(FunDef,Termination
         val result = if (g.isGuaranteed) "\u2713" else "\u2717"
         val verdict = g match {
           case LoopsGivenInputs(reason, args) =>
-            "Non-terminating for call: " + args.mkString(fd.id + "(", ",", ")")
+            val niceArgs = args.map { v =>
+              SelfPrettyPrinter.print(v, PrettyPrinter(v))(ctx, program)
+            }
+            "Non-terminating for call: " + niceArgs.mkString(fd.id + "(", ",", ")")
           case CallsNonTerminating(funDefs) =>
             "Calls non-terminating functions " + funDefs.map(_.id).mkString(",")
           case Terminates(reason) =>