diff --git a/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala b/src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala
index 8442624baf7886c71dde9e72ffe28554791d0664..ff0573a5803639fcf94839c55bca0a871c4ae9f5 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 915aa9edbd74f6eb8284b9a7d85ac827a4a26ef0..e49d71bac411e1d9a3d45be09a51a785cc9c15c3 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)