Fix parallel search with FairZ3Solver

src/main/scala/leon/synthesis/Heuristics.scala

@@ -23,15 +23,19 @@ trait Heuristic {
 
 object HeuristicStep {
   def verifyPre(sctx: SynthesisContext, problem: Problem)(s: Solution): Solution = {
-    sctx.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
-      case (Some(true), model) =>
-        sctx.reporter.warning("Heuristic failed to produce weakest precondition:")
-        sctx.reporter.warning(" - problem: "+problem)
-        sctx.reporter.warning(" - precondition: "+s.pre)
-        s
-      case _ =>
-        s
-    }
+    //sctx here is unsafe to use in parallel. onSuccess should take a sctx for
+    //this to be possible
+
+    //sctx.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
+    //  case (Some(true), model) =>
+    //    sctx.reporter.warning("Heuristic failed to produce weakest precondition:")
+    //    sctx.reporter.warning(" - problem: "+problem)
+    //    sctx.reporter.warning(" - precondition: "+s.pre)
+    //    s
+    //  case _ =>
+    //    s
+    //}
+    s
   }
 
   def apply(sctx: SynthesisContext, problem: Problem, subProblems: List[Problem], onSuccess: List[Solution] => Solution) = {

src/main/scala/leon/synthesis/ParallelSearch.scala

@@ -28,15 +28,19 @@ class ParallelSearch(synth: Synthesizer,
 
     t.app.apply(sctx) match {
       case RuleSuccess(sol) =>
-        info(prefix+"Got: "+t.problem)
-        info(prefix+"Solved with: "+sol)
+        synth.synchronized {
+          info(prefix+"Got: "+t.problem)
+          info(prefix+"Solved with: "+sol)
+        }
 
         ExpandSuccess(sol)
       case RuleDecomposed(sub, onSuccess) =>
-        info(prefix+"Got: "+t.problem)
-        info(prefix+"Decomposed into:")
-        for(p <- sub) {
-          info(prefix+" - "+p)
+        synth.synchronized {
+          info(prefix+"Got: "+t.problem)
+          info(prefix+"Decomposed into:")
+          for(p <- sub) {
+            info(prefix+" - "+p)
+          }
         }
 
         Expanded(sub.map(TaskTryRules(_)))