From 4ca7538c55fdc094d44a73f505326d3dd9c07ea8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 5 Jun 2012 13:07:57 +0200
Subject: [PATCH] more debug messages
---
src/main/scala/leon/FairZ3Solver.scala | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 8ec0984ee..88d696f5b 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -631,6 +631,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
case (Some(true), m) => { // SAT
validatingStopwatch.start
+ Logger.debug("Model Found: " + m, 4, "z3solver")
val (trueModel, model) = if(Settings.verifyModel)
validateAndDeleteModel(m, toCheckAgainstModels, varsInVC, evaluator)
else {
@@ -686,6 +687,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
foundAnswer(Some(true))
} else {
luckyStopwatch.start
+ Logger.debug("Model Found: " + m2, 4, "z3solver")
// we might have been lucky :D
val (wereWeLucky, cleanModel) = validateAndDeleteModel(m2, toCheckAgainstModels, varsInVC, evaluator)
if(wereWeLucky) {
--
GitLab