Fix info being too large in precondition.

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

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

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

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("")),