diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala
index aa9be2481673e613473e50a80dd3616cf7d74cb4..60f4b55bb39854d57556fb7873733a610fbbbc95 100644
--- a/src/main/scala/inox/Main.scala
+++ b/src/main/scala/inox/Main.scala
@@ -64,7 +64,7 @@ trait MainHelpers {
     solvers.unrolling.optFeelingLucky -> Description(Solvers, "Use evaluator to find counter-examples early"),
     solvers.unrolling.optUnrollAssumptions -> Description(Solvers, "Use unsat-assumptions to drive unfolding while remaining fair"),
     solvers.unrolling.optNoSimplifications -> Description(Solvers, "Disable selector/quantifier simplifications in solvers"),
-    solvers.unrolling.optModelFinding -> Description(Solvers, "Enhance model-finding capabilities of solvers"),
+    solvers.unrolling.optModelFinding -> Description(Solvers, "Enhance model-finding capabilities of solvers by given aggresivity"),
     solvers.smtlib.optCVC4Options -> Description(Solvers, "Pass extra options to CVC4"),
     evaluators.optMaxCalls -> Description(Evaluators, "Maximum function invocations allowed during evaluation (-1 for unbounded)"),
     evaluators.optIgnoreContracts -> Description(Evaluators, "Don't fail on invalid contracts during evaluation")
diff --git a/src/main/scala/inox/solvers/unrolling/Templates.scala b/src/main/scala/inox/solvers/unrolling/Templates.scala
index c07a618f1863440bba5e7351d78cea5251224848..f8180875587b90d6803a08d82fff74108060a87d 100644
--- a/src/main/scala/inox/solvers/unrolling/Templates.scala
+++ b/src/main/scala/inox/solvers/unrolling/Templates.scala
@@ -46,10 +46,11 @@ trait Templates extends TemplateGenerator
   private[unrolling] lazy val falseT = mkEncoder(Map.empty)(BooleanLiteral(false))
 
   protected lazy val simplify = !ctx.options.findOptionOrDefault(optNoSimplifications)
+  protected lazy val deferFactor =  3 * ctx.options.findOptionOrDefault(optModelFinding)
 
   private var currentGen: Int = 0
   protected def currentGeneration: Int = currentGen
-  protected def nextGeneration(gen: Int): Int = gen + 3
+  protected def nextGeneration(gen: Int): Int = gen + 3 + deferFactor
 
   trait Manager extends IncrementalStateWrapper {
     def unrollGeneration: Option[Int]
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
index 052cfaf1700b02783ff28f689f9324e89656e315..caae2a21aef5b7b9cc2d31148b4847cefc04aa6d 100644
--- a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
+++ b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -12,10 +12,15 @@ import combinators._
 
 import scala.collection.mutable.{Map => MutableMap}
 
-object optUnrollFactor      extends LongOptionDef("unrollfactor", default = 1, "<PosInt>")
+object optUnrollFactor      extends IntOptionDef("unrollfactor", default = 1, "<PosInt>")
 object optFeelingLucky      extends FlagOptionDef("feelinglucky", false)
 object optUnrollAssumptions extends FlagOptionDef("unrollassumptions", false)
-object optModelFinding      extends FlagOptionDef("modelfinding", false)
+object optModelFinding      extends IntOptionDef("modelfinding", 0, "<PosInt> | 0 (off)") {
+  override val parser: OptionParsers.OptionParser[Int] = (s => s match {
+    case "" => Some(1)
+    case _ => OptionParsers.intParser(s)
+  })
+}
 
 trait AbstractUnrollingSolver extends Solver { self =>
 
@@ -70,7 +75,7 @@ trait AbstractUnrollingSolver extends Solver { self =>
   lazy val unrollFactor = options.findOptionOrDefault(optUnrollFactor)
   lazy val feelingLucky = options.findOptionOrDefault(optFeelingLucky)
   lazy val unrollAssumptions = options.findOptionOrDefault(optUnrollAssumptions)
-  lazy val modelFinding = options.findOptionOrDefault(optModelFinding)
+  lazy val modelFinding = options.findOptionOrDefault(optModelFinding) > 0
 
   def check(config: CheckConfiguration): config.Response[Model, Assumptions] =
     checkAssumptions(config)(Set.empty)
@@ -628,7 +633,7 @@ trait AbstractUnrollingSolver extends Solver { self =>
 
           val timer = ctx.timers.solvers.unroll.start()
           // unfolling `unrollFactor` times
-          for (i <- 1 to unrollFactor.toInt if templates.canUnroll) {
+          for (i <- 1 to unrollFactor.toInt if templates.canUnroll && !abort && !pause) {
             val newClauses = templates.unroll
             for (ncl <- newClauses) {
               underlying.assertCnstr(ncl)