diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index a1cb99a49d9a53bfe0dd650d711b5f8b3b285012..3026068a141841162064e46d6e9c3a462837bb93 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -33,7 +33,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
             case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
               val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, pre)
               val vc = implies(and(precOrTrue(fd), path), pre2)
-              val fiS = exprToShortString(fi)
+              val fiS = sizeLimit(fi.toString, 40)
               VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS"), this).setPos(fi)
           }
 
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 4fc868f9ed244ceca45ea94d00686f2590a28776..bc26e77966b98bc819c84d30a166dc96b0e1ed4e 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -78,7 +78,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
               val vc = implies(and(CaseClassInstanceOf(cct, arg.toVariable), precOrTrue(fd), path), implies(andJoin(subCases), replace((tfd.params.map(_.toVariable) zip args).toMap, pre)))
 
               // Crop the call to display it properly
-              val fiS = exprToShortString(fi)
+              val fiS = sizeLimit(fi.toString, 25)
 
               VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "call $fiS, ind. on ($arg : ${cct.classDef.id)}"), this).setPos(fi)
             }
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index b424abf5f625a326409a5a7431a2d034648b9a54..b6cb7611728e2cbb5f1c92ec4aab18a7c291add0 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -31,10 +31,14 @@ abstract class Tactic(vctx: VerificationContext) {
     CollectorWithPaths(f).traverse(expr)
   }
 
-  protected def exprToShortString(e: Expr) = {
+  protected def sizeLimit(s: String, limit: Int) = {
+    require(limit > 3)
     // Crop the call to display it properly
-    val eS = e.toString
-    val s = eS.takeWhile(_ != '\n').take(35)
-    if (s == eS) s else s ++ " ..."
+    val res = s.takeWhile(_ != '\n').take(limit)
+    if (res == s) {
+      res
+    } else {
+      res + " ..."
+    }
   }
 }
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 495ab09f7bd17af26fb38f13b97f341c5142df56..0667ed67271b076df8ee7de496c9a1a038281798 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -23,16 +23,6 @@ case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
   lazy val totalInvalid: Int = vrs.count(_._2.isInvalid)
   lazy val totalUnknown: Int = vrs.count(_._2.isInconclusive)
 
-  def sizeLimit(str: String, limit: Int): String = {
-    require(limit > 3)
-    val res = str.takeWhile(_ != '\n').take(35)
-    if (res != str) {
-      res + "..."
-    } else {
-      str
-    }
-  }
-
   def summaryString : String = if(totalConditions >= 0) {
     import utils.ASCIIHelpers._
 
@@ -42,7 +32,7 @@ case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
       val timeStr = vr.timeMs.map(t => f"${t/1000d}%-3.3f").getOrElse("")
       Row(Seq(
         Cell(vc.fd.id.toString),
-        Cell(sizeLimit(vc.kind.name, 30)),
+        Cell(vc.kind.name),
         Cell(vc.getPos),
         Cell(vr.status),
         Cell(vr.solvedWith.map(_.name).getOrElse("")),