diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index c924e8bb5c7b188580dffdd1e4a34038bf20a383..a4cb128314921e8607eca9ca5b819cccb636d4d8 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -75,8 +75,9 @@ trait DeterministicEvaluator extends Evaluator {
   /** From a not yet well evaluated context with dependencies between variables, returns a head where all exprs are values (as a Left())
    *  If this does not succeed, it provides an error message as Right()*/
   private def _evalEnv(mapping: Iterable[(Identifier, Expr)]): Either[Map[Identifier, Value], String] = {
-    var f= mapping.toSet
-    var mBuilder = collection.mutable.ListBuffer[(Identifier, Value)]()
+    val (evaled, nonevaled) = mapping.partition{ case (id, expr) => purescala.ExprOps.isValue(expr)}
+    var f= nonevaled.toSet
+    var mBuilder = collection.mutable.ListBuffer[(Identifier, Value)]() ++= evaled
     var changed = true
     while(f.nonEmpty && changed) {
       changed = false
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 1828709efa5b42a49630039dd20ef5415e9bf626..f3a9a94caaabf7e5d2c104439f041de680c54f53 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -2177,6 +2177,7 @@ object ExprOps extends GenTreeOps[Expr] {
       case (FiniteLambda(mapping, default, tpe), exTpe@FunctionType(ins, out)) =>
         tpe == exTpe
       case (Lambda(valdefs, body), FunctionType(ins, out)) =>
+        variablesOf(e).isEmpty &&
         (valdefs zip ins forall (vdin => (vdin._1.getType == vdin._2) < s"${vdin._1.getType} is not equal to ${vdin._2}")) &&
         (body.getType == out) < s"${body.getType} is not equal to ${out}"
       case (FiniteBag(elements, fbtpe), BagType(tpe)) =>
diff --git a/src/main/scala/leon/repair/rules/Focus.scala b/src/main/scala/leon/repair/rules/Focus.scala
index cd0da333bcfd1882d3360fd769e6f7f49584eef0..1645b7bccd8c892b855f8b06c2bb42f5cbfd84a6 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, env).result match {
+        evaluator.evalEnvExpr(e, (p.as zip ex.ins).toMap ++ env) match {
           case Some(BooleanLiteral(b)) => b
           case _ => true
         }