diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 62ee881093fcf5965ebed21bccf000334aeb0510..bdfb1b7878b216a265e43e7043cf7cd499ad3086 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -728,8 +728,8 @@ trait AbstractZ3Solver
             }
           }
 
-          case Z3NumeralAST(Some(v)) => IntLiteral(v)
-          case Z3NumeralAST(None) => {
+          case Z3NumeralIntAST(Some(v)) => IntLiteral(v)
+          case Z3NumeralIntAST(None) => {
             reporter.info("Cannot read exact model from Z3: Integer does not fit in machine word")
             reporter.info("Exiting procedure now")
             sys.exit(0)
@@ -774,7 +774,7 @@ trait AbstractZ3Solver
           }
         }
       }
-      case Z3NumeralAST(Some(v)) => IntLiteral(v)
+      case Z3NumeralIntAST(Some(v)) => IntLiteral(v)
       case _ => throw e
     }
 
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index b62c45e9788cb2831b0f3e37110fc8efa193bf6c..ae065bc4631060e6d804c29a1fdc583a9c7b2ee6 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -447,6 +447,8 @@ case object CEGIS extends Rule("CEGIS") {
         var baseExampleInputs: Seq[Seq[Expr]] = Seq()
 
         // We populate the list of examples with a predefined one
+        sctx.reporter.debug("Acquiring list of examples")
+
         if (p.pc == BooleanLiteral(true)) {
           baseExampleInputs = p.as.map(a => simplestValue(a.getType)) +: baseExampleInputs
         } else {
@@ -573,7 +575,7 @@ case object CEGIS extends Rule("CEGIS") {
             // We further filter the set of working programs to remove those that fail on known examples
             if (useCEPruning && hasInputExamples() && ndProgram.canTest()) {
 
-              for (p <- prunedPrograms) {
+              for (p <- prunedPrograms if !interruptManager.isInterrupted()) {
                 if (!allInputExamples().forall(ndProgram.testForProgram(p))) {
                   // This program failed on at least one example
                   solver1.assertCnstr(Not(And(p.map(Variable(_)).toSeq)))
@@ -752,6 +754,7 @@ case object CEGIS extends Rule("CEGIS") {
         } catch {
           case e: Throwable =>
             sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
+            e.printStackTrace
             RuleApplicationImpossible
         } finally {
           solver1.free()
diff --git a/src/main/scala/leon/utils/InterruptManager.scala b/src/main/scala/leon/utils/InterruptManager.scala
index d9a149aae6e668f35bcf94d7d0b301bb9d561989..79a799fac8ee905b50b7628f0087256d46f026d3 100644
--- a/src/main/scala/leon/utils/InterruptManager.scala
+++ b/src/main/scala/leon/utils/InterruptManager.scala
@@ -23,7 +23,10 @@ class InterruptManager(reporter: Reporter) {
     if (!interrupted.get()) {
       interrupted.set(true)
 
-      interruptibles.keySet.foreach(_.interrupt())
+      val it = interruptibles.keySet.iterator
+      for (i <- it) {
+         i.interrupt()
+      }
     } else {
       reporter.warning("Already interrupted!")
     }
@@ -33,7 +36,10 @@ class InterruptManager(reporter: Reporter) {
     if (interrupted.get()) {
       interrupted.set(false)
 
-      interruptibles.keySet.foreach(_.recoverInterrupt())
+      val it = interruptibles.keySet.iterator
+      for (i <- it) {
+         i.recoverInterrupt()
+      }
     } else {
       reporter.warning("Not interrupted!")
     }
@@ -46,12 +52,12 @@ class InterruptManager(reporter: Reporter) {
   def registerSignalHandler() {
     oldHandler = Signal.handle(sigINT, new SignalHandler {
       def handle(sig: Signal) {
+        Signal.handle(sigINT, oldHandler)
         println
-        reporter.info("Aborting...")
+        reporter.info("Aborting Leon...")
 
         interrupt()
 
-        Signal.handle(sigINT, oldHandler)
       }
     })
   }
diff --git a/unmanaged/64/scalaz3_2.10-2.0.jar b/unmanaged/64/scalaz3_2.10-2.0.jar
index 6f76dd893d73a076b90a13e438cb699fdf02c9a5..c276fb7f7e42b5aeab23f97ee0e94b2b7d44436d 100644
Binary files a/unmanaged/64/scalaz3_2.10-2.0.jar and b/unmanaged/64/scalaz3_2.10-2.0.jar differ