diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 3258128f8774807ac1bc7d4980a1350c85e08f0b..466e1c0aed5c1398cac87dd03c9228a8494e0232 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -224,12 +224,19 @@ class FairZ3Solver(context : LeonContext)
 
     def blockersInfo = blockersInfoStack.head
 
+    // Note that this computes cumulated sets.
+    private var unlockedStack : List[MutableSet[Z3AST]] = List(MutableSet())
+    def unlockedSet : MutableSet[Z3AST] = unlockedStack.head
+    def wasUnlocked(id : Z3AST) : Boolean = unlockedStack.head(id)
+
     def push() {
       blockersInfoStack = (MutableMap() ++ blockersInfo) :: blockersInfoStack
+      unlockedStack     = (MutableSet() ++ unlockedStack.head) :: unlockedStack
     }
 
     def pop(lvl: Int) {
       blockersInfoStack = blockersInfoStack.drop(lvl)
+      unlockedStack     = unlockedStack.drop(lvl)
     }
 
     def z3CurrentZ3Blockers = blockersInfo.map(_._2._3)
@@ -260,9 +267,13 @@ class FairZ3Solver(context : LeonContext)
       val z3ast = z3.mkNot(id)
       blockersInfo.get(id) match {
         case Some((exGen, origGen, _, exFis)) =>
-          assert(exGen == gen, "Mixing the same id "+id+" with various generations "+ exGen+" and "+gen)
+          // PS: when recycling `b`s, this assertion becomes dangerous.
+          // It's better to simply take the min of the generations.
+          // assert(exGen == gen, "Mixing the same id "+id+" with various generations "+ exGen+" and "+gen)
+
+          val minGen = gen min exGen
 
-          blockersInfo(id) = ((gen, origGen, z3ast, fis++exFis))
+          blockersInfo(id) = ((minGen, origGen, z3ast, fis++exFis))
         case None =>
           blockersInfo(id) = ((gen, gen, z3ast, fis))
       }
@@ -319,26 +330,35 @@ class FairZ3Solver(context : LeonContext)
     def unlock(id: Z3AST) : Seq[Z3AST] = {
       assert(blockersInfo contains id)
 
+      if(unlockedSet(id)) return Seq.empty
+
       val (gen, origGen, _, fis) = blockersInfo(id)
+
       blockersInfo -= id
+      val twice = wasUnlocked(id)
 
       var newClauses : Seq[Z3AST] = Seq.empty
 
+      var reintroducedSelf : Boolean = false
+
       for(fi <- fis) {
         val template              = getTemplate(fi.funDef)
         val (newExprs, newBlocks) = template.instantiate(id, fi.args)
 
-        // println("In unlock :")
-        // println("CLAUSES")
-        // newExprs.foreach(println) 
-
-        for((i, fis) <- newBlocks) {
-          registerBlocker(nextGeneration(gen), i, fis)
+        for((i, fis2) <- newBlocks) {
+          registerBlocker(nextGeneration(gen), i, fis2)
+          if(i == id) {
+            reintroducedSelf = true
+          }
         }
 
         newClauses ++= newExprs
       }
 
+      if(!reintroducedSelf) {
+        unlockedSet += id
+      }
+
       newClauses
     }
   }
@@ -580,13 +600,11 @@ class FairZ3Solver(context : LeonContext)
             if(!foundDefinitiveAnswer) { 
               reporter.info("- We need to keep going.")
 
-              //val toReleaseAsPairs = unrollingBank.getBlockersToUnlock
-              // unrollingBank.dumpBlockers
-              val toReleaseAsPairs = unrollingBank.getZ3BlockersToUnlock
+              val toRelease = unrollingBank.getZ3BlockersToUnlock
 
               reporter.info(" - more unrollings")
 
-              for(id <- toReleaseAsPairs) {
+              for(id <- toRelease) {
                 unlockingTime.start
                 val newClauses = unrollingBank.unlock(id)
                 unlockingTime.stop
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index f4e3724c45d6d26d6d41475ca18694cf0d1fb209..01d303148066e8ad8058ad72698924b0b3aa3ba7 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -78,6 +78,9 @@ class FunctionTemplate private(
       (idToZ3Ids(b) -> funs.map(fi => Z3FunctionInvocation(fi.funDef, fi.args.map(solver.toZ3Formula(_, idToZ3Ids).get))))
   }
 
+  // We use a cache to create the same boolean variables.
+  private val cache : MutableMap[Seq[Z3AST],Map[Z3AST,Z3AST]] = MutableMap.empty
+
   def instantiate(aVar : Z3AST, args : Seq[Z3AST]) : (Seq[Z3AST], Map[Z3AST,Set[Z3FunctionInvocation]]) = {
     assert(args.size == funDef.args.size)
 
@@ -99,11 +102,19 @@ class FunctionTemplate private(
         }
       }
     }
+    // ...end of ground evaluation part.
+
+    val (wasHit,baseIDSubstMap) = cache.get(args) match {
+      case Some(m) => (true,m)
+      case None =>
+        val newMap : Map[Z3AST,Z3AST] = 
+          (zippedExprVars ++ zippedCondVars).map(p => p._2 -> solver.idToFreshZ3Id(p._1)).toMap ++
+          (z3FunDefArgs zip args)
+        cache(args) = newMap
+        (false,newMap)
+    }
 
-    val idSubstMap : Map[Z3AST, Z3AST] =
-      Map(z3ActivatingBool -> aVar) ++
-      (zippedExprVars ++ zippedCondVars).map{ case (id, c) => c -> solver.idToFreshZ3Id(id) } ++
-      (z3FunDefArgs zip args)
+    val idSubstMap : Map[Z3AST,Z3AST] = baseIDSubstMap + (z3ActivatingBool -> aVar)
 
     val (from, to) = idSubstMap.unzip
     val (fromArray, toArray) = (from.toArray, to.toArray)