From c372e65915855b40e4f867cf70749cdbfdda866b Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Thu, 29 Nov 2012 23:36:10 +0100 Subject: [PATCH] Bleh --- src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala index 20fa8cc8e..f1e11303b 100644 --- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala @@ -732,13 +732,13 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ val blockingSetAsZ3 : Seq[Z3AST] = blockingSet.toSeq.map(toZ3Formula(_).get) // println("Blocking set : " + blockingSet) - solver.push - if(!blockingSetAsZ3.isEmpty) - solver.assertCnstr(z3.mkAnd(blockingSetAsZ3 : _*)) + solver.push() + for (block <- blockingSetAsZ3) { + solver.assertCnstr(block) + } reporter.info(" - Running Z3 search...") - val res = solver.checkAssumptions(assumptionsAsZ3 :_*) reporter.info(" - Finished search with blocked literals") @@ -785,6 +785,7 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ val core = z3CoreToCore(solver.getUnsatCore) + // Removes blocking literals solver.pop(1) if (!forceStop) { @@ -805,7 +806,8 @@ class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ // we might have been lucky :D val (wereWeLucky, cleanModel) = validateAndDeleteModel(solver.getModel, toCheckAgainstModels, varsInVC) if(wereWeLucky) { - reporter.info("Found lucky to "+solver.getAssertions.toSeq+" with "+assumptions) + reporter.info("Found lucky to "+solver.getAssertions.toSeq+" with "+assumptionsAsZ3) + reporter.info("Stack: "+ownStack) foundAnswer(Some(true), cleanModel) } } -- GitLab