diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index d6c15b2693114313f959f61c9511271d57b17008..947f4ce28b3d6e93a73ecec6875decddf7658a97 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -20,15 +20,13 @@ abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
   // should halt as soon as possible with any result (Unknown is ok) as soon as forceStop is true
   def solve(expression: Expr) : Option[Boolean]
 
-  def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = (solve(expression), Map.empty)
-
   def solveSAT(expression: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
-    solveOrGetCounterexample(Not(expression)) match {
-      case (Some(true), _) =>
+    solve(Not(expression)) match {
+      case Some(true) =>
         (Some(false), Map())
-      case (Some(false), model) =>
-        (Some(true), model)
-      case (None, _) =>
+      case Some(false) =>
+        (Some(true), Map())
+      case None =>
         (None, Map())
     }
   }
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 95d89c73d68fd4b93639c0c774a3a14f8481624c..c2b236bce67ae8c7187da56373dd56b885df503f 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -141,9 +141,9 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
 
   def solve(vc: Expr) = decide(vc, true)
 
-  override def solveOrGetCounterexample(vc : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
+  override def solveSAT(vc : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
     restartZ3
-    val (res, model, core) = decideWithModel(vc, true)
+    val (res, model, core) = decideWithModel(vc, false)
     (res, model)
   }
 
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 0100286d6446b96173fa7e2c0b1d7b8d49ceeb9f..2e2a7cf6f8bb02e4fe6bc966da4d92c31590f91b 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -51,26 +51,26 @@ class UninterpretedZ3Solver(reporter : Reporter) extends Solver(reporter) with A
   protected[leon] def functionDeclToDef(decl: Z3FuncDecl) : FunDef = reverseFunctionMap(decl)
   protected[leon] def isKnownDecl(decl: Z3FuncDecl) : Boolean = reverseFunctionMap.isDefinedAt(decl)
 
-  override def solve(expression: Expr) : Option[Boolean] = solveOrGetCounterexample(expression)._1
+  override def solve(expression: Expr) : Option[Boolean] = solveSAT(Not(expression))._1.map(!_)
 
   // Where the solving occurs
-  override def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
+  override def solveSAT(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
     restartZ3
 
     val emptyModel    = Map.empty[Identifier,Expr]
     val unknownResult = (None, emptyModel)
-    val validResult   = (Some(true), emptyModel)
+    val unsatResult   = (Some(false), emptyModel)
 
     val result = toZ3Formula(expression).map { asZ3 => 
-      z3.assertCnstr(z3.mkNot(asZ3))
+      z3.assertCnstr(asZ3)
       z3.checkAndGetModel() match {
-        case (Some(false), _) => validResult
+        case (Some(false), _) => unsatResult
         case (Some(true), model) => {
           if(containsFunctionCalls(expression)) {
             unknownResult
           } else { 
             val variables = variablesOf(expression)
-            val r = (Some(false), modelToMap(model, variables))
+            val r = (Some(true), modelToMap(model, variables))
             model.delete
             r
           }