Implement solveSATWithCores

src/main/scala/leon/solvers/Solver.scala

@@ -33,6 +33,15 @@ abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
     }
   }
 
+  def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
+    solveSAT(And(expression +: assumptions.toSeq)) match {
+      case (Some(false), _) =>
+        (Some(false), Map(), assumptions)
+      case (r, m) =>
+        (r, m, Set())
+    }
+  }
+
   def superseeds : Seq[String] = Nil
 
   private var _forceStop = false

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -161,6 +161,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
     }
   }
 
+  override def solveSATWithCores(expression: Expr, assumptions: Set[Expr]): (Option[Boolean], Map[Identifier, Expr], Set[Expr]) = {
+    restartZ3
+    decideWithModel(expression, false, None, Some(assumptions))
+  }
+
   private[this] def decideWithModel(vc: Expr, forValidity: Boolean, evaluator: Option[(Map[Identifier,Expr]) => Boolean] = None, assumptions: Option[Set[Expr]] = None): (Option[Boolean], Map[Identifier,Expr], Set[Expr]) = {
     val initializationStopwatch = new Stopwatch("init",               false)
     val blocking2Z3Stopwatch    = new Stopwatch("blocking-set-to-z3", false)