diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 1397bf5b32a327c0b7b639d869d1f197ff40e74d..d4f5e72406270e126a62cc3904189f9c4553836f 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -507,12 +507,12 @@ abstract class CEGISLike(name: String) extends Rule(name) {
        * Here we check the validity of a (small) number of programs in isolation.
        * We keep track of CEXs generated by invalid programs and preemptively filter the rest of the programs with them.
        */
-      def validatePrograms(bss: Set[Set[Identifier]]): Either[Seq[Seq[Expr]], Solution] = {
+      def validatePrograms(bss: Set[Set[Identifier]]): Either[Seq[Seq[Expr]], Stream[Solution]] = {
         val origImpl = cTreeFd.fullBody
 
         var cexs = Seq[Seq[Expr]]()
 
-        var best: Option[Solution] = None
+        var best: List[Solution] = Nil
 
         for (bs <- bss.toSeq) {
           // We compute the corresponding expr and replace it in place of the C-tree
@@ -537,6 +537,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
             val solver = solverf.getNewSolver()
             try {
               debug("Sending candidate to solver...")
+              def currentSolution(trusted: Boolean) = Solution(BooleanLiteral(true), Set(), outerSol, isTrusted = trusted)
               solver.assertCnstr(cnstr)
               solver.check match {
                 case Some(true) =>
@@ -556,14 +557,12 @@ abstract class CEGISLike(name: String) extends Rule(name) {
                 case Some(false) =>
                   // UNSAT, valid program
                   debug("Found valid program!")
-                  return Right(Solution(BooleanLiteral(true), Set(), outerSol, true))
+                  return Right(Stream(currentSolution(true)))
 
                 case None =>
                   debug("Found a non-verifiable solution...")
-                  if (useOptTimeout) {
-                    // Optimistic valid solution
-                    best = Some(Solution(BooleanLiteral(true), Set(), outerSol, false))
-                  }
+                  // Optimistic valid solution
+                  best +:= currentSolution(false)
               }
             } finally {
               solverf.reclaim(solver)
@@ -573,11 +572,13 @@ abstract class CEGISLike(name: String) extends Rule(name) {
           }
         }
 
-        best.map{ sol =>
+        if (useOptTimeout && best.nonEmpty) {
           // Interpret timeout in CE search as "the candidate is valid"
-          info("CEGIS could not prove the validity of the resulting expression")
-          Right(sol)
-        }.getOrElse(Left(cexs))
+          info(s"CEGIS could not prove the validity of the resulting ${best.size} expression(s)")
+          Right(best.toStream)
+        } else {
+          Left(cexs)
+        }
       }
 
       def allProgramsClosed = prunedPrograms.isEmpty
@@ -825,7 +826,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
 
             def nPassing = ndProgram.prunedPrograms.size
 
-            def programsReduced() = nPassing <= 10 || nInitial / nPassing > testReductionRatio
+            def programsReduced() = nPassing <= 10 || (nPassing <= 100 && nInitial / nPassing > testReductionRatio)
             gi.canGrow = programsReduced
 
             def allInputExamples() = {
@@ -904,9 +905,9 @@ abstract class CEGISLike(name: String) extends Rule(name) {
                 val programsToValidate = ndProgram.prunedPrograms
                 debug(s"Will send ${programsToValidate.size} program(s) to validate individually")
                 ndProgram.validatePrograms(programsToValidate) match {
-                  case Right(sol) =>
+                  case Right(sols) =>
                     // Found solution! Exit CEGIS
-                    result = Some(RuleClosed(sol))
+                    result = Some(RuleClosed(sols))
                   case Left(cexs) =>
                     debug(s"Found cexs! $cexs")
                     // Found some counterexamples