Remove deprecated accesses, update scalaz3, improve cancellation

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
     }
 

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

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