diff --git a/src/main/scala/leon/solvers/unrolling/TemplateManager.scala b/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
index 36bad0b5879b0a8dcab1c46cdc90aa5014de556c..e55c46f2fc97f442e6a49a8a71307cb5390fc5de 100644
--- a/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
+++ b/src/main/scala/leon/solvers/unrolling/TemplateManager.scala
@@ -497,6 +497,7 @@ class TemplateManager[T](protected[unrolling] val encoder: TemplateEncoder[T]) e
   def blocker(b: T): Unit = condImplies += (b -> Set.empty)
   def isBlocker(b: T): Boolean = condImplies.isDefinedAt(b) || condImplied.isDefinedAt(b)
   def blockerParents(b: T): Set[T] = condImplied(b)
+  def blockerChildren(b: T): Set[T] = condImplies(b)
 
   def implies(b1: T, b2: T): Unit = implies(b1, Set(b2))
   def implies(b1: T, b2s: Set[T]): Unit = {
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingBank.scala b/src/main/scala/leon/solvers/unrolling/UnrollingBank.scala
index feb6188271796b411db8c8ae5004c1d23e21aadb..7ba55bd379e528e2b3702e1138f7d5ecbfd2154d 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingBank.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingBank.scala
@@ -196,7 +196,7 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
     clauses
   }
 
-  def nextGeneration(gen: Int) = gen + 3
+  def nextGeneration(gen: Int) = gen + 5
 
   def decreaseAllGenerations() = {
     for ((block, (gen, origGen, ast, infos)) <- callInfos) {
@@ -209,19 +209,34 @@ class UnrollingBank[T <% Printable](ctx: LeonContext, templateGenerator: Templat
     }
   }
 
-  def promoteBlocker(b: T) = {
-    if (callInfos contains b) {
-      val (_, origGen, notB, fis) = callInfos(b)
+  def promoteBlocker(b: T, force: Boolean = false): Boolean = {
+    var seen: Set[T] = Set.empty
+    var promoted: Boolean = false
 
-      callInfos += b -> (1, origGen, notB, fis)
-    }
+    def rec(b: T): Unit = if (!seen(b)) {
+      seen += b
+      if (callInfos contains b) {
+        val (_, origGen, notB, fis) = callInfos(b)
+
+        callInfos += b -> (1, origGen, notB, fis)
+        promoted = true
+      }
 
-    if (blockerToApps contains b) {
-      val app = blockerToApps(b)
-      val (_, origGen, _, notB, infos) = appInfos(app)
+      if (blockerToApps contains b) {
+        val app = blockerToApps(b)
+        val (_, origGen, _, notB, infos) = appInfos(app)
 
-      appInfos += app -> (1, origGen, b, notB, infos)
+        appInfos += app -> (1, origGen, b, notB, infos)
+        promoted = true
+      }
+
+      if (!promoted && force) {
+        for (cb <- templateGenerator.manager.blockerChildren(b)) rec(cb)
+      }
     }
+
+    rec(b)
+    promoted
   }
 
   def instantiateQuantifiers(force: Boolean = false): Seq[T] = {
diff --git a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
index 99fdbd048055a6f044a3b2678a115e93ab39eae8..76f18864b453df290c372af35658707525058224 100644
--- a/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/unrolling/UnrollingSolver.scala
@@ -397,7 +397,7 @@ trait AbstractUnrollingSolver[T]
                   unrollingBank.decreaseAllGenerations()
 
                   for (b <- templateGenerator.manager.getBlockersToPromote(model.eval)) {
-                    unrollingBank.promoteBlocker(b)
+                    unrollingBank.promoteBlocker(b, force = true)
                   }
                 }
               }