diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 403fb08fd20c9297b91cd6294cfc4a707e7ad40a..b7aa7dc664c80941d8fcd23e7e5f807aead28174 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -210,7 +210,11 @@ trait AbstractUnrollingSolver[T]
   private def validateModel(model: Model, assumptions: Seq[Expr], silenceErrors: Boolean): Boolean = {
     val expr = andJoin(assumptions ++ constraints)
 
-    evaluator.eval(expr, model) match {
+    val newExpr = model.toSeq.foldLeft(expr){
+      case (e, (k, v)) => let(k, v, e)
+    }
+    
+    evaluator.eval(newExpr) match {
       case EvaluationResults.Successful(BooleanLiteral(true)) =>
         reporter.debug("- Model validated.")
         true