diff --git a/src/main/scala/leon/solvers/templates/DatatypeManager.scala b/src/main/scala/leon/solvers/templates/DatatypeManager.scala
index 8f9c2202adac023c52de03a693a075a660e21a99..365fe85ff9839d477ba2b192db0fe5d891a079f6 100644
--- a/src/main/scala/leon/solvers/templates/DatatypeManager.scala
+++ b/src/main/scala/leon/solvers/templates/DatatypeManager.scala
@@ -20,6 +20,11 @@ import Template._
 
 import scala.collection.mutable.{Map => MutableMap, Set => MutableSet}
 
+case class FreshFunction(expr: Expr) extends Expr with Extractable {
+  val getType = BooleanType
+  val extract = Some(Seq(expr), (exprs: Seq[Expr]) => FreshFunction(exprs.head))
+}
+
 object DatatypeTemplate {
 
   def apply[T](
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index edb096ef222243506d0af47b69f8ef340c5fe857..647c75a69caac67f8cfa43fbe96be24ea3e9583c 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -24,11 +24,6 @@ case class App[T](caller: T, tpe: FunctionType, args: Seq[Arg[T]], encoded: T) {
   override def toString = "(" + caller + " : " + tpe + ")" + args.map(_.encoded).mkString("(", ",", ")")
 }
 
-case class FreshFunction(expr: Expr) extends Expr with Extractable {
-  val getType = BooleanType
-  val extract = Some(Seq(expr), (exprs: Seq[Expr]) => FreshFunction(exprs.head))
-}
-
 object LambdaTemplate {
 
   def apply[T](
@@ -238,7 +233,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) extends DatatypeManager(enco
     neqClauses ++ extClauses
   }
 
-  def assumptions: Seq[T] = freeBlockers.flatMap(_._2.map(p => encoder.mkNot(p._2))).toSeq
+  def assumptions: Seq[T] = freeBlockers.toSeq.flatMap(_._2.map(p => encoder.mkNot(p._1)))
 
   private val typeBlockers = new IncrementalMap[T, T]()
   private val typeEnablers: MutableSet[T] = MutableSet.empty
diff --git a/src/main/scala/leon/solvers/templates/TemplateManager.scala b/src/main/scala/leon/solvers/templates/TemplateManager.scala
index 62a3f0c7617fbe819f7671e1b7a024fdc5b4832c..56c8e6211e033ce0c002f695b535999a724ab223 100644
--- a/src/main/scala/leon/solvers/templates/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateManager.scala
@@ -159,18 +159,19 @@ object Template {
       var clauses: Seq[T] = Seq.empty
 
       val cleanGuarded = guardedExprs.map { case (b, es) => b -> es.map { e =>
+        def clean(expr: Expr): Expr = postMap {
+          case FreshFunction(f) => Some(BooleanLiteral(true))
+          case _ => None
+        } (expr)
+
         val withPaths = CollectorWithPaths { case FreshFunction(f) => f }.traverse(e)
         functions ++= withPaths.map { case (f, TopLevelAnds(paths)) =>
           val tpe = bestRealType(f.getType).asInstanceOf[FunctionType]
-          val path = andJoin(paths.filterNot(_.isInstanceOf[FreshFunction]))
+          val path = andJoin(paths.map(clean))
           (encodeExpr(and(Variable(b), path)), tpe, encodeExpr(f))
         }
 
-        val cleanExpr = postMap {
-          case FreshFunction(f) => Some(BooleanLiteral(true))
-          case _ => None
-        } (e)
-
+        val cleanExpr = clean(e)
         clauses :+= encodeExpr(Implies(Variable(b), cleanExpr))
         cleanExpr
       }}
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 3cadf39a6e3853196d4cdf6b7493ea91a6077c73..7ae02d83e0a6245c7345ef7349211e6c246221ac 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -257,7 +257,7 @@ trait AbstractZ3Solver extends Solver {
       }
 
     case other =>
-      throw SolverUnsupportedError(other, this)
+      unsupported(other)
   }
 
   protected[leon] def toZ3Formula(expr: Expr, initialMap: Map[Identifier, Z3AST] = Map.empty): Z3AST = {