diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 172281235e2c40aef6583c64156f991d90a6c6d3..a180b1f168f1f0b304ded85491f2a4e8bdd4f31b 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -52,6 +52,7 @@ object FunctionClosure extends Pass {
       val newFunDef = new FunDef(newFunId, rt, newVarDecls).setPosInfo(fd)
       newFunDef.fromLoop = fd.fromLoop
       newFunDef.parent = fd.parent
+      newFunDef.addAnnotation(fd.annotations.toSeq:_*)
 
       val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
       val freshPostcondition = postcondition.map(expr => replace(freshVarsExpr, expr))
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index 2f5f1bc53fc000242758f19aee766cf175dadf84..2c5d4d5a532614873b9b6786481e82f0ebd4a3de 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -24,6 +24,7 @@ object UnitElimination extends Pass {
         freshFunDef.parent = fd.parent
         freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
         freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
+        freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
         fun2FreshFun += (fd -> freshFunDef)
       } else {
         fun2FreshFun += (fd -> fd) //this will make the next step simpler
@@ -97,6 +98,9 @@ object UnitElimination extends Pass {
         else {
           val (newFd, rest) = if(fd.args.exists(vd => vd.tpe == UnitType)) {
             val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
+            freshFunDef.addAnnotation(fd.annotations.toSeq:_*)
+            freshFunDef.parent = fd.parent
+            freshFunDef.fromLoop = fd.fromLoop
             freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
             freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
             fun2FreshFun += (fd -> freshFunDef)