From 44fad5669b6fcd89348aa5af74086c72eed3fcbf Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 15 Nov 2012 19:38:47 +0100
Subject: [PATCH] Flip answer when needed
---
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 11 ++++++++---
1 file changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index c2b236bce..b9090d50f 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -139,7 +139,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
})
}
- def solve(vc: Expr) = decide(vc, true)
+ override def solve(vc: Expr) = decide(vc, true)
override def solveSAT(vc : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
restartZ3
@@ -458,8 +458,13 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
if(forceStop) {
(None, Map.empty, Set.empty)
} else {
- assert(foundDefinitiveAnswer)
- (definitiveAnswer, definitiveModel, definitiveCore)
+ val realAnswer = if(forValidity) {
+ definitiveAnswer
+ } else {
+ definitiveAnswer.map(!_)
+ }
+
+ (realAnswer, definitiveModel, definitiveCore)
}
}
--
GitLab