From a2479356a4dc92d8c0a5b847301e361c5a54cd52 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Thu, 20 Dec 2012 20:44:06 +0100
Subject: [PATCH] Displaying counter-examples.
FairZ3Solver no longer displays counter-examples. As a result, they were
not shown when doing verification. The fix is to have AnalysisPhase
display the counter-examples when it wants to.
---
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 3 +--
src/main/scala/leon/verification/AnalysisPhase.scala | 7 +++++--
2 files changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 517080077..3523e1ce7 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -159,8 +159,7 @@ class FairZ3Solver(context : LeonContext)
evalResult match {
case EvaluationSuccessful(BooleanLiteral(true)) =>
- reporter.info("- Model validated:")
- reporter.info(modelAsString)
+ reporter.info("- Model validated.")
(true, asMap)
case EvaluationSuccessful(BooleanLiteral(false)) =>
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 07fe90ae7..2e340cac1 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -109,7 +109,9 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val t1 = System.nanoTime
se.init()
- val solverResult = se.solve(vc)
+ val (satResult, counterexample) = se.solveSAT(Not(vc))
+ val solverResult = satResult.map(!_)
+
val t2 = System.nanoTime
val dt = ((t2 - t1) / 1000000) / 1000.0
@@ -125,8 +127,9 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
true
}
case Some(false) => {
+ reporter.error("Found counter-example : ")
+ reporter.error(counterexample.toSeq.sortBy(_._1.name).map(p => p._1 + " -> " + p._2).mkString("\n"))
reporter.error("==== INVALID ====")
-
vcInfo.value = Some(false)
vcInfo.solvedWith = Some(se)
vcInfo.time = Some(dt)
--
GitLab