diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index e80100f78e7d9c83d47d090b885a3b9af3a75431..f72b889209512be5606abcd3d19f900188ee23a7 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -78,9 +78,13 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
                   case NotValid(_, ces) if !ces.isEmpty =>
                     reporter.error("I ended up finding this counter example:\n"+ces.mkString("  |  "))
     
-                  case _ =>
+                  case NotValid(_, _) =>
                     solutions ::= sol
-                    reporter.info("Solution was not trusted but verification passed!")
+                    reporter.warning("Solution is not trusted!")
+
+                  case Valid =>
+                    solutions ::= sol
+                    reporter.info("Solution was not trusted but post-validation passed!")
                 }
               } else {
                 reporter.info("Found trusted solution!")
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index dcc7cad3fee9a039533cf94aea017fd14744545d..622ab658d15b0dbb90cedf2de8c3081b89d5cfc5 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -403,7 +403,14 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
                   return Left(Stream(Solution(BooleanLiteral(true), Set(), sol, true)))
 
                 case None =>
-                  None
+                  if (useOptTimeout) {
+                    // Interpret timeout in CE search as "the candidate is valid"
+                    sctx.reporter.info("CEGIS could not prove the validity of the resulting expression")
+                    // Optimistic valid solution
+                    return Left(Stream(Solution(BooleanLiteral(true), Set(), sol, false)))
+                  } else {
+                    None
+                  }
               }
             } finally {
               solver.free