From ea7cbd6a5fb44de92bc5368bbfd901269e94aa33 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sat, 29 Oct 2016 15:00:01 +0200
Subject: [PATCH] Fix for unique lambda extractions from model
---
.../scala/inox/solvers/unrolling/LambdaTemplates.scala | 2 +-
.../scala/inox/solvers/unrolling/UnrollingSolver.scala | 10 +++++-----
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index 8442624ba..ff0573a58 100644
--- a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
@@ -259,7 +259,7 @@ trait LambdaTemplates { self: Templates =>
freeFunctions += ft -> (freeFunctions(ft) + (b -> f))
lazy val gen = nextGeneration(currentGeneration)
- for (app @ (_, App(caller, _, args, _)) <- applications(tpe)) {
+ for (app @ (_, App(caller, _, args, _)) <- applications(ft)) {
val cond = mkAnd(b, mkEquals(f, caller))
registerAppBlocker(gen, app, Right(f), cond, args)
}
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 915aa9edb..e49d71bac 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -318,11 +318,11 @@ trait AbstractUnrollingSolver extends Solver { self =>
val lambda = FiniteLambda(params, mappings, dflt)
// make sure `lambda` is not equal to any other distinct extracted first-class function
val res = (funExtractions.collectFirst {
- case (encoded, `lambda`) =>
- Right(encoded)
- case (e, img) if
- wrapped.eval(templates.mkEquals(e, f), BooleanType) == Some(BooleanLiteral(true)) =>
- Left(img)
+ case (encoded, `lambda`) => Right(encoded)
+ case (e, img) if (
+ bestRealType(img.getType) == bestRealType(lambda.getType) &&
+ wrapped.eval(templates.mkEquals(e, f), BooleanType) == Some(BooleanLiteral(true))
+ )=> Left(img)
}) match {
case Some(Right(enc)) => wrapped.eval(enc, tpe).get match {
case Lambda(_, Let(_, IntegerLiteral(n), _)) => uniquateClosure(n, lambda)
--
GitLab