More reliable shutdown

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("?"))
 

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 {

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
+        }
 
     }
   }

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
   }
 }