diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 51708007722e5f815409ca338c896436915f0f0a..3523e1ce71703db35dd9346269dd284e5de91d42 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 07fe90ae734dfa094b51af55d48340295be80b78..2e340cac1e6f8db1abd2efef32e7ef27a147e8b7 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)