Improve how fails are handled by synthesis/repair

src/main/scala/leon/repair/Repairman.scala

@@ -65,10 +65,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
 
         try {
           reporter.info(ASCIIHelpers.title("3. Synthesizing repair"))
-          val (search, solutions) = synth.validate(synth.synthesize()) match {
-            case (search, sols) =>
-              (search, sols.collect { case (s, true) => s })
-          }
+          val (search, solutions) = synth.validate(synth.synthesize(), allowPartial = false)
 
           if (synth.settings.generateDerivationTrees) {
             val dot = new DotGenerator(search.g)
@@ -80,8 +77,8 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
           } else {
 
             reporter.info(ASCIIHelpers.title("Repair successful:"))
-            for ((sol, i) <- solutions.zipWithIndex) {
-              reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+":"))
+            for ( ((sol, isTrusted), i) <- solutions.zipWithIndex) {
+              reporter.info(ASCIIHelpers.subTitle("Solution "+(i+1)+ (if(isTrusted) "" else " (untrusted)" ) + ":"))
               val expr = sol.toSimplifiedExpr(ctx, synth.program)
               reporter.info(expr.asString(ctx))
             }
@@ -139,7 +136,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
     val timeoutMs = verifTimeoutMs.getOrElse(3000L)
     val solverf = SolverFactory.getFromSettings(ctx, program).withTimeout(timeoutMs)
     val vctx = VerificationContext(ctx, program, solverf, reporter)
-    val vcs = AnalysisPhase.generateVCs(vctx, Some(Seq(fd.id.name)))
+    val vcs = AnalysisPhase.generateVCs(vctx, Seq(fd))
 
     try {
       val report = AnalysisPhase.checkVCs(

src/main/scala/leon/synthesis/SynthesisPhase.scala

@@ -77,7 +77,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
 
     chooses.foreach { ci =>
       val synthesizer = new Synthesizer(ctx, p, ci, options)
-      val (search, solutions) = synthesizer.validate(synthesizer.synthesize())
+      val (search, solutions) = synthesizer.validate(synthesizer.synthesize(), true)
 
       try {
         val fd = ci.fd

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -48,7 +48,7 @@ class Synthesizer(val context : LeonContext,
     (s, sols)
   }
 
-  def validate(results: (Search, Stream[Solution])): (Search, Stream[(Solution, Boolean)]) = {
+  def validate(results: (Search, Stream[Solution]), allowPartial: Boolean): (Search, Stream[(Solution, Boolean)]) = {
     val (s, sols) = results
 
     val result = sols.map {
@@ -58,7 +58,7 @@ class Synthesizer(val context : LeonContext,
         validateSolution(s, sol, 5.seconds)
     }
 
-    (s, if (result.isEmpty) {
+    (s, if (result.isEmpty && allowPartial) {
       List((new PartialSolution(s.g, true).getSolution, false)).toStream
     } else {
       result
@@ -77,7 +77,7 @@ class Synthesizer(val context : LeonContext,
 
     try {
       val vctx = VerificationContext(context, npr, solverf, context.reporter)
-      val vcs = generateVCs(vctx, Some(fds.map(_.id.name)))
+      val vcs = generateVCs(vctx, fds)
       val vcreport = checkVCs(vctx, vcs)
 
       if (vcreport.totalValid == vcreport.totalConditions) {

src/main/scala/leon/verification/AnalysisPhase.scala

@@ -36,25 +36,6 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
 
     reporter.debug("Generating Verification Conditions...")
 
-    try { 
-      val vcs = generateVCs(vctx, filterFuns)
-
-      reporter.debug("Checking Verification Conditions...")
-
-      checkVCs(vctx, vcs)
-    } finally {
-      solverF.shutdown()
-    }
-  }
-
-  def generateVCs(vctx: VerificationContext, filterFuns: Option[Seq[String]]): Seq[VC] = {
-
-    import vctx.reporter
-    import vctx.program
-
-    val defaultTactic   = new DefaultTactic(vctx)
-    val inductionTactic = new InductionTactic(vctx)
-
     def excludeByDefault(fd: FunDef): Boolean = fd.annotations contains "library"
 
     val fdFilter = {
@@ -65,11 +46,29 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
 
     val toVerify = program.definedFunctions.filter(fdFilter).sortWith((fd1, fd2) => fd1.getPos < fd2.getPos)
 
-    val vcs = for(funDef <- toVerify) yield {
+    for(funDef <- toVerify) {
       if (excludeByDefault(funDef)) {
-        reporter.warning("Forcing verification of "+funDef.id.name+" which was assumed verified")
+        reporter.warning("Forcing verification of " + funDef.id.name + " which was assumed verified")
       }
+    }
+
+
+    try {
+      val vcs = generateVCs(vctx, toVerify)
+
+      reporter.debug("Checking Verification Conditions...")
+
+      checkVCs(vctx, vcs)
+    } finally {
+      solverF.shutdown()
+    }
+  }
 
+  def generateVCs(vctx: VerificationContext, toVerify: Seq[FunDef]): Seq[VC] = {
+    val defaultTactic   = new DefaultTactic(vctx)
+    val inductionTactic = new InductionTactic(vctx)
+
+    val vcs = for(funDef <- toVerify) yield {
       val tactic: Tactic =
         if (funDef.annotations.contains("induct")) {
           inductionTactic