diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index fdb065d00e7e4c250fa23652d3a63be08ba27864..ac9635208b7abf60feb5360cc7c05abb122a1479 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -317,7 +317,7 @@ trait QuantificationTemplates { self: Templates =>
     if (handledMatchers(relevantBlockers -> matcher)) {
       Seq.empty
     } else if (interrupted) {
-      ignoredMatchers += ((currentGeneration + 1, blockers, matcher))
+      ignoredMatchers += ((currentGeneration, blockers, matcher))
       Seq.empty
     } else {
       ctx.reporter.debug(" -> instantiating matcher " + blockers.mkString("{",",","}") + " ==> " + matcher)
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index b21b0ce929b9d7b45ecbaee9b64bda59c847a23a..fae2c9e23aebdd5fabe3572597168aa3ef05c62c 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -97,6 +97,8 @@ trait AbstractUnrollingSolver extends Solver { self =>
     freeVars.reset()
   }
 
+  ctx.interruptManager.registerForInterrupts(this)
+
   override def interrupt(): Unit = {
     interrupted = true
   }