Crop preconditions when printing

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 =>

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)
             }
         }
 

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 ++ " ..."
+  }
 }