diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index bce3e3bb1fed5b693cfa263b46b35b9d2aecc3a0..448f42c252342fb887e4ed5172d38db916ca4886 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -391,8 +391,15 @@ class FairZ3Solver(context : LeonContext)
       frameExpressions = Nil :: frameExpressions
     }
 
+    override def init() {
+      FairZ3Solver.super.init
+    }
+
     def halt() {
-      z3.interrupt
+      FairZ3Solver.super.halt
+      if(z3 ne null) {
+        z3.interrupt
+      }
     }
 
     def pop(lvl: Int = 1) {
@@ -590,6 +597,7 @@ class FairZ3Solver(context : LeonContext)
                   }
 
                 case None =>
+                  foundAnswer(None)
               }
             }
 
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 1bdf8d1cfb68026d0257d74e189752ae15949a33..296d4ef401007d165f0f6e9d6b59790a3f6ba2e6 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -557,8 +557,12 @@ case object CEGIS extends Rule("CEGIS") {
                                 // the assumptions are.
                                 solver1.getUnsatCore
 
-                              case _ =>
+                              case Some(true) =>
+                                // Can't be!
                                 bssAssumptions
+
+                              case None =>
+                                return RuleApplicationImpossible
                             }
 
                             solver1.pop()
@@ -602,10 +606,7 @@ case object CEGIS extends Rule("CEGIS") {
                           result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), expr)))
 
                         case _ =>
-                          if (!sctx.shouldStop.get) {
-                            sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
-                          }
-                          needMoreUnrolling = true
+                          return RuleApplicationImpossible
                       }
                     }
 
@@ -617,7 +618,7 @@ case object CEGIS extends Rule("CEGIS") {
                       solver1.check match {
                         case Some(false) =>
                           // Unsat even without blockers (under which fcalls are then uninterpreted)
-                          result = Some(RuleApplicationImpossible)
+                          return RuleApplicationImpossible
 
                         case _ =>
                       }
@@ -626,11 +627,8 @@ case object CEGIS extends Rule("CEGIS") {
                     needMoreUnrolling = true
 
                   case _ =>
-                    if (!sctx.shouldStop.get) {
-                      sctx.reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
-                    }
                     //println("%%%% WOOPS")
-                    needMoreUnrolling = true
+                    return RuleApplicationImpossible
                 }
               }