diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index f91fa5d2e2005c00359391862f3963dd080fa6d6..3646cc2d8dd25dd36fad975dfacff9043ab0f6ce 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -432,7 +432,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ
             reporter.info("UNSAT BECAUSE: "+core.mkString(" AND "))
 
             if (!forceStop) {
-              if (Settings.luckyTest) {
+              if (Settings.luckyTest && false) {
                 // we need the model to perform the additional test
                 reporter.info(" - Running search without blocked literals (w/ lucky test)")
               } else {
@@ -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) {
+                  if (Settings.luckyTest && !forceStop && false) {
                     // we might have been lucky :D
                     val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, entireFormula, varsInVC)
                     if(wereWeLucky) {
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index 0c48bd42a1cb331b4c4ceabee03e50d149f7fe90..befe0ee2a733714dc7cb68b81eb8f58b3ca32443 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -20,7 +20,7 @@ class ParallelSearch(synth: Synthesizer,
 
     solver.initZ3
 
-    SynthesisContext(solver = solver, reporter = synth.reporter)
+    SynthesisContext(solver = solver, reporter = synth.reporter, shouldStop = synth.shouldStop)
   }
 
   def expandAndTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskRunRule) = {
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 831bd545081588569548ac0d5d6b06ed17d3b505..d23f4df29b7b07473518104988e35a57c280e43c 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -3,12 +3,15 @@ package synthesis
 
 import solvers.Solver
 
+import java.util.concurrent.atomic.AtomicBoolean
+
 case class SynthesisContext(
   solver: Solver,
-  reporter: Reporter
+  reporter: Reporter,
+  shouldStop: AtomicBoolean
 )
 
 object SynthesisContext {
-  def fromSynthesizer(synth: Synthesizer) = SynthesisContext(synth.solver, synth.reporter)
+  def fromSynthesizer(synth: Synthesizer) = SynthesisContext(synth.solver, synth.reporter, new AtomicBoolean(false))
 }
 
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index ccf4be6d12f19de9e5abe39ddf00a3a5e6c638d6..aa054774a52953451b515645d10c1706d85e5c58 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -15,6 +15,8 @@ import collection.mutable.PriorityQueue
 
 import synthesis.search._
 
+import java.util.concurrent.atomic.AtomicBoolean
+
 class Synthesizer(val context : LeonContext,
                   val solver: Solver,
                   val program: Program,
@@ -26,7 +28,7 @@ class Synthesizer(val context : LeonContext,
 
   import reporter.{error,warning,info,fatalError}
 
-  var continue = true
+  var shouldStop = new AtomicBoolean(false)
 
   def synthesize(): (Solution, Boolean) = {
 
@@ -43,7 +45,7 @@ class Synthesizer(val context : LeonContext,
         println
         reporter.info("Aborting...")
 
-        continue = false
+        shouldStop.set(true)
         search.stop()
 
         Signal.handle(sigINT, oldHandler)
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index c1029c5db50fa6de129b958276421972c1338597..6dd2b83b6ddba159e1981f16ab631d3df261de4e 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -163,7 +163,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
 
               //println("Unrolling #"+unrolings+" bss size: "+bss.size)
 
-              while (result.isEmpty && continue) {
+              while (result.isEmpty && continue && !sctx.shouldStop.get) {
                 //println("Looking for CE...")
                 //println("-"*80)
                 //println(basePhi)
@@ -262,7 +262,7 @@ case object CEGIS extends Rule("CEGIS", 150) {
               }
 
               unrolings += 1
-            } while(unrolings < maxUnrolings && result.isEmpty)
+            } while(unrolings < maxUnrolings && result.isEmpty && !sctx.shouldStop.get)
 
             result.getOrElse(RuleApplicationImpossible)
 
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index a9a3201aed8d3694a2fd715da6b1792bc3ed0746..d0f32ccee0de188790f03bdbf578bd0d3a44c51d 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -4,6 +4,7 @@ import akka.actor._
 import akka.util.duration._
 import akka.util.Timeout
 import akka.pattern.ask
+import akka.pattern.AskTimeoutException
 import akka.dispatch.Await
 
 abstract class AndOrGraphParallelSearch[WC,
@@ -27,7 +28,11 @@ abstract class AndOrGraphParallelSearch[WC,
       system.actorOf(Props(new Worker(master)), name = "Worker"+i)
     }
 
-    Await.result(master.ask(Protocol.BeginSearch)(timeout), timeout)
+    try {
+      Await.result(master.ask(Protocol.BeginSearch)(timeout), timeout)
+    } catch {
+      case e: AskTimeoutException =>
+    }
 
     if (system ne null) {
       system.shutdown
@@ -92,8 +97,6 @@ abstract class AndOrGraphParallelSearch[WC,
                 w ! RequestOrTask(ol.task)
             }
           }
-
-
       }
     }