diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index f42d6ed34b6d60402a4d8b065bc1e747c2da4d09..d6c15b2693114313f959f61c9511271d57b17008 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/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
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index e35dc8815d1587ecfacb60581df7367123bccbbe..95d89c73d68fd4b93639c0c774a3a14f8481624c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/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)