diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 502563f0fe0a32546ded292141430af4be31779a..80f71fd87be7f27e1793e13fe38eb09b78f78d62 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -14,8 +14,6 @@ import purescala.Extractors._
 import purescala.Quantification._
 import solvers.{Model, HenkinModel}
 import solvers.SolverFactory
-import synthesis.ConversionPhase.convertHoles
-import leon.purescala.ExprOps
 
 abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int) extends Evaluator(ctx, prog) {
   val name = "evaluator"
@@ -123,11 +121,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
     case en@Ensuring(body, post) =>
       if ( exists{
         case Hole(_,_) => true
+        case WithOracle(_,_) => true
         case _ => false
-      }(en))
-        e(convertHoles(en, ctx))
-      else
+      }(en)) {
+        import synthesis.ConversionPhase.convert
+        e(convert(en, ctx))
+      } else {
         e(en.toAssert)
+      }
 
     case Error(tpe, desc) =>
       throw RuntimeError("Error reached in evaluation: " + desc)
diff --git a/src/main/scala/leon/synthesis/ConversionPhase.scala b/src/main/scala/leon/synthesis/ConversionPhase.scala
index bab77552bf1c6cfb8d3f151aed97c66bca6904ce..d76cff69b1a630718632f70e8684ff2426506cd2 100644
--- a/src/main/scala/leon/synthesis/ConversionPhase.scala
+++ b/src/main/scala/leon/synthesis/ConversionPhase.scala
@@ -78,7 +78,7 @@ object ConversionPhase extends UnitPhase[Program] {
    *
    */
 
-  def convertHoles(e : Expr, ctx : LeonContext) : Expr = {
+  def convert(e : Expr, ctx : LeonContext) : Expr = {
     val (pre, body, post) = breakDownSpecs(e)
 
     // Ensure that holes are not found in pre and/or post conditions
@@ -178,7 +178,7 @@ object ConversionPhase extends UnitPhase[Program] {
   def apply(ctx: LeonContext, pgm: Program): Unit = {
     // TODO: remove side-effects
     for (fd <- pgm.definedFunctions) {
-      fd.fullBody = convertHoles(fd.fullBody,ctx)
+      fd.fullBody = convert(fd.fullBody,ctx)
     }
   }