don't store the tactic in the VC

src/main/scala/leon/verification/DefaultTactic.scala

@@ -16,7 +16,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
         case (Some(post), Some(body)) =>
           val vc = implies(precOrTrue(fd), application(post, Seq(body)))
 
-          Seq(VC(vc, fd, VCKinds.Postcondition, this).setPos(post))
+          Seq(VC(vc, fd, VCKinds.Postcondition).setPos(post))
         case _ =>
           Nil
       }
@@ -34,7 +34,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
               val pre2 = tfd.withParamSubst(args, pre)
               val vc = implies(and(precOrTrue(fd), path), pre2)
               val fiS = sizeLimit(fi.asString, 40)
-              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS"), this).setPos(fi)
+              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi)
           }
 
         case None =>
@@ -80,7 +80,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
             case ((e, kind, correctnessCond), path) =>
               val vc = implies(and(precOrTrue(fd), path), correctnessCond)
 
-              VC(vc, fd, kind, this).setPos(e)
+              VC(vc, fd, kind).setPos(e)
           }
 
         case None =>

src/main/scala/leon/verification/InductionTactic.scala

@@ -44,7 +44,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
             implies(andJoin(subCases), application(post, Seq(body)))
           )
 
-          VC(vc, fd, VCKinds.Info(VCKinds.Postcondition, s"ind. on ${arg.asString} / ${cct.classDef.id.asString}"), this).setPos(fd)
+          VC(vc, fd, VCKinds.Info(VCKinds.Postcondition, s"ind. on ${arg.asString} / ${cct.classDef.id.asString}")).setPos(fd)
         }
 
       case (body, _, post) =>
@@ -84,7 +84,7 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
           // Crop the call to display it properly
           val fiS = sizeLimit(fi.asString, 25)
 
-          VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS, ind. on (${arg.asString} : ${cct.classDef.id.asString})"), this).setPos(fi)
+          VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS, ind. on (${arg.asString} : ${cct.classDef.id.asString})")).setPos(fi)
         }
 
       case (body, _) =>

src/main/scala/leon/verification/VerificationCondition.scala

@@ -11,7 +11,7 @@ import leon.utils.Positioned
 import leon.solvers._
 
 /** This is just to hold some history information. */
-case class VC(condition: Expr, fd: FunDef, kind: VCKind, tactic: Tactic) extends Positioned {
+case class VC(condition: Expr, fd: FunDef, kind: VCKind) extends Positioned {
   override def toString = {
     fd.id.name +" - " +kind.toString
   }

src/main/scala/leon/xlang/FixReportLabels.scala

@@ -36,8 +36,7 @@ object FixReportLabels extends LeonPhase[VerificationReport, VerificationReport]
       val nvc = VC(
         vc.condition,
         fd,
-        vcKind,
-        vc.tactic
+        vcKind
       ).setPos(vc.getPos)
 
       nvc -> ovr