diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index d941f1c0edc81b9501eb557e87405e6b7add14fd..919a8c458de6a418a59518f7f269cd7feb106d7c 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -208,7 +208,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
       val report = VerificationPhase.checkVCs(
         vctx,
         vcs,
-        stopAfter = Some({ (vc, vr) => vr.isInvalid })
+        stopWhen = _.isInvalid
       )
 
       val vrs = report.vrs
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 50f2da1afa4481735cf214237997b473e9d89b3b..467ed7376173ad53475b838134f509a40e2fe5aa 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -3,6 +3,7 @@
 package leon
 package synthesis
 
+import leon.purescala.Expressions.Choose
 import purescala.Definitions._
 import purescala.ExprOps._
 import purescala.DefOps._
@@ -145,7 +146,7 @@ class Synthesizer(val context : LeonContext,
     try {
       val vctx = VerificationContext(context, npr, solverf, context.reporter)
       val vcs = generateVCs(vctx, fds)
-      val vcreport = checkVCs(vctx, vcs)
+      val vcreport = checkVCs(vctx, vcs, stopWhen = _.isInvalid)
 
       if (vcreport.totalValid == vcreport.totalConditions) {
         (sol, Some(true))
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index e9a9fe60122b40d29bc94d7b15c32a6db6995e8e..39ed875a056d3dcc189ab526302abc7569550085 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -95,7 +95,7 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
   def checkVCs(
     vctx: VerificationContext,
     vcs: Seq[VC],
-    stopAfter: Option[(VC, VCResult) => Boolean] = None
+    stopWhen: VCResult => Boolean = _ => false
   ): VerificationReport = {
     val interruptManager = vctx.context.interruptManager
 
@@ -107,14 +107,14 @@ object VerificationPhase extends SimpleLeonPhase[Program,VerificationReport] {
       for (vc <- vcs.par if !stop) yield {
         val r = checkVC(vctx, vc)
         if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
-        stop = stopAfter.exists(_(vc, r))
+        stop = stopWhen(r)
         vc -> Some(r)
       }
     } else {
       for (vc <- vcs.toSeq.sortWith((a,b) => a.fd.getPos < b.fd.getPos) if !interruptManager.isInterrupted && !stop) yield {
         val r = checkVC(vctx, vc)
         if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
-        stop = stopAfter.exists(_(vc, r))
+        stop = stopWhen(r)
         vc -> Some(r)
       }
     }