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

@@ -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)) =>

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)