diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index d998013231be4548a885340fce579e39e09e40e9..69551967cd50aee4ed3929ed0349632a08ecd34e 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -22,6 +22,17 @@ abstract class Solver(val reporter: Reporter) extends Extension(reporter) {
 
   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), _) =>
+        (Some(false), Map())
+      case (Some(false), model) =>
+        (Some(true), model)
+      case (None, _) =>
+        (None, Map())
+    }
+  }
+
   def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
   def superseeds : Seq[String] = Nil
 
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 0e39e3f9cbf2c47c56addddca760a62d7fc6bcce..7ad623ec0b4a4be74ffc62781fe9aceebfef10e4 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -33,13 +33,13 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
 
       while (result.isEmpty && i < maxTries) {
         val phi = And(p.phi +: predicates)
-        synth.solveSAT(phi) match {
+        synth.solver.solveSAT(phi) match {
           case (Some(true), satModel) =>
             val satXsModel = satModel.filterKeys(xss) 
 
             val newPhi = valuateWithModelIn(phi, xss, satModel)
 
-            synth.solveSAT(Not(newPhi)) match {
+            synth.solver.solveSAT(Not(newPhi)) match {
               case (Some(true), invalidModel) =>
                 // Found as such as the xs break, refine predicates
                 predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 213793663c43bb02e881c6f849a2349dd527ceda..c6371a00e686d7d3e10101566be1d268598bbac2 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -88,7 +88,7 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth, 50, 0) {
 
       val tpe = TupleType(p.xs.map(_.getType))
 
-      synth.solveSAT(p.phi) match {
+      synth.solver.solveSAT(p.phi) match {
         case (Some(true), model) =>
           RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe)))
         case (Some(false), model) =>
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index f51749d8203232f8613cdae00423531241d86d3d..2f8dc774ea9fac0c34cf9d365bdf025343350348 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -22,7 +22,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
   )
 
   def run(ctx: LeonContext)(p: Program): Program = {
-    val reporter = new QuietReporter
+    val reporter = new SilentReporter
 
     val mainSolver = new FairZ3Solver(reporter)
     mainSolver.setProgram(p)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 895ec71c44dea208d6b82f1fb818b951c748a29e..936862fd4b5e3ba0b8521e7a8e1f745b61ca52db 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -13,7 +13,7 @@ import java.io.File
 import collection.mutable.PriorityQueue
 
 class Synthesizer(val r: Reporter,
-                  solver: Solver,
+                  val solver: Solver,
                   generateDerivationTrees: Boolean,
                   filterFuns: Option[Set[String]],
                   firstOnly: Boolean,
@@ -70,18 +70,6 @@ class Synthesizer(val r: Reporter,
     bestSolutionSoFar()
   }
 
-  def solveSAT(phi: Expr): (Option[Boolean], Map[Identifier, Expr]) = {
-    solver.solveOrGetCounterexample(Not(phi)) match {
-      case (Some(true), _) =>
-        (Some(false), Map())
-      case (Some(false), model) =>
-        (Some(true), model)
-      case (None, _) =>
-        println("WOOPS: failure on "+phi)
-        (None, Map())
-    }
-  }
-
   val rules = Rules.all(this) ++ Heuristics.all(this)
 
   import purescala.Trees._