diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index f7d395feb913244ed24e5aa0379c1e2e8480610c..b9c0dfd94e449ac5a7d130e1279da8ebb7c19b92 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
@@ -13,7 +13,7 @@ import purescala.ExprOps._
 import purescala.Types._
 import utils._
 
-import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks}
+import z3.FairZ3Component.{optFeelingLucky, optUseCodeGen, optAssumePre, optNoChecks, optUnfoldFactor}
 import templates._
 import evaluators._
 
@@ -27,6 +27,7 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
   val useCodeGen     = context.findOptionOrDefault(optUseCodeGen)
   val assumePreHolds = context.findOptionOrDefault(optAssumePre)
   val disableChecks  = context.findOptionOrDefault(optNoChecks)
+  val unfoldFactor   = context.findOptionOrDefault(optUnfoldFactor)
 
   protected var lastCheckResult : (Boolean, Option[Boolean], Option[HenkinModel]) = (false, None, None)
 
@@ -306,14 +307,17 @@ class UnrollingSolver(val context: LeonContext, val program: Program, underlying
           if(!hasFoundAnswer) {
             reporter.debug("- We need to keep going.")
 
-            val toRelease = unrollingBank.getBlockersToUnlock
+            // unfolling `unfoldFactor` times
+            for (i <- 1 to unfoldFactor.toInt) {
+              val toRelease = unrollingBank.getBlockersToUnlock
 
-            reporter.debug(" - more unrollings")
+              reporter.debug(" - more unrollings")
 
-            val newClauses = unrollingBank.unrollBehind(toRelease)
+              val newClauses = unrollingBank.unrollBehind(toRelease)
 
-            for(ncl <- newClauses) {
-              solver.assertCnstr(ncl)
+              for (ncl <- newClauses) {
+                solver.assertCnstr(ncl)
+              }
             }
 
             reporter.debug(" - finished unrolling")
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
index 256dcf38fc5dc99f31ce2f6fb30dc12e0caa5268..70ebd260f931a6a428a84afad9640accf193887d 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
@@ -14,9 +14,10 @@ trait FairZ3Component extends LeonComponent {
   val optUnrollCores   = LeonFlagOptionDef("unrollcores", "Use unsat-cores to drive unrolling while remaining fair", false)
   val optAssumePre     = LeonFlagOptionDef("assumepre",   "Assume precondition holds (pre && f(x) = body) when unfolding", false)
   val optNoChecks      = LeonFlagOptionDef("nochecks",    "Disable counter-example check in presence of foralls"   , false)
+  val optUnfoldFactor  = LeonLongOptionDef("unfoldFactor", "Number of unfoldings to perform in each unfold step", default = 1, "<PosInt>")
 
   override val definedOptions: Set[LeonOptionDef[Any]] =
-    Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre)
+    Set(optEvalGround, optCheckModels, optFeelingLucky, optUseCodeGen, optUnrollCores, optAssumePre, optUnfoldFactor)
 }
 
 object FairZ3Component extends FairZ3Component
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index 21119c4e2728c99850e3af0d1c12e498866f771e..ea09de821427e39cffa3ea9c304e7d1e5a910a4c 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -57,7 +57,6 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
       }
     }
 
-
     try {
       val vcs = generateVCs(vctx, toVerify)
 
diff --git a/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala b/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala
new file mode 100644
index 0000000000000000000000000000000000000000..113e7193a592f8f34739d53992b41857000acd5d
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/TestLazinessOfAnd.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+object AndTest {
+   def nonterm(x: BigInt) : BigInt = {
+     nonterm(x + 1)
+   } ensuring(res => false)
+
+   def precond(y : BigInt) = y < 0
+
+   /**
+    * Leon should find a counter-example here.
+   **/
+   def foo(y: BigInt) : Boolean = {
+     require(precond(y))
+     y >= 0 && (nonterm(0) == 0)
+   } holds
+}