From 4882f9c7c2b95dd707eae2dd825af93c1e576d40 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Tue, 26 Apr 2016 17:04:52 +0200
Subject: [PATCH] Fixed the UnrollingSolver.scala evaluation.
---
src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 403fb08fd..b7aa7dc66 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
--
GitLab