API for telling which solver solved (for portfolio)

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()
 

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 =>

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 {