diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 2274336b9d7a332d760312d2c7a0c380c9d15119..18dbe6ced2b5ca160b69bd61d762a45d8c1d7062 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -71,8 +71,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
   def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
     case Variable(id) =>
       rctx.mappings.get(id) match {
-        case Some(v) =>
+        case Some(v) if (v != expr) =>
           e(v)
+        case Some(v) =>
+          v
         case None =>
           throw EvalError("No value for identifier " + id.name + " in mapping.")
       }
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index b56974ffc6bba8c7510e4d3ac861de29a3556c2c..82b02486f71a5ec772327b3caf909ef8f544fb6c 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -79,10 +79,20 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
       case _ => Nil
     }
 
+    val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
+
     val testClusters = collect[Map[Identifier, Expr]] {
       case FunctionInvocation(tfd, List(in, out, FiniteMap(inouts))) if tfd.id.name == "passes" =>
         val infos = extractIds(Tuple(Seq(in, out)))
-        val exs   = inouts.map{ case (i, o) => Tuple(Seq(i, o)) }
+        val exs   = inouts.map{ case (i, o) =>
+          val test = Tuple(Seq(i, o)) 
+          val ids = variablesOf(test)
+          evaluator.eval(test, ids.map { (i: Identifier) => i -> i.toVariable }.toMap) match {
+            case EvaluationResults.Successful(res) => res
+            case _ =>
+              test
+          }
+        }
 
         // Check whether we can extract all ids from example
         val results = exs.collect { case e if infos.forall(_._2.isDefinedAt(e)) =>
@@ -147,7 +157,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
 object Problem {
   def fromChoose(ch: Choose, pc: Expr = BooleanLiteral(true)): Problem = {
     val xs = ch.vars
-    val phi = ch.pred
+    val phi = simplifyLets(ch.pred)
     val as = (variablesOf(And(pc, phi))--xs).toList
 
     Problem(as, pc, phi, xs)