diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index 5ab872b84d9d495ddec840889c98d2a10222c44f..4d77d89dd578604ab10f322997118436ac83810d 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -30,6 +30,8 @@ object EpsilonElimination extends UnitPhase[Program] {
           }.toMap ++ Seq((epsilonVar, Variable(resId)))
           val postcondition = replace(eMap, pred)
           newFunDef.postcondition = Some(Lambda(Seq(ValDef(resId)), postcondition))
+          newFunDef.addFlags(fd.flags)
+          newFunDef.addFlag(Annotation("extern", Seq()))
           LetDef(Seq(newFunDef), FunctionInvocation(newFunDef.typed, bSeq map Variable))
 
         case (other, _) => other