diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 342cd06290c91646620ed341173938712940b666..23648ee3ff6fa1201917c7af5542fa214e2c762f 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -378,7 +378,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
       vctx, 
       vcs, 
       checkInParallel = true,
-      interruptOn = _.counterExample.isDefined 
+      stopAfter = _.counterExample.isDefined
     )
 
     val theVCs = vcs.getOrElse(fd, Nil)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index fbbacc65602604fc1fc6d99810ec5a2b405d03c2..484c9f3d44f8ee533c5f3949f672c449e889a45a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -11,6 +11,8 @@ abstract class SMTLIBSolver(val context: LeonContext,
                             val program: Program)
   extends IncrementalSolver with Interruptible with SMTLIBTarget {
 
+  context.interruptManager.registerForInterrupts(this)
+
   protected var interrupted = false
 
   override def interrupt(): Unit = {
@@ -31,6 +33,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
   override def free() = {
     interpreter.free()
+    context.interruptManager.unregisterForInterrupts(this)
     reporter.ifDebug { _ => out.close() }
   }
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index c0d799182d468ffba6e402f07067176cc3077b57..bea2751115a30daaa040246047aadfb05a4c5084 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -664,7 +664,7 @@ trait SMTLIBTarget {
     case CheckSatStatus(SatStatus)     => Some(true)
     case CheckSatStatus(UnsatStatus)   => Some(false)
     case CheckSatStatus(UnknownStatus) => None
-    case _                               => None
+    case _                             => None
   }
 
   override def getModel: Map[Identifier, Expr] = {
diff --git a/src/main/scala/leon/utils/InterruptManager.scala b/src/main/scala/leon/utils/InterruptManager.scala
index 753edf9a944c793e4f876002a2e6d1c8d6b28421..de0fafebeec40778ada713348a47f11852bac4b2 100644
--- a/src/main/scala/leon/utils/InterruptManager.scala
+++ b/src/main/scala/leon/utils/InterruptManager.scala
@@ -12,20 +12,43 @@ import java.util.WeakHashMap
 class InterruptManager(reporter: Reporter) extends Interruptible {
   private[this] val interruptibles = new WeakHashMap[Interruptible, Boolean]()
   private[this] val sigINT = new Signal("INT")
-  private[this] var oldHandler: SignalHandler = null
+  private[this] val withinTimeout: AtomicBoolean = new AtomicBoolean(false)
+  private[this] val handler = new SignalHandler {
+    def handle(sig: Signal) {
+      println()
+      if (withinTimeout.get()) {
+        reporter.warning("Aborting Leon...")
+        System.exit(1)
+      }
+      else {
+        reporter.warning("Interrupted...")
+        setTimeout()
+        interrupt()
+      }
+    }
+  }
+  private val exitWindow = 1000
+  private[this] def setTimeout() = {
+    import scala.concurrent.Future
+    import scala.concurrent.ExecutionContext.Implicits.global
+    withinTimeout.set(true)
+    Future { Thread.sleep(exitWindow) } onComplete { _ => withinTimeout.set(false) }
+    ()
+  }
 
   val interrupted: AtomicBoolean = new AtomicBoolean(false)
 
   @inline
-  def isInterrupted = interrupted.get()
+  def isInterrupted = interrupted.get
 
   def interrupt() = synchronized {
-    if (!interrupted.get()) {
+    if (!isInterrupted) {
       interrupted.set(true)
 
       val it = interruptibles.keySet.iterator
+
       for (i <- it) {
-         i.interrupt()
+        i.interrupt()
       }
     } else {
       reporter.warning("Already interrupted!")
@@ -33,7 +56,7 @@ class InterruptManager(reporter: Reporter) extends Interruptible {
   }
 
   def recoverInterrupt() = synchronized {
-    if (interrupted.get()) {
+    if (isInterrupted) {
       interrupted.set(false)
 
       val it = interruptibles.keySet.iterator
@@ -46,22 +69,18 @@ class InterruptManager(reporter: Reporter) extends Interruptible {
   }
 
   def registerForInterrupts(i: Interruptible) = synchronized {
-    if (interrupted.get) {
+    if (isInterrupted) {
       i.interrupt()
     }
     interruptibles.put(i, true)
   }
 
-  def registerSignalHandler() {
-    oldHandler = Signal.handle(sigINT, new SignalHandler {
-      def handle(sig: Signal) {
-        Signal.handle(sigINT, oldHandler)
-        println
-        reporter.warning("Aborting Leon...")
-
-        interrupt()
-
-      }
-    })
+  // We should not need this because keys should automatically be removed
+  // from the WeakHashMap when gc'ed.
+  // But let's have it anyway!
+  def unregisterForInterrupts(i: Interruptible) = synchronized {
+    interruptibles.remove(i)
   }
+
+  def registerSignalHandler() = Signal.handle(sigINT, handler)
 }
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index fb335abee94a1837f75c3244e01dbef01b05db56..056858e0da7e002bb0836eaad8df445f09662c51 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -69,7 +69,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
       vctx: VerificationContext, 
       vcs: Map[FunDef, List[VerificationCondition]], 
       checkInParallel: Boolean = false,
-      interruptOn : VerificationCondition => Boolean = { _ => false }
+      stopAfter : VerificationCondition => Boolean = { _ => false }
   ) : VerificationReport = {
     import vctx.reporter
     import vctx.solverFactory
@@ -143,21 +143,23 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
       }
     }
     
-    var interrupt = false 
+    var stop = false
     
     if (checkInParallel) {
       val allVCsPar = (for {(_, vcs) <- vcs.toSeq; vcInfo <- vcs} yield vcInfo).par
-      for (vc <- allVCsPar if !interruptManager.isInterrupted && !interrupt) {
+      for (vc <- allVCsPar if !stop) {
         checkVC(vc)
-        interrupt = interruptOn(vc)
+        if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
+        stop = stopAfter(vc)
       }
     } else {
       for {
         (funDef, vcs) <- vcs.toSeq.sortWith((a,b) => a._1.getPos < b._1.getPos)
-        vc <- vcs if !interruptManager.isInterrupted && !interrupt
+        vc <- vcs if !interruptManager.isInterrupted && !stop
       } {
         checkVC(vc)
-        interrupt = interruptOn(vc)
+        if (interruptManager.isInterrupted) interruptManager.recoverInterrupt()
+        stop = stopAfter(vc)
       }
     }