From d91f2517f6d54f1ee08d988e81a5f718c735ed58 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 15 Nov 2012 21:26:00 +0100
Subject: [PATCH] Yay cores!
---
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index b9090d50f..68efe5d24 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -326,14 +326,20 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
// we need the model to perform the additional test
reporter.info(" - Running search without blocked literals (w/ lucky test)")
secondZ3SearchStopwatch.start
- val (result2,m2) = assumptionsAsZ3 match {
- case Some(as) => val res = z3.checkAssumptions(as: _*); (res._1, res._2)
- case None => z3.checkAndGetModel()
+ val (result2,m2,c2) = assumptionsAsZ3 match {
+ case Some(as) => z3.checkAssumptions(as: _*)
+ case None => val res = z3.checkAndGetModel(); (res._1, res._2, Seq.empty[Z3AST])
}
secondZ3SearchStopwatch.stop
reporter.info(" - Finished search without blocked literals")
if (result2 == Some(false)) {
+ val core: Set[Expr] = c2.map(ast => fromZ3Formula(m, ast, Some(BooleanType)) match {
+ case n @ Not(Variable(_)) => n
+ case v @ Variable(_) => v
+ case _ => scala.sys.error("Impossible element extracted from core: " + ast)
+ }).toSet
+
foundAnswer(Some(true), core = core)
} else {
luckyStopwatch.start
--
GitLab