diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 6a994e454975ba8b0b06cf8f80a92351f2c8ced7..84b1957b56615694992bbdbd8e588218876b8cb1 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -337,7 +337,7 @@ object ExprOps {
     rec(initBinders, e)
   }
 
-  /** Returns the set of identifiers in an expression */
+  /** Returns the set of free variables in an expression */
   def variablesOf(expr: Expr): Set[Identifier] = {
     import leon.xlang.Expressions.LetVar
     fold[Set[Identifier]] {
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index a00066ef1d4aca5f42ef3820d3fe133db074a7c3..6e90f0da4cf9de18af003d8bb04ffd0c2dd11500 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -14,7 +14,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
   def generatePostconditions(fd: FunDef): Seq[VC] = {
     (fd.postcondition, fd.body) match {
       case (Some(post), Some(body)) =>
-        val vc = implies(precOrTrue(fd), application(post, Seq(body)))
+        val vc = implies(fd.precOrTrue, application(post, Seq(body)))
         Seq(VC(vc, fd, VCKinds.Postcondition).setPos(post))
       case _ =>
         Nil
@@ -31,7 +31,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
         calls.map {
           case ((fi @ FunctionInvocation(tfd, args), pre), path) =>
             val pre2 = tfd.withParamSubst(args, pre)
-            val vc = implies(and(precOrTrue(fd), path), pre2)
+            val vc = implies(and(fd.precOrTrue, path), pre2)
             val fiS = sizeLimit(fi.asString, 40)
             VC(vc, fd, VCKinds.Info(VCKinds.Precondition, s"call $fiS")).setPos(fi)
         }
@@ -74,7 +74,7 @@ class DefaultTactic(vctx: VerificationContext) extends Tactic(vctx) {
 
       calls.map {
         case (e, correctnessCond) =>
-          val vc = implies(precOrTrue(fd), correctnessCond)
+          val vc = implies(fd.precOrTrue, correctnessCond)
 
           VC(vc, fd, eToVCKind(e)).setPos(e)
       }
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index 74b7b99af5de75d16eed02b93ecf081ddb9e93f6..65f96a090d4449845921252737bb35a3c3b9a327 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -35,12 +35,12 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
 
           val subCases = selectors.map { sel =>
             replace(Map(arg.toVariable -> sel),
-              implies(precOrTrue(fd), application(post, Seq(body)))
+              implies(fd.precOrTrue, application(post, Seq(body)))
             )
           }
 
           val vc = implies(
-            and(IsInstanceOf(arg.toVariable, cct), precOrTrue(fd)),
+            and(IsInstanceOf(arg.toVariable, cct), fd.precOrTrue),
             implies(andJoin(subCases), application(post, Seq(body)))
           )
 
@@ -72,12 +72,12 @@ class InductionTactic(vctx: VerificationContext) extends DefaultTactic(vctx) {
 
           val subCases = selectors.map { sel =>
             replace(Map(arg.toVariable -> sel),
-              implies(precOrTrue(fd), tfd.withParamSubst(args, pre))
+              implies(fd.precOrTrue, tfd.withParamSubst(args, pre))
             )
           }
 
           val vc = implies(
-            andJoin(Seq(IsInstanceOf(arg.toVariable, cct), precOrTrue(fd), path) ++ subCases),
+            andJoin(Seq(IsInstanceOf(arg.toVariable, cct), fd.precOrTrue, path) ++ subCases),
             tfd.withParamSubst(args, pre)
           )
 
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 98af8cde056833cc316829d8b4319269696769f7..8f539708da8f9f4071a1843d8d711c55215ed344 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -21,12 +21,6 @@ abstract class Tactic(vctx: VerificationContext) {
   def generatePreconditions(function: FunDef): Seq[VC]
   def generateCorrectnessConditions(function: FunDef): Seq[VC]
 
-  // Helper functions
-  protected def precOrTrue(fd: FunDef): Expr = fd.precondition match {
-    case Some(pre) => pre
-    case None => BooleanLiteral(true)
-  }
-
   protected def sizeLimit(s: String, limit: Int) = {
     require(limit > 3)
     // Crop the call to display it properly