diff --git a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
index 70f0ee251e055137acd25cf1bb68bf325736c477..85382cfcdf39a7d1cd77c78a4a76b7ed32a02689 100644
--- a/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/QuantificationManager.scala
@@ -1199,8 +1199,12 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
               }
             }.toMap
 
-            if (conditionals.isEmpty) {
-              value
+            if (conditionals.isEmpty) f match {
+              case FiniteLambda(mapping, dflt, tpe) =>
+                Lambda(params.map(ValDef(_)), mapping.foldRight(dflt) { case ((es, v), elze) =>
+                  IfExpr(andJoin((params zip es).map(p => Equals(p._1.toVariable, p._2))), v, elze)
+                })
+              case _ => f
             } else {
               val ((_, dflt)) +: rest = conditionals.toSeq.sortBy { case (conds, _) =>
                 (conds.flatMap(variablesOf).toSet.size, conds.size)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index ee54fc9f2dc0cd9739da6686ea19f1b1821a3aa5..7bd2d93e828ce92ae948f11b1c0ce06e0fae4aff 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -54,6 +54,7 @@ trait AbstractZ3Solver extends Solver {
   )
 
   // @nv: This MUST take place AFTER Z3Context was created!!
+  // Well... actually maybe not, but let's just leave it here to be sure
   toggleWarningMessages(true)
 
   protected var solver : Z3Solver  = null