diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index a4cb128314921e8607eca9ca5b819cccb636d4d8..c308c5e347e859bc192833bf015e4c2013dc26b9 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -25,7 +25,7 @@ abstract class Evaluator(val context: LeonContext, val program: Program) extends
   /** Evaluates an expression given a simple model (assumes expr is quantifier-free).
     * Mainly useful for compatibility reasons.
     */
-  final def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = eval(expr, new Model(mapping))
+  def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = eval(expr, new Model(mapping))
 
   /** Evaluates a ground expression. */
   final def eval(expr: Expr) : EvaluationResult = eval(expr, Model.empty)
@@ -48,14 +48,14 @@ trait DeterministicEvaluator extends Evaluator {
   type Value = Expr
   
   /**Evaluates the environment first, resolving non-cyclic dependencies, and then evaluate the expression */
-  final def evalEnvExpr(expr: Expr, mapping: Iterable[(Identifier, Expr)]) : EvaluationResult = {
+  override def eval(expr: Expr, mapping: Map[Identifier, Expr]) : EvaluationResult = {
     if(mapping.forall{ case (key, value) => purescala.ExprOps.isValue(value) }) {
-      eval(expr, mapping.toMap)
+      super.eval(expr, mapping.toMap)
     } else (_evalEnv(mapping) match {
-      case Left(m) => eval(expr, m)
+      case Left(m) => super.eval(expr, m)
       case Right(errorMessage) => 
         val m = mapping.filter{ case (k, v) => purescala.ExprOps.isValue(v) }.toMap
-        eval(expr, m) match {
+        super.eval(expr, m) match {
           case res @ evaluators.EvaluationResults.Successful(result) => res
           case _ => evaluators.EvaluationResults.EvaluatorError(errorMessage)
         }
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index bdeff625545a1081700de01c57d0f317e0411d2d..a881953bb9354472703660cae8bacbb542e67596 100644
--- a/src/main/scala/leon/repair/rules/Focus.scala
+++ b/src/main/scala/leon/repair/rules/Focus.scala
@@ -66,7 +66,7 @@ case object Focus extends PreprocessingRule("Focus") {
 
     def existsFailing(e: Expr, env: Map[Identifier, Expr], evaluator: DeterministicEvaluator): Boolean = {
       p.eb.invalids.exists { ex =>
-        evaluator.evalEnvExpr(e, (p.as zip ex.ins).toMap ++ env).result match {
+        evaluator.eval(e, (p.as zip ex.ins).toMap ++ env).result match {
           case Some(BooleanLiteral(b)) => b
           case _ => true
         }
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 92664547e33e73ccce08544a235249b5c0856d0a..6cababe398c6159ec4e5cce721b795a751825bda 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -184,7 +184,7 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
   /** Filter inputs through expr which is an expression evaluating to a boolean */
   def filterIns(expr: Expr): QualifiedExamplesBank = {
     filterIns(m =>
-      hctx.defaultEvaluator.evalEnvExpr(expr, m)
+      hctx.defaultEvaluator.eval(expr, m)
       .result == Some(BooleanLiteral(true)))
   }
 
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 6100c8c3c6bad2b4554c1ab9eac9667894812ca2..52756108c029ff7fcad5d0f2a0e6aaceb3d6770c 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -107,7 +107,7 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
           ((p.as zip i.ins).toMap, p.pc.toClause)
       }
 
-      evaluator.evalEnvExpr(cond, mapping) match {
+      evaluator.eval(cond, mapping) match {
         case EvaluationResults.Successful(BooleanLiteral(true)) => true
         case _ => false
       }
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index e4e5192bc96b99bcfb2f28272665329ffc37a612..933ae752b19eff0ff816718ef7e6c4ee79560f22 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -453,11 +453,11 @@ abstract class CEGISLike(name: String) extends Rule(name) {
         timers.testForProgram.start()
         val res = ex match {
           case InExample(ins) =>
-            evaluator.evalEnvExpr(cnstr, p.as.zip(ins).toMap ++ p.pc.bindings)
+            evaluator.eval(cnstr, p.as.zip(ins).toMap ++ p.pc.bindings)
 
           case InOutExample(ins, outs) =>
             val eq = equality(innerSol, tupleWrap(outs))
-            evaluator.evalEnvExpr(eq, p.as.zip(ins).toMap ++ p.pc.bindings)
+            evaluator.eval(eq, p.as.zip(ins).toMap ++ p.pc.bindings)
         }
         timers.testForProgram.stop()
 
diff --git a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
index ba3cb368510f2fd79c811766c57f55d71d1c4d71..4463e6818b2b7b102cf404bd80ca794d9b96c3c7 100644
--- a/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
+++ b/src/main/scala/leon/synthesis/rules/IntroduceRecCalls.scala
@@ -67,7 +67,7 @@ case object IntroduceRecCalls extends NormalizingRule("Introduce rec. calls") {
 
         val evaluator = new NoChooseEvaluator(hctx, hctx.program)
         def mapExample(ex: Example): List[Example] = {
-          val results = calls map (evaluator.evalEnvExpr(_, p.as.zip(ex.ins)).result)
+          val results = calls map (evaluator.eval(_, p.as.zip(ex.ins).toMap).result)
           if (results forall (_.isDefined)) List({
             val extra = results map (_.get)
             ex match {