diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index d92c65399765e7cac61c18f1668105321354131e..bf27ce8bd5105241226393468db3d3795f4322f9 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -15,6 +15,6 @@ class DefaultEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluat
   def initGC = new GlobalContext()
 
   case class DefaultRecContext(mappings: Map[Identifier, Expr]) extends RecContext {
-    def withVars(news: Map[Identifier, Expr]) = copy(news)
+    def newVars(news: Map[Identifier, Expr]) = copy(news)
   }
 }
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
index 7903f8c5eb99506eebd0b1407926a4d78ee593b5..b350aafc54e16779b021d99a8046d1ef11074806 100644
--- a/src/main/scala/leon/evaluators/DualEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -26,7 +26,7 @@ class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) exte
   val isCompiled = prog.definedFunctions.toSet
 
   case class DefaultRecContext(mappings: Map[Identifier, Expr], needJVMRef: Boolean = false) extends RecContext {
-    def withVars(news: Map[Identifier, Expr]) = copy(news)
+    def newVars(news: Map[Identifier, Expr]) = copy(news)
   }
 
   case class RawObject(o: AnyRef, tpe: TypeTree) extends Expr {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index a741602ddb99680026510a09647b9caea9728830..b62d2ffc58c0c7dbfd7a9ac53d8ef83de5db76c1 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -32,14 +32,14 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
   trait RecContext {
     def mappings: Map[Identifier, Expr]
 
-    def withVars(news: Map[Identifier, Expr]): RC;
+    def newVars(news: Map[Identifier, Expr]): RC;
 
     def withNewVar(id: Identifier, v: Expr): RC = {
-      withVars(mappings + (id -> v))
+      newVars(mappings + (id -> v))
     }
 
     def withNewVars(news: Map[Identifier, Expr]): RC = {
-      withVars(mappings ++ news)
+      newVars(mappings ++ news)
     }
   }
 
@@ -89,7 +89,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
         case Lambda(params, body) =>
           val newArgs = args.map(e)
           val mapping = (params.map(_.id) zip newArgs).toMap
-          e(body)(rctx.withVars(mapping), gctx)
+          e(body)(rctx.withNewVars(mapping), gctx)
         case f =>
           throw EvalError("Cannot apply non-lambda function " + f)
       }
@@ -149,7 +149,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
       val evArgs = args.map(a => e(a))
 
       // build a mapping for the function...
-      val frame = rctx.withVars((tfd.params.map(_.id) zip evArgs).toMap)
+      val frame = rctx.newVars((tfd.params.map(_.id) zip evArgs).toMap)
       
       if(tfd.hasPrecondition) {
         e(tfd.precondition.get)(frame, gctx) match {
diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index c95b5f716e52246fe638f41f5c9c8de5195d24d1..8321a9c5c7cc2543b860889cf978e654bc2005a7 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -21,7 +21,7 @@ class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) ex
   class TracingGlobalContext(var values: List[(Tree, Expr)]) extends GlobalContext
 
   case class TracingRecContext(mappings: Map[Identifier, Expr], tracingFrames: Int) extends RecContext {
-    def withVars(news: Map[Identifier, Expr]) = copy(mappings = news)
+    def newVars(news: Map[Identifier, Expr]) = copy(mappings = news)
   }
 
   override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = {
diff --git a/src/main/scala/leon/repair/RepairNDEvaluator.scala b/src/main/scala/leon/repair/RepairNDEvaluator.scala
index 054e20aa3c9abf6f6e6a485c730a3dd456bf1cb7..4dd78d134ad05c7006ddd806eac660be294b17ff 100644
--- a/src/main/scala/leon/repair/RepairNDEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairNDEvaluator.scala
@@ -26,7 +26,7 @@ class RepairNDEvaluator(ctx: LeonContext, prog: Program, fd : FunDef, cond: Expr
       val evArgs = args.map(a => e(a))
 
       // build a mapping for the function...
-      val frame = rctx.withVars((tfd.params.map(_.id) zip evArgs).toMap)
+      val frame = rctx.newVars((tfd.params.map(_.id) zip evArgs).toMap)
       
       if(tfd.hasPrecondition) {
         e(tfd.precondition.get)(frame, gctx) match {
@@ -76,4 +76,4 @@ class RepairNDEvaluator(ctx: LeonContext, prog: Program, fd : FunDef, cond: Expr
   
   
   
-}
\ No newline at end of file
+}
diff --git a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
index 5b8791f4700ad4224e25dcdb42785b6ed96cf0dd..791b7ec01804289780695f88b7136b078dc2fd71 100644
--- a/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
+++ b/src/main/scala/leon/repair/RepairTrackingEvaluator.scala
@@ -45,7 +45,7 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
   def fiStatus = fiStatus_.toMap.withDefaultValue(false)
   
   case class CollectingRecContext(mappings: Map[Identifier, Expr], lastFI : Option[FI]) extends RecContext {
-    def withVars(news: Map[Identifier, Expr]) = copy(news, lastFI)
+    def newVars(news: Map[Identifier, Expr]) = copy(news, lastFI)
     def withLastFI(fi : FI) = copy(lastFI = Some(fi))
   }
   
@@ -59,7 +59,7 @@ class RepairTrackingEvaluator(ctx: LeonContext, prog: Program) extends Recursive
       val evArgs = args.map(a => e(a))
       
       // build a mapping for the function...
-      val frameBlamingCaller = rctx.withVars((tfd.params.map(_.id) zip evArgs).toMap)
+      val frameBlamingCaller = rctx.newVars((tfd.params.map(_.id) zip evArgs).toMap)
       
       if(tfd.hasPrecondition) {
         e(tfd.precondition.get)(frameBlamingCaller, gctx) match {