diff --git a/src/main/scala/leon/Extensions.scala b/src/main/scala/leon/Extensions.scala
index e9fdde89c3555b41b47b696c542733b0bf411830..53bd6f37e0f0d419acfe4f1d879cde7e85537244 100644
--- a/src/main/scala/leon/Extensions.scala
+++ b/src/main/scala/leon/Extensions.scala
@@ -1,5 +1,6 @@
 package leon
 
+import purescala.Common._
 import purescala.Trees._
 import purescala.Definitions._
 
@@ -20,6 +21,8 @@ object Extensions {
     // 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 isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
     def superseeds : Seq[String] = Nil
 
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 2c429bab38594f4109c467a89e62106d1cc60d6b..b54f5db1d9c7456dcda45756433167f8a0a7ebd4 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -478,6 +478,11 @@ 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]) = {
+    restartZ3
+    decideWithModel(vc, true)
+  }
+
   def solveWithBounds(vc: Expr, fv: Boolean) : (Option[Boolean], Map[Identifier,Expr]) = {
     restartZ3
     boundValues
diff --git a/src/main/scala/leon/TrivialSolver.scala b/src/main/scala/leon/TrivialSolver.scala
index 7e08c483237aa6649c9da425d6e0c58c7b9301aa..0b05bbb59ffdfcff30c623f18e66a1ba3eb4e101 100644
--- a/src/main/scala/leon/TrivialSolver.scala
+++ b/src/main/scala/leon/TrivialSolver.scala
@@ -18,5 +18,4 @@ class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
     case And(exs) if exs.contains(BooleanLiteral(false)) => Some(false)
     case _ => None
   }
-
 }