Skip to content
Snippets Groups Projects
Commit 73ce19e6 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Portfolio should implement assertVC

parent ee367ec7
No related branches found
No related tags found
No related merge requests found
...@@ -6,6 +6,7 @@ package combinators ...@@ -6,6 +6,7 @@ package combinators
import purescala.Common._ import purescala.Common._
import purescala.Expressions._ import purescala.Expressions._
import verification.VC
import utils.Interruptible import utils.Interruptible
import scala.concurrent._ import scala.concurrent._
...@@ -27,6 +28,10 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, ...@@ -27,6 +28,10 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
solversInsts.foreach(_.assertCnstr(expression)) solversInsts.foreach(_.assertCnstr(expression))
} }
override def assertVC(vc: VC): Unit = {
solversInsts.foreach(_.assertVC(vc))
}
def check: Option[Boolean] = { def check: Option[Boolean] = {
modelMap = Map() modelMap = Map()
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment