From 594c86f324c264efcd38458fe28740423dde36d3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 6 May 2015 15:58:22 +0200
Subject: [PATCH] Only getModel if the solver returns SAT, not all solvers
support models
---
.../scala/leon/solvers/combinators/PortfolioSolver.scala | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 0e4578928..f15d2180a 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -34,7 +34,13 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
// solving
val fs = solversInsts.map { s =>
Future {
- (s, s.check, s.getModel)
+ val result = s.check
+ val model: Map[Identifier, Expr] = if (result == Some(true)) {
+ s.getModel
+ } else {
+ Map()
+ }
+ (s, result, model)
}
}
--
GitLab