diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 3c99385712e6a163aa0454defeaa5dc10a554b3f..6cc38396dc9c287f2be19670b7bce10a2532424a 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -14,7 +14,7 @@ import scala.concurrent.duration._
 
 import ExecutionContext.Implicits.global
 
-class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, solvers: Seq[SolverFactory[S]])
+class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, val solvers: Seq[SolverFactory[S]])
         extends Solver with Interruptible {
 
   val name = "Pfolio"
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index dbaa76433c0fb2c6cafaa3cf0c3947feb4b5b7dd..01bfc5ec2037528f1e92188f6b4b41c6b2093ee1 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -9,6 +9,7 @@ import purescala.ExprOps._
 import scala.concurrent.duration._
 
 import solvers._
+import solvers.combinators.PortfolioSolver
 import solvers.smtlib.SMTLIBCVC4QuantifiedSolver
 
 object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
@@ -33,10 +34,17 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
         baseSolverF
     }
 
-    val isSMTQuantified = {
-      val solver = baseSolverF.getNewSolver
-      val res = solver.isInstanceOf[SMTLIBCVC4QuantifiedSolver]
-      solver.free
+    def isSMTQuantified[S <: Solver](sf: SolverFactory[S]): Boolean = {
+      val solver: S = sf.getNewSolver()
+      val res = solver match {
+        case _ : SMTLIBCVC4QuantifiedSolver =>
+          true
+        case ps: PortfolioSolver[_] =>
+          ps.solvers exists isSMTQuantified
+        case _ =>
+          false
+      }
+      solver.free()
       res
     }
 
@@ -45,7 +53,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
     reporter.debug("Generating Verification Conditions...")
 
     try { 
-      val vcs = generateVCs(vctx, filterFuns, forceGrouped = isSMTQuantified)
+      val vcs = generateVCs(vctx, filterFuns, forceGrouped = isSMTQuantified(baseSolverF))
 
       reporter.debug("Checking Verification Conditions...")