diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 3646cc2d8dd25dd36fad975dfacff9043ab0f6ce..70368d7c86d0a2a9a5ff5e9e57cf132601f29d63 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/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) {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 5a61217a0db7614fb272964263f159fd0bd6ab34..48f38675a6cd91181ce8163ed3b7453c8484eda2 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/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()
+        }
       }
     }
 
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index bf3fed4e9049015daa4668a8480f708eb27a0845..e8d402b4f346801b463924242a9223658ff3f566 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/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))