diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index befe0ee2a733714dc7cb68b81eb8f58b3ca32443..a6d436509f23a472fe111cd81311b893d696ddae 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -23,6 +23,11 @@ class ParallelSearch(synth: Synthesizer,
     SynthesisContext(solver = solver, reporter = synth.reporter, shouldStop = synth.shouldStop)
   }
 
+  override def stop() = {
+    synth.shouldStop.set(true)
+    super.stop()
+  }
+
   def expandAndTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskRunRule) = {
     val prefix = "[%-20s] ".format(Option(t.rule).getOrElse("?"))
 
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index bc254e2fa594e5e7a51d38c846e8000c95d444d0..88a51b8059d4e0508bfe4f50aa71235ead18b8c8 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -69,7 +69,7 @@ class SimpleSearch(synth: Synthesizer,
   }
 
   def search(): Option[Solution] = {
-    while (!g.tree.isSolved && !isStopped) {
+    while (!g.tree.isSolved) {
       nextLeaf() match {
         case Some(l)  =>
           l match {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index d0f32ccee0de188790f03bdbf578bd0d3a44c51d..0f126660e164b43d33726b01a03057af35c5fecd 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -14,7 +14,7 @@ abstract class AndOrGraphParallelSearch[WC,
 
   def initWorkerContext(w: ActorRef): WC
 
-  val nWorkers = 5
+  val nWorkers = 7
   val timeout = 600.seconds
 
   var system: ActorSystem = _
@@ -128,8 +128,10 @@ abstract class AndOrGraphParallelSearch[WC,
         sendWork()
 
       case Terminated(w) =>
-        processing -= workers(w).get
-        workers -= w
+        if (workers contains w) {
+          processing -= workers(w).get
+          workers -= w
+        }
 
     }
   }
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index 1291babe91f044a8cc4d37cdcc65019cf2713a54..bf3fed4e9049015daa4668a8480f708eb27a0845 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -60,10 +60,8 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
   case class ExpandSuccess[T <: AOTask[S]](sol: S) extends ExpandResult[T]
   case class ExpandFailure[T <: AOTask[S]]() extends ExpandResult[T]
 
-  var isStopped = false
-
   def stop() {
-    isStopped = true
+
   }
 
   def search(): Option[S]
@@ -79,6 +77,11 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
         al.isUnsolvable = true
         al.parent.unsolvable(al)
     }
+
+    if (g.tree.isSolved) {
+      stop()
+    }
+
     processing -= al
   }
 
@@ -93,6 +96,11 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
         ol.isUnsolvable = true
         ol.parent.unsolvable(ol)
     }
+
+    if (g.tree.isSolved) {
+      stop()
+    }
+
     processing -= ol
   }
 }