diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 72cfffec3f8ef3fd8a526d778fda1f26a9ec1a41..b9ba6df1f688e01edf631e995ba2f8623bcfc5fe 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -6,6 +6,7 @@ package synthesis
 import purescala.ExprOps._
 
 import purescala.ScalaPrinter
+import leon.utils._
 import purescala.Definitions.{Program, FunDef}
 import leon.utils.ASCIIHelpers
 
@@ -20,12 +21,11 @@ object SynthesisPhase extends TransformationPhase {
   val optDerivTrees  = LeonFlagOptionDef( "derivtrees", "Generate derivation trees", false)
 
   // CEGIS options
-  val optCEGISShrink     = LeonFlagOptionDef( "cegis:shrink",     "Shrink non-det programs when tests pruning works well",  true)
   val optCEGISOptTimeout = LeonFlagOptionDef( "cegis:opttimeout", "Consider a time-out of CE-search as untrusted solution", true)
   val optCEGISVanuatoo   = LeonFlagOptionDef( "cegis:vanuatoo",   "Generate inputs using new korat-style generator",       false)
 
   override val definedOptions : Set[LeonOptionDef[Any]] =
-    Set(optManual, optCostModel, optDerivTrees, optCEGISShrink, optCEGISOptTimeout, optCEGISVanuatoo)
+    Set(optManual, optCostModel, optDerivTrees, optCEGISOptTimeout, optCEGISVanuatoo)
 
   def processOptions(ctx: LeonContext): SynthesisSettings = {
     val ms = ctx.findOption(optManual)
@@ -57,7 +57,6 @@ object SynthesisPhase extends TransformationPhase {
       manualSearch = ms,
       functions = ctx.findOption(SharedOptions.optFunctions) map { _.toSet },
       cegisUseOptTimeout = ctx.findOption(optCEGISOptTimeout),
-      cegisUseShrink = ctx.findOption(optCEGISShrink),
       cegisUseVanuatoo = ctx.findOption(optCEGISVanuatoo)
     )
   }
@@ -74,21 +73,25 @@ object SynthesisPhase extends TransformationPhase {
 
       val synthesizer = new Synthesizer(ctx, program, ci, options)
 
-      val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
+      val to = new TimeoutFor(ctx.interruptManager)
 
-      try {
-        if (options.generateDerivationTrees) {
-          val dot = new DotGenerator(search.g)
-          dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot")
-        }
+      to.interruptAfter(options.timeoutMs) {
+        val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), allowPartial = true)
+
+        try {
+          if (options.generateDerivationTrees) {
+            val dot = new DotGenerator(search.g)
+            dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot")
+          }
 
-        val (sol, _) = solutions.head
+          val (sol, _) = solutions.head
 
-        val expr = sol.toSimplifiedExpr(ctx, program)
-        fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
-        functions += fd
-      } finally {
-        synthesizer.shutdown()
+          val expr = sol.toSimplifiedExpr(ctx, program)
+          fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
+          functions += fd
+        } finally {
+          synthesizer.shutdown()
+        }
       }
     }
 
diff --git a/src/main/scala/leon/synthesis/SynthesisSettings.scala b/src/main/scala/leon/synthesis/SynthesisSettings.scala
index 9d227bdb611f2ca44eb70a95ce52bc506712e160..5202818e18765ebf4086ef41d1685967a14940d0 100644
--- a/src/main/scala/leon/synthesis/SynthesisSettings.scala
+++ b/src/main/scala/leon/synthesis/SynthesisSettings.scala
@@ -17,7 +17,6 @@ case class SynthesisSettings(
   
   // Cegis related options
   cegisUseOptTimeout: Option[Boolean] = None,
-  cegisUseShrink: Option[Boolean]     = None,
   cegisUseVanuatoo: Option[Boolean]   = None
 
 )
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 09ee7dd30b49b180c38131372d39600bd9faad1e..4f03c9bed6ca7c7ce5338d04283483ab9f348890 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -45,14 +45,10 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
     // CEGIS Flags to activate or deactivate features
     val useOptTimeout    = sctx.settings.cegisUseOptTimeout.getOrElse(true)
     val useVanuatoo      = sctx.settings.cegisUseVanuatoo.getOrElse(false)
-    val useShrink        = sctx.settings.cegisUseShrink.getOrElse(false)
 
     // Limits the number of programs CEGIS will specifically validate individually
     val validateUpTo     = 3
 
-    // Shrink the program when the ratio of passing cases is less than the threshold
-    val shrinkThreshold  = 1.0/2
-
     val interruptManager = sctx.context.interruptManager
 
     val params = getParams(sctx, p)
@@ -827,14 +823,13 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
 
                     if (nPassing <= validateUpTo) {
                       // All programs failed verification, we filter everything out and unfold
-                      //ndProgram.shrinkTo(Set(), unfolding == maxUnfoldings)
                       doFilter     = false
                       skipCESearch = true
                     }
                 }
               }
 
-              if (doFilter && !(nPassing < nInitial * shrinkThreshold && useShrink)) {
+              if (doFilter) {
                 sctx.reporter.debug("Excluding "+wrongPrograms.size+" programs")
                 wrongPrograms.foreach {
                   ndProgram.excludeProgram(_, true)