Simlify check/getModel in ProofSolver

In case of PortfolioSolver, the Exception should be handled correctly
through Future magic

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
   }
 

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

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"