diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala index 8ec0984ee1994371ad95a95b7367887c923d2ff5..88d696f5bd41c4fe5091c1bc51ba1921ca6201fc 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) {