From 73ce19e64455b19931c2f8552ee4e02401da4bde Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 26 May 2015 12:52:00 +0200
Subject: [PATCH] Portfolio should implement assertVC
---
.../scala/leon/solvers/combinators/PortfolioSolver.scala | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index d70294e04..3c9938571 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -6,6 +6,7 @@ package combinators
import purescala.Common._
import purescala.Expressions._
+import verification.VC
import utils.Interruptible
import scala.concurrent._
@@ -27,6 +28,10 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
solversInsts.foreach(_.assertCnstr(expression))
}
+ override def assertVC(vc: VC): Unit = {
+ solversInsts.foreach(_.assertVC(vc))
+ }
+
def check: Option[Boolean] = {
modelMap = Map()
--
GitLab