Remove pre-processing phase during evaluation (what?)

src/main/scala/leon/evaluators/RecursiveEvaluator.scala

@@ -77,16 +77,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
       e(IfExpr(Not(cond), Error(expr.getType, oerr.getOrElse("Assertion failed @"+expr.getPos)), body))
 
     case en@Ensuring(body, post) =>
-      if ( exists{
-        case Hole(_,_) => true
-        case WithOracle(_,_) => true
-        case _ => false
-      }(en)) {
-        import synthesis.ConversionPhase.convert
-        e(convert(en, ctx))
-      } else {
-        e(en.toAssert)
-      }
+      e(en.toAssert)
 
     case Error(tpe, desc) =>
       throw RuntimeError("Error reached in evaluation: " + desc)

src/main/scala/leon/evaluators/StreamEvaluator.scala

@@ -58,16 +58,7 @@ class StreamEvaluator(ctx: LeonContext, prog: Program)
       e(IfExpr(Not(cond), Error(expr.getType, oerr.getOrElse("Assertion failed @"+expr.getPos)), body))
 
     case en@Ensuring(body, post) =>
-      if ( exists{
-        case Hole(_,_) => true
-        case WithOracle(_,_) => true
-        case _ => false
-      }(en)) {
-        import synthesis.ConversionPhase.convert
-        e(convert(en, ctx))
-      } else {
-        e(en.toAssert)
-      }
+      e(en.toAssert)
 
     case Error(tpe, desc) =>
       Stream()

src/main/scala/leon/synthesis/ConversionPhase.scala

@@ -60,7 +60,7 @@ object ConversionPhase extends UnitPhase[Program] {
    *   post(res)
    * }
    *
-   * 3) Completes abstract definitions:
+   * 3) Completes abstract definitions (IF NOT EXTERN):
    *
    *  def foo(a: T) = {
    *    require(..a..)
@@ -92,7 +92,7 @@ object ConversionPhase extends UnitPhase[Program] {
    * (in practice, there will be no pre-and postcondition)
    */
 
-  def convert(e : Expr, ctx : LeonContext) : Expr = {
+  def convert(e : Expr, ctx : LeonContext, isExtern: Boolean) : Expr = {
     val (pre, body, post) = breakDownSpecs(e)
 
     // Ensure that holes are not found in pre and/or post conditions
@@ -183,8 +183,12 @@ object ConversionPhase extends UnitPhase[Program] {
         }
 
       case None =>
-        val newPost = post getOrElse Lambda(Seq(ValDef(FreshIdentifier("res", e.getType))), BooleanLiteral(true))
-        withPrecondition(Choose(newPost), pre)
+        if (isExtern) {
+          e
+        } else {
+          val newPost = post getOrElse Lambda(Seq(ValDef(FreshIdentifier("res", e.getType))), BooleanLiteral(true))
+          withPrecondition(Choose(newPost), pre)
+      }
     }
 
     // extract spec from chooses at the top-level
@@ -202,7 +206,7 @@ object ConversionPhase extends UnitPhase[Program] {
   def apply(ctx: LeonContext, pgm: Program): Unit = {
     // TODO: remove side-effects
     for (fd <- pgm.definedFunctions) {
-      fd.fullBody = convert(fd.fullBody,ctx)
+      fd.fullBody = convert(fd.fullBody, ctx, fd.annotations("extern"))
     }
   }