diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 62e4f9f9dab420e65abbb59a3e8c9845f82cedad..b98224402ed252b9801b11d846f4aa4dea039fd6 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -59,10 +59,12 @@ object CodeGeneration {
   def compileFunDef(funDef : FunDef, ch : CodeHandler)(implicit env : CompilationEnvironment) {
     val newMapping = funDef.args.map(_.id).zipWithIndex.toMap
 
+    val body = funDef.body.getOrElse(throw CompilationException("Can't compile a FunDef without body"))
+
     val bodyWithPre = if(funDef.hasPrecondition && env.compileContracts) {
-      IfExpr(funDef.precondition.get, funDef.getBody, Error("Precondition failed"))
+      IfExpr(funDef.precondition.get, body, Error("Precondition failed"))
     } else {
-      funDef.getBody
+      body
     }
 
     val bodyWithPost = if(funDef.hasPostcondition && env.compileContracts) {
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 93a51b9f5665457568276472e404d5c97adef482..f1f3311becb8249fa2b5180569f3d9c22e9e3099 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -326,11 +326,6 @@ object Definitions {
     def hasPrecondition : Boolean = precondition.isDefined
     def hasPostcondition : Boolean = postcondition.isDefined
 
-    def getImplementation : Expr = body.get
-    def getBody : Expr = body.get
-    def getPrecondition : Expr = precondition.get
-    def getPostcondition : Expr = postcondition.get
-
     def allIdentifiers : Set[Identifier] = {
       args.map(_.id).toSet ++
       body.map(TreeOps.allIdentifiers(_)).getOrElse(Set[Identifier]()) ++
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 32e919992f42c6978d843d8a5990ad27a79c0f87..6c5e64b19eeb9df3a063698df21716ce0ab4436e 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -343,19 +343,21 @@ object FunctionTemplate {
     }
 
     // Now the postcondition.
-    if (funDef.hasPostcondition) {
-      val post0 : Expr = matchToIfThenElse(funDef.getPostcondition)
-      val post : Expr = replace(Map(ResultVariable() -> invocation), post0)
+    funDef.postcondition match {
+      case Some(post) =>
+        val newPost : Expr = replace(Map(ResultVariable() -> invocation), matchToIfThenElse(post))
 
-      val postHolds : Expr =
-        if(funDef.hasPrecondition) {
-          Implies(prec.get, post)
-        } else {
-          post
-        }
+        val postHolds : Expr =
+          if(funDef.hasPrecondition) {
+            Implies(prec.get, newPost)
+          } else {
+            newPost
+          }
+
+        val finalPred2 : Expr = rec(activatingBool,  postHolds)
+        storeGuarded(activatingBool, finalPred2)
+      case None =>
 
-      val finalPred2 : Expr = rec(activatingBool,  postHolds)
-      storeGuarded(activatingBool, finalPred2)
     }
 
     new FunctionTemplate(solver, funDef, activatingBool, Set(condVars.toSeq : _*), Set(exprVars.toSeq : _*), Map(guardedExprs.toSeq : _*),
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index e68aa363801fbd3bf4a1b0f03bc65f20f903c800..a9054aea47ada170e721a268c6b0e7bc5ae0aacd 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -238,10 +238,13 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
       }
       case LetDef(fd, b) => {
         //Recall that here the nested function should not access mutable variables from an outside scope
-        val newFd = if(!fd.hasImplementation) fd else {
-          val (fdRes, fdScope, fdFun) = toFunction(fd.getBody)
-          fd.body = Some(fdScope(fdRes))
-          fd
+        val newFd = fd.body match {
+          case Some(b) =>
+            val (fdRes, fdScope, fdFun) = toFunction(b)
+            fd.body = Some(fdScope(fdRes))
+            fd
+          case None =>
+            fd
         }
         val (bodyRes, bodyScope, bodyFun) = toFunction(b)
         (bodyRes, (b2: Expr) => LetDef(newFd, bodyScope(b2)), bodyFun)