diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 89af09e583097f4f38bad008397080c73c566a9c..9337fb7004b2fa90f3ad691550ddc0e72fa68344 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -29,6 +29,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
     "  -P:funcheck:nobapa             Disable BAPA Z3 extension" + "\n" +
     "  -P:funcheck:impure             Generate testcases only for impure functions" + "\n" +
     "  -P:funcheck:testcases=[1,2]    Number of testcases to generate per function" + "\n" +
+    "  -P:funcheck:testbounds=l:u     Lower and upper bounds for integers in recursive datatypes" + "\n" +
     "  -P:funcheck:quiet              No info and warning messages from the extensions" + "\n" +
     "  -P:funcheck:XP                 Enable weird transformations and other bug-producing features" + "\n" +
     "  -P:funcheck:PLDI               PLDI 2011 settings. Now frozen. Not completely functional. See CAV." + "\n" +
@@ -56,6 +57,7 @@ class FunCheckPlugin(val global: Global) extends Plugin {
         case s if s.startsWith("unrolling=") =>  purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
         case s if s.startsWith("functions=") =>  purescala.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
         case s if s.startsWith("extensions=") => purescala.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
+        case s if s.startsWith("testbounds=") => purescala.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
         case s if s.startsWith("testcases=") =>  purescala.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
         case _ => error("Invalid option: " + option)
       }
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index 720b3ea581da27523185b35eb3048c3922b049d9..c1e378783c66bd2da138c4d3958f38480b7e4442 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -16,6 +16,7 @@ object Settings {
   var useBAPA: Boolean = true
   var impureTestcases: Boolean = false
   var nbTestcases: Int = 1
+  var testBounds: (Int, Int) = (0, 3)
   var useInstantiator: Boolean = false
   var useFairInstantiator: Boolean = false
   def useAnyInstantiator : Boolean = useInstantiator || useFairInstantiator
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index aad4a92a09a6ece0ac5da550e29a69b57a814ef3..30585f28845454500a8f3a95799f0a57134fbc2c 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -176,8 +176,8 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3S
   }
 
   private def boundValues : Unit = {
-    val upperBound: Z3AST = z3.mkInt(3, z3.mkIntSort)
-    val lowerBound: Z3AST = z3.mkInt(0, z3.mkIntSort)
+    val lowerBound: Z3AST = z3.mkInt(Settings.testBounds._1, z3.mkIntSort)
+    val upperBound: Z3AST = z3.mkInt(Settings.testBounds._2, z3.mkIntSort)
 
     def isUnbounded(field: VarDecl) : Boolean = field.getType match {
       case Int32Type => true