diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala
index 619b7660686c9ff984e85aaa867eab9f522aecd9..29e102281ae6572f86a286404cee9dfb1d670bdd 100644
--- a/src/main/scala/leon/datagen/GrammarDataGen.scala
+++ b/src/main/scala/leon/datagen/GrammarDataGen.scala
@@ -55,7 +55,7 @@ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar = ValueGra
 
   def generate(tpe: TypeTree): Iterator[Expr] = {
     val enum = new MemoizedEnumerator[Label, Expr, ProductionRule[Label, Expr]](grammar.getProductions)
-    enum.iterator(Label(tpe)).flatMap(expandGenerics)
+    enum.iterator(Label(tpe)).flatMap(expandGenerics).takeWhile(_ => !interrupted.get)
   }
 
   def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
@@ -82,6 +82,7 @@ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar = ValueGra
       detupled.take(maxEnumerated)
               .filter(filterCond)
               .take(maxValid)
+              .takeWhile(_ => !interrupted.get)
     }
   }
 
diff --git a/src/main/scala/leon/datagen/SolverDataGen.scala b/src/main/scala/leon/datagen/SolverDataGen.scala
index 34d94c1a9013edc2c1d2e3f923e5a754e2934862..37dcfba061b7ef9fd71bb2d31e57754950eed5d5 100644
--- a/src/main/scala/leon/datagen/SolverDataGen.scala
+++ b/src/main/scala/leon/datagen/SolverDataGen.scala
@@ -15,7 +15,7 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) e
   implicit val ctx0 = ctx
 
   def generate(tpe: TypeTree): FreeableIterator[Expr] = {
-    generateFor(Seq(FreshIdentifier("tmp", tpe)), BooleanLiteral(true), 20, 20).map(_.head)
+    generateFor(Seq(FreshIdentifier("tmp", tpe)), BooleanLiteral(true), 20, 20).map(_.head).takeWhile(_ => !interrupted.get)
   }
 
   def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): FreeableIterator[Seq[Expr]] = {
@@ -76,7 +76,7 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) e
 
       val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
 
-      enum.take(maxValid).map(model => ins.map(model))
+      enum.take(maxValid).map(model => ins.map(model)).takeWhile(_ => !interrupted.get)
     }
   }
 
diff --git a/src/main/scala/leon/utils/FreeableIterator.scala b/src/main/scala/leon/utils/FreeableIterator.scala
index ad2942c93a40b0eab58a407d66262cf5a6920c6e..9b37342703fb44570566f3801bfeb24573c606b5 100644
--- a/src/main/scala/leon/utils/FreeableIterator.scala
+++ b/src/main/scala/leon/utils/FreeableIterator.scala
@@ -4,6 +4,8 @@ package leon
 package utils
 
 abstract class FreeableIterator[T] extends Iterator[T] {
+  orig =>
+
   private[this] var nextElem: Option[T] = None
 
   def hasNext = {
@@ -20,8 +22,6 @@ abstract class FreeableIterator[T] extends Iterator[T] {
   def free()
 
   override def map[B](f: T => B): FreeableIterator[B] = {
-    val orig = this
-
     new FreeableIterator[B] {
       def computeNext() = orig.computeNext.map(f)
       def free() = orig.free()
@@ -29,10 +29,8 @@ abstract class FreeableIterator[T] extends Iterator[T] {
   }
 
   override def take(n: Int): FreeableIterator[T] = {
-    val orig = this
-
     new FreeableIterator[T] {
-      private var c = 0;
+      private var c = 0
 
       def computeNext() = {
         if (c < n) {
@@ -47,6 +45,13 @@ abstract class FreeableIterator[T] extends Iterator[T] {
     }
   }
 
+  override def takeWhile(p: T => Boolean) = {
+    new FreeableIterator[T] {
+      def computeNext(): Option[T] = orig.computeNext.filter(p)
+      def free(): Unit = orig.free()
+    }
+  }
+
   override def toList: List[T] = {
     val res = super.toList
     free()
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 104389eb7e9a1b8d7878d09d678a31448ed5b283..839e45dbab58091826eb16827e79ba5f083c692f 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -2,7 +2,6 @@
 
 package leon.regression.verification
 
-import smtlib.interpreters.Z3Interpreter
 import leon.solvers.SolverFactory
 
 // If you add another regression test, make sure it contains exactly one object, whose name matches the file name.