diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 0571e324220f036b220758cfedf6b864f49b1601..b424abf5f625a326409a5a7431a2d034648b9a54 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -10,8 +10,7 @@ import purescala.ExprOps._
 abstract class Tactic(vctx: VerificationContext) {
   val description : String
 
-  def generateVCs(fdUnsafe: FunDef): Seq[VC] = {
-    val fd = fdUnsafe.duplicate
+  def generateVCs(fd: FunDef): Seq[VC] = {
     fd.fullBody = matchToIfThenElse(fd.fullBody)
     generatePostconditions(fd) ++
     generatePreconditions(fd) ++