Reintroduce luckytests fix two problems arising from parallelism of task dispatching

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -447,7 +447,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
                   foundAnswer(Some(false), core = z3CoreToCore(solver.getUnsatCore))
                 case Some(true) =>
                   //reporter.info("SAT WITHOUT Blockers")
-                  if (Settings.luckyTest && !forceStop && false) {
+                  if (Settings.luckyTest && !forceStop) {
                     // we might have been lucky :D
                     val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
                     if(wereWeLucky) {

src/main/scala/leon/synthesis/search/AndOrGraph.scala

@@ -142,15 +142,19 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S](val root: OT, val cos
     }
 
     def unsolvable(l: AndTree) {
-      triedAlternatives += l.task -> alternatives(l.task)
-      alternatives -= l.task
-
-
-      if (alternatives.isEmpty) {
-        isUnsolvable = true
-        parent.unsolvable(this)
-      } else {
-        updateMin()
+      if (alternatives contains l.task) {
+        triedAlternatives += l.task -> alternatives(l.task)
+        alternatives -= l.task
+
+
+        if (alternatives.isEmpty) {
+          isUnsolvable = true
+          if (parent ne null) {
+            parent.unsolvable(this)
+          }
+        } else {
+          updateMin()
+        }
       }
     }
 

src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala

@@ -15,7 +15,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
 
     def collectFromAnd(at: g.AndTree, costs: List[Int]) {
       val newCosts = at.minCost.value :: costs
-      if (!at.isSolved) {
+      if (!at.isSolved && !at.isUnsolvable) {
         at match {
           case l: g.Leaf =>
             collectLeaf(WL(l, newCosts.reverse)) 
@@ -30,7 +30,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
     def collectFromOr(ot: g.OrTree, costs: List[Int]) {
       val newCosts = ot.minCost.value :: costs
 
-      if (!ot.isSolved) {
+      if (!ot.isSolved && !ot.isUnsolvable) {
         ot match {
           case l: g.Leaf =>
             collectLeaf(WL(l, newCosts.reverse))