diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala index dfab2acc88c122f9654ab49b4862497b4de2c355..b429f0ed50ff82bedcee619fbea8cbd35917f9f7 100644 --- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala +++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala @@ -941,11 +941,14 @@ trait CodeExtraction extends ASTExtractors { NoTree(funDef.returnType) } - if (fctx.isExtern && !exists(_.isInstanceOf[NoTree])(finalBody)) { - reporter.warning(finalBody.getPos, "External function could be extracted as Leon tree: "+finalBody) - } + //if (fctx.isExtern && !exists(_.isInstanceOf[NoTree])(finalBody)) { + // reporter.warning(finalBody.getPos, "External function could be extracted as Leon tree: "+finalBody) + //} funDef.fullBody = finalBody + if(fctx.isExtern) { //extern never keeps the body, but we keep pre and post + funDef.body = None + } // Post-extraction sanity checks