diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 7a8056c6a9492c723a81b6ef1854f4a564816d7e..292af0cf81a417477e53ed029e3455e7b050e35e 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -391,6 +391,7 @@ object Definitions {
     def precondition_=(oe: Option[Expr]) = {
       fullBody = withPrecondition(fullBody, oe) 
     }
+    def precOrTrue = precondition getOrElse BooleanLiteral(true)
 
     def postcondition = postconditionOf(fullBody)
     def postcondition_=(op: Option[Expr]) = {
@@ -532,6 +533,7 @@ object Definitions {
     def fullBody      = cached(fd.fullBody)
     def body          = fd.body map cached
     def precondition  = fd.precondition map cached
+    def precOrTrue    = cached(fd.precOrTrue)
     def postcondition = fd.postcondition map cached
 
     def hasImplementation = body.isDefined
diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 607e9aeb4ccd079199bb3d97e9d495a19d6c7b67..7f76beff85796ec47d8ff5a49e4613c752c9ac41 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -82,7 +82,7 @@ class FunctionClosure extends TransformationPhase {
       }
       newFunDef.postcondition = freshPostcondition
       
-      pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
+      pathConstraints = fd.precOrTrue :: pathConstraints
       val freshBody = fd.body.map(body => introduceLets(body, fd2FreshFd + (fd -> ((newFunDef, extraValDefOldIds.map(_.toVariable))))))
       newFunDef.body = freshBody
       pathConstraints = pathConstraints.tail
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index f94272e9b0923aa493681ed320f07b8a1a2005ee..25b58c1dcaeb64a0d874d7a9b26e76749021594d 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -175,7 +175,7 @@ object MethodLifting extends TransformationPhase {
           // Add precondition if the method was defined in a subclass
           val pre = and(
             classPre(fd),
-            nfd.precondition.getOrElse(BooleanLiteral(true))
+            nfd.precOrTrue
           )
           nfd.fullBody = withPrecondition(nfd.fullBody, Some(pre))
         
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index d38af251c0faadd29fcd5b7bd48f7bea21fa2691..47dc7abac071490e5d9408512413c80d23050185 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -137,7 +137,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
 
     val term  = Terminating(fd.typed, fd.params.map(_.id.toVariable))
     val guide = Guide(origBody)
-    val pre   = fd.precondition.getOrElse(BooleanLiteral(true))
+    val pre   = fd.precOrTrue
 
     val ci = ChooseInfo(
       fd,
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index a7215bc97889cd7b2cc448d7358aa6e5fba3ae9f..b882bafe2fd9a9e82b3d56dd987b16a717fd7e5f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -47,7 +47,7 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target with SMTLIBQuantifiedT
 
         val specAssert = tfd.postcondition map { post =>
           val term = implies(
-            tfd.precondition getOrElse BooleanLiteral(true),
+            tfd.precOrTrue,
             application(post, Seq(FunctionInvocation(tfd, Seq())))
           )
           SMTAssert(toSMT(term)(Map()))
@@ -99,7 +99,7 @@ trait SMTLIBCVC4QuantifiedTarget extends SMTLIBCVC4Target with SMTLIBQuantifiedT
         post <- tfd.postcondition
       } {
         val term = implies(
-          tfd.precondition getOrElse BooleanLiteral(true),
+          tfd.precOrTrue,
           application(post, Seq(tfd.applied))
         )
         try {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
index 0de742f5e01e7125a4d25740012df3b86c975ca3..7aa281b677f13b65df6008508575f8dfb7a0c9e7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBQuantifiedTarget.scala
@@ -40,8 +40,8 @@ trait SMTLIBQuantifiedTarget extends SMTLIBTarget {
           Seq(fi)
         )
       } getOrElse BooleanLiteral(true)
-      val pre = tfd.precondition getOrElse BooleanLiteral(true)
-      and(pre, post)
+
+      and(tfd.precOrTrue, post)
     }
 
     // We want to check if the negation of the vc is sat under inductive hyp.
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
index 6c20b337d732a0d5d7a4de6e7fe221fb430beaa0..0735b2396ba7f5b8b64cbe87fc8850a71d74da7e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedTarget.scala
@@ -59,7 +59,7 @@ trait SMTLIBZ3QuantifiedTarget extends SMTLIBZ3Target with SMTLIBQuantifiedTarge
       post <- tfd.postcondition
     } {
       val term = implies(
-        tfd.precondition getOrElse BooleanLiteral(true),
+        tfd.precOrTrue,
         application(post, Seq(tfd.applied))
       )
       try {
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index cd67adf98d97e0addc052f62e603792fddb10ee7..5e36c593b12f7df74575ad634b0683991245cbb5 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -42,7 +42,7 @@ object ChooseInfo {
 
   def extractFromFunction(ctx: LeonContext, prog: Program, fd: FunDef): Seq[ChooseInfo] = {
 
-    val actualBody = and(fd.precondition.getOrElse(BooleanLiteral(true)), fd.body.get)
+    val actualBody = and(fd.precOrTrue, fd.body.get)
     val term = Terminating(fd.typed, fd.params.map(_.id.toVariable))
 
     val eFinder = new ExamplesFinder(ctx, prog)
diff --git a/src/main/scala/leon/termination/Strengthener.scala b/src/main/scala/leon/termination/Strengthener.scala
index dc3d0818830accf356fdfc93853df45f0d8e1198..e6c53a472da1f5d997f9eb8fde61892c16863b12 100644
--- a/src/main/scala/leon/termination/Strengthener.scala
+++ b/src/main/scala/leon/termination/Strengthener.scala
@@ -35,7 +35,7 @@ trait Strengthener { self : RelationComparator =>
 
         funDef.postcondition = Some(postcondition)
 
-        val prec = matchToIfThenElse(funDef.precondition.getOrElse(BooleanLiteral(true)))
+        val prec = matchToIfThenElse(funDef.precOrTrue)
         val body = matchToIfThenElse(funDef.body.get)
         val post = matchToIfThenElse(postcondition)
         val formula = implies(prec, application(post, Seq(body)))