diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 1b022209415cb732a6860150955363c4b26dc1a6..eece54ca86528b26062fbfd6d42f0a2c2e7a5e2d 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -3,6 +3,8 @@
 package leon
 package purescala
 
+import utils.Simplifiers
+
 import leon.solvers._
 
 import scala.collection.concurrent.TrieMap
@@ -1805,7 +1807,7 @@ object TreeOps {
    *   if (..) { foo(b, a) } else { .. }
    * }
    **/
-  def flattenFunctions(fdOuter: FunDef): FunDef = {
+  def flattenFunctions(fdOuter: FunDef, ctx: LeonContext, p: Program): FunDef = {
     fdOuter.body match {
       case Some(LetDef(fdInner, FunctionInvocation(tfdInner2, args))) if fdInner == tfdInner2.fd =>
         val argsDef  = fdOuter.params.map(_.id)
@@ -1851,9 +1853,11 @@ object TreeOps {
 
           val newFd = fdOuter.duplicate
 
+          val simp = Simplifiers.bestEffort(ctx, p) _
+
           newFd.body          = fdInner.body.map(b => simplePreTransform(pre)(b))
-          newFd.precondition  = mergePre(fdOuter.precondition, fdInner.precondition)
-          newFd.postcondition = mergePost(fdOuter.postcondition, fdInner.postcondition)
+          newFd.precondition  = mergePre(fdOuter.precondition, fdInner.precondition).map(simp)
+          newFd.postcondition = mergePost(fdOuter.postcondition, fdInner.postcondition).map{ case (id, ex) => id -> simp(ex) }
 
           newFd
         } else {