diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 6652424333a536e340e799553967eed6092a0864..60ddb145058eeb33b4bcb796307fba87d586d52f 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -9,6 +9,7 @@ import purescala.Expressions._
 import purescala.Extractors._
 import purescala.ExprOps._
 import purescala.Types._
+import purescala.TypeOps._
 import purescala.Definitions._
 import purescala.Constructors._
 import purescala.Quantification._
@@ -253,14 +254,6 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
       res
     }
 
-    def liftToIfExpr(pathVar: Identifier, parts: Seq[Expr], join: Seq[Expr] => Expr, recons: (Expr, Expr) => Expr): Expr = {
-      val partitions = groupWhile(parts)(!requireDecomposition(_))
-      partitions.map(join) match {
-        case Seq(e) => e
-        case seq => rec(pathVar, seq.reduceRight(recons))
-      }
-    }
-
     def rec(pathVar: Identifier, expr: Expr): Expr = {
       expr match {
         case a @ Assert(cond, err, body) =>
@@ -416,7 +409,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
           val idArgs : Seq[Identifier] = lambdaArgs(l)
           val trArgs : Seq[T] = idArgs.map(id => substMap.getOrElse(id, encoder.encodeId(id)))
 
-          val lid = FreshIdentifier("lambda", l.getType, true)
+          val lid = FreshIdentifier("lambda", bestRealType(l.getType), true)
           val clause = liftedEquals(Variable(lid), l, idArgs, inlineFirst = true)
 
           val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index 07019aefd6e7f1b266cc60860c12f8840f48b126..618a23c3a285b11bc9d4fb2da4eccecc87a45f16 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -11,6 +11,7 @@ import purescala.Quantification._
 import purescala.Extractors._
 import purescala.ExprOps._
 import purescala.Types._
+import purescala.TypeOps._
 
 import utils._
 
@@ -116,7 +117,7 @@ object Template {
 
     val (fiArgs, appArgs) = args.splitAt(tfd.params.size)
     val app @ Application(caller, arguments) = rec(FunctionInvocation(tfd, fiArgs), appArgs)
-    Matcher(encodeExpr(caller), caller.getType, arguments.map(arg => Left(encodeExpr(arg))), encodeExpr(app))
+    Matcher(encodeExpr(caller), bestRealType(caller.getType), arguments.map(arg => Left(encodeExpr(arg))), encodeExpr(app))
   }
 
   def encode[T](
@@ -142,7 +143,9 @@ object Template {
     }).toSeq
 
     val optIdCall = optCall.map(tfd => TemplateCallInfo[T](tfd, arguments.map(_._2)))
-    val optIdApp = optApp.map { case (idT, tpe) => App(idT, tpe, arguments.map(_._2)) }
+    val optIdApp = optApp.map { case (idT, tpe) =>
+      App(idT, bestRealType(tpe).asInstanceOf[FunctionType], arguments.map(_._2))
+    }
 
     lazy val invocMatcher = optCall.filter(_.returnType.isInstanceOf[FunctionType])
       .map(tfd => invocationMatcher(encodeExpr)(tfd, arguments.map(_._1.toVariable)))
@@ -160,7 +163,7 @@ object Template {
         for (e <- es) {
           funInfos ++= firstOrderCallsOf(e).map(p => TemplateCallInfo(p._1, p._2.map(encodeExpr)))
           appInfos ++= firstOrderAppsOf(e).map { case (c, args) =>
-            App(encodeExpr(c), c.getType.asInstanceOf[FunctionType], args.map(encodeExpr))
+            App(encodeExpr(c), bestRealType(c.getType).asInstanceOf[FunctionType], args.map(encodeExpr))
           }
 
           matchInfos ++= fold[Map[Expr, Matcher[T]]] { (expr, res) =>
@@ -175,7 +178,7 @@ object Template {
                   case None => Left(encodeExpr(arg))
                 })
 
-                Some(expr -> Matcher(encodeExpr(c), c.getType, encodedArgs, encodeExpr(expr)))
+                Some(expr -> Matcher(encodeExpr(c), bestRealType(c.getType), encodedArgs, encodeExpr(expr)))
               case _ => None
             })
           }(e).values
diff --git a/src/main/scala/leon/solvers/templates/UnrollingBank.scala b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
index e6e5cd22370ec7bc8709e022e683f3d465bfd246..d1c4432a3c69f1882c9b4a1787a12dc8cf64f520 100644
--- a/src/main/scala/leon/solvers/templates/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/templates/UnrollingBank.scala
@@ -334,6 +334,12 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
       newClauses ++= newCls
     }
 
+    /*
+    for ((app @ (b, _), (gen, _, _, _, infos)) <- thisAppInfos if infos.isEmpty) {
+      registerAppBlocker(nextGeneration(gen), app, infos)
+    }
+    */
+
     reporter.debug(s"   - ${newClauses.size} new clauses")
     //context.reporter.ifDebug { debug =>
     //  debug(s" - new clauses:")