diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index 415f4edaa8b63edd319a696c7dc9042e75692cda..a1cb99a49d9a53bfe0dd650d711b5f8b3b285012 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -33,8 +33,8 @@ 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)
-
-              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fi"), this).setPos(fi)
+              val fiS = exprToShortString(fi)
+              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS"), this).setPos(fi)
           }
 
         case None =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 27facb188510ab35f465530ef8b4986120a7bfbd..4fc868f9ed244ceca45ea94d00686f2590a28776 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -77,7 +77,10 @@ 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)))
 
-              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "call $fi, ind. on $arg / ${cct.classDef.id}"), this).setPos(fi)
+              // Crop the call to display it properly
+              val fiS = exprToShortString(fi)
+
+              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 7462818fbbcc4beda259d492c3d98b853fd0e799..0571e324220f036b220758cfedf6b864f49b1601 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -31,4 +31,11 @@ abstract class Tactic(vctx: VerificationContext) {
   protected def collectWithPC[T](f: PartialFunction[Expr, T])(expr: Expr): Seq[(T, Expr)] = {
     CollectorWithPaths(f).traverse(expr)
   }
+
+  protected def exprToShortString(e: Expr) = {
+    // Crop the call to display it properly
+    val eS = e.toString
+    val s = eS.takeWhile(_ != '\n').take(35)
+    if (s == eS) s else s ++ " ..."
+  }
 }