diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index daf7b84999f46bd6ebcd647e86477d5e383f18ff..69eef744946d8ca3435feb2e315bde2dc135d5b3 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -21,6 +21,7 @@ trait Solver {
 
   def check: Option[Boolean]
   def getModel: Map[Identifier, Expr]
+  def getResultSolver: Option[Solver] = Some(this)
 
   def free()
 
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 5bb6d94719220d69ca238028374e4d3a72bffc9f..1f990a0c5336193643460d840f42217f397adc88 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -23,6 +23,9 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
 
   protected var modelMap = Map[Identifier, Expr]()
   protected var solversInsts: Seq[S] = solvers.map(_.getNewSolver())
+  protected var resultSolver: Option[Solver] = None
+
+  override def getResultSolver = resultSolver
 
   def assertCnstr(expression: Expr): Unit = {
     solversInsts.foreach(_.assertCnstr(expression))
@@ -54,7 +57,10 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
     val res = Await.result(result, 10.days) match {
       case Some((s, r, m)) =>
         modelMap = m
-        context.reporter.debug("Solved with "+s.name)
+        resultSolver = s.getResultSolver
+        resultSolver.foreach { solv =>
+          context.reporter.debug("Solved with "+solv)
+        }
         solversInsts.foreach(_.interrupt())
         r
       case None =>
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 3fbc3671e7b47bfe24392da109f51c3b0b3152e8..e8b3b39f3ba1599bd7d3b0e3dcb4822636247b89 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -161,10 +161,10 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
           VCResult(status, Some(s), Some(dt))
 
         case Some(false) =>
-          VCResult(VCStatus.Valid, Some(s), Some(dt))
+          VCResult(VCStatus.Valid, s.getResultSolver, Some(dt))
 
         case Some(true) =>
-          VCResult(VCStatus.Invalid(s.getModel), Some(s), Some(dt))
+          VCResult(VCStatus.Invalid(s.getModel), s.getResultSolver, Some(dt))
       }
 
       reporter.synchronized {