diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index dd14587760b046d2deb6ccbd7f6a62f0fb398951..70d8091b2df531781e6816557eaadd7331827837 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -34,7 +34,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
               val pre2 = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, pre)
               val vc = implies(and(precOrTrue(fd), path), pre2)
 
-              VC(vc, fd, VCKinds.Precondition, this).setPos(fi)
+              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fi"), this).setPos(fi)
           }
 
         case None =>
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index efd77f8766f78596380b40b6c8efa47cb3bb7e33..27facb188510ab35f465530ef8b4986120a7bfbd 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -77,7 +77,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)))
 
-              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "ind. on $arg / ${cct.classDef.id}"), this).setPos(fi)
+              VC(vc, fd, VCKinds.Info(VCKinds.Precondition, "call $fi, ind. on $arg / ${cct.classDef.id}"), this).setPos(fi)
             }
         }