diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 6cc38396dc9c287f2be19670b7bce10a2532424a..5bb6d94719220d69ca238028374e4d3a72bffc9f 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -61,9 +61,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
         None
     }
 
-    // Block until all solvers finished
-    Await.result(Future.fold(fs)(0){ (i, r) => i+1 }, 10.days)
-
+    fs map { Await.ready(_, 10.days) }
     res
   }
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index e02c0dfc9a1f454003200a0d717211e061a659d6..3684d61bf14cefe200d07e729e9ea5ba96cf0ee3 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -37,22 +37,8 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
 
   // This solver does not support model extraction
   override def getModel: Map[Identifier, Expr] = {
-    reporter.warning(s"Solver $name does not support model extraction.")
-    Map()
-  }
-
-  // FIXME: mk: This is kind of hiding the problem under the carpet.
-  // We could just return an empty counterexample, but this breaks PortfolioSolver
-  override def check: Option[Boolean] = {
-    super.check match {
-      case Some(true) =>
-        reporter.warning(s"Solver $name found a counterexample, " +
-          "but masking it as unknown because counterexamples are not supported."
-        )
-        None
-      case other =>
-        other
-    }
+    // We don't send the error through reporter because it may be caught by PortfolioSolver
+    throw LeonFatalError(Some(s"Solver $name does not support model extraction."))
   }
 
   protected val allowQuantifiedAssersions: Boolean = true
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 2975fef1931aae92d3b03826a483015dee4c5475..92ae2308d2da1fd33c5e6065b6d2bddc44d94c02 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -9,8 +9,6 @@ import purescala.ExprOps._
 import scala.concurrent.duration._
 
 import solvers._
-import solvers.combinators.PortfolioSolver
-import solvers.smtlib.SMTLIBCVC4QuantifiedSolver
 
 object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
   val name = "Analysis"