diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index bba6f4fa2789e75cbabfff59b2bab6ed2ccd65cc..616f3420d686569e6cbfe4485b399d0d7823129d 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/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 =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 878b902cea86d8896ae608dc6452573541a6f860..9e06e4abd0fb88c8c0db782f27880390e814d34f 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/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, _) =>
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index ba23961e3cd8e3eaa37d9f581c35b0df5d91b646..8ddbf97abfb7c28c2aafaef446c7c0bed422ffe5 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/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
   }
diff --git a/src/main/scala/leon/xlang/FixReportLabels.scala b/src/main/scala/leon/xlang/FixReportLabels.scala
index 91eabf9c3c30f1103067c18d5026ae49c16f5532..614057b3bbbc99b7edf8fe2b8af3c3578ff47ea1 100644
--- a/src/main/scala/leon/xlang/FixReportLabels.scala
+++ b/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