diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index dcad10769bab3a9101e9ee4fb215cdd225acdcb4..2bec96b30ffd95dc6cf1eb58fd54560dc07f78fd 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -954,7 +954,7 @@ object TreeOps {
 
   def genericTransform[C](pre:  (Expr, C) => (Expr, C),
                           post: (Expr, C) => (Expr, C),
-                          combiner: (Expr, C, Seq[C]) => C)(init: C)(expr: Expr) = {
+                          combiner: (Seq[C]) => C)(init: C)(expr: Expr) = {
 
     def rec(eIn: Expr, cIn: C): (Expr, C) = {
 
@@ -968,20 +968,20 @@ object TreeOps {
           val (e1, c) = rec(e, ctx)
           val newE = builder(e1)
 
-          (newE, combiner(newE, cIn, Seq(c)))
+          (newE, combiner(Seq(c)))
 
         case BinaryOperator(e1, e2, builder) =>
           val (ne1, c1) = rec(e1, ctx)
           val (ne2, c2) = rec(e2, ctx)
           val newE = builder(ne1, ne2)
 
-          (newE, combiner(newE, cIn, Seq(c1, c2)))
+          (newE, combiner(Seq(c1, c2)))
 
         case NAryOperator(es, builder) =>
           val (nes, cs) = es.map{ rec(_, ctx)}.unzip
           val newE = builder(nes)
 
-          (newE, combiner(newE, cIn, cs))
+          (newE, combiner(cs))
 
         case e =>
           sys.error("Expression "+e+" ["+e.getClass+"] is not extractable")
@@ -993,7 +993,7 @@ object TreeOps {
     rec(expr, init)
   }
 
-  private def noCombiner[C](e: Expr, initC: C, subCs: Seq[C]) = initC
+  private def noCombiner(subCs: Seq[Unit]) = ()
 
   def simpleTransform(pre: Expr => Expr, post: Expr => Expr)(expr: Expr) = {
     val newPre  = (e: Expr, c: Unit) => (pre(e), ())
@@ -1303,6 +1303,37 @@ object TreeOps {
     rec(expr, Nil)
   }
 
+  def formulaSize(e: Expr): Int = e match {
+    case t: Terminal =>
+      1
+
+    case UnaryOperator(e, builder) =>
+      formulaSize(e)+1
+
+    case BinaryOperator(e1, e2, builder) =>
+      formulaSize(e1)+formulaSize(e2)+1
+
+    case NAryOperator(es, _) =>
+      es.map(formulaSize).foldRight(0)(_ + _)+1
+  }
+
+  def collectChooses(e: Expr): List[Choose] = {
+    def post(e: Expr, cs: List[Choose]) = {
+      val newCs = e match {
+        case c: Choose => c :: cs
+        case _ => cs
+      }
+
+      (e, newCs)
+    }
+
+    def combiner(cs: Seq[List[Choose]]) = {
+      cs.foldLeft(List[Choose]())(_ ::: _)
+    }
+
+    genericTransform[List[Choose]]((_, _), post, combiner)(List())(e)._2
+  }
+
   def valuateWithModel(model: Map[Identifier, Expr])(id: Identifier): Expr = {
     model.getOrElse(id, simplestValue(id.getType))
   }
diff --git a/src/main/scala/leon/synthesis/Complexity.scala b/src/main/scala/leon/synthesis/Complexity.scala
index eb967a4b2c1c25101e27fe529b7de5717aaeac91..8106beed5d6ba3ae23e1253ba99f82b02e04d647 100644
--- a/src/main/scala/leon/synthesis/Complexity.scala
+++ b/src/main/scala/leon/synthesis/Complexity.scala
@@ -2,6 +2,7 @@ package leon
 package synthesis
 
 import purescala.Trees._
+import purescala.TreeOps._
 
 abstract class Complexity[T <: Complexity[T]] extends Ordered[T] {
   def compare(that: T) = this.value - that.value
@@ -21,9 +22,16 @@ case class TaskComplexity(t: Task) extends Complexity[TaskComplexity] {
 }
 
 case class SolutionComplexity(s: Solution) extends Complexity[SolutionComplexity] {
-  lazy val value = 42
+  lazy val value = {
+    val chooses = collectChooses(s.term)
+    val chooseCost = 1000 * chooses.foldLeft(0)((i, c) => i + (math.pow(2, c.vars.size).toInt + formulaSize(c.pred)))
+
+    formulaSize(s.pre) + formulaSize(s.term) + chooseCost
+  }
 }
 
 case class ProblemComplexity(p: Problem) extends Complexity[ProblemComplexity] {
-  lazy val value = 42
+  lazy val value = {
+    math.pow(2, p.xs.size).toInt + formulaSize(p.phi)
+  }
 }
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 021f03b820dea706422831cf13077b1edea77d0c..7210ef271b7b656694e363f664a978abdfac4a12 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -276,7 +276,7 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 20, 0) {
   }
 }
 
-class GiveUp(synth: Synthesizer) extends Rule("GiveUp", synth, 0, 100) {
+class GiveUp(synth: Synthesizer) extends Rule("GiveUp", synth, -100000, 100) {
   def applyOn(task: Task): RuleResult = {
     RuleSuccess(Solution.choose(task.problem))
   }
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 7754d81f69a5e4e21bc77b97a6b247a4d4f7eca5..7adfb5aef6d21fd473cc1565ce7814578084c336 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -21,12 +21,12 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
   )
 
   def run(ctx: LeonContext)(p: Program): Program = {
-    val quietReporter = new QuietReporter
+    val reporter = new SilentReporter
     val solvers  = List(
-      new TrivialSolver(quietReporter),
-      new FairZ3Solver(quietReporter)
+      new TrivialSolver(reporter),
+      new FairZ3Solver(reporter)
     )
-    val uninterpretedZ3 = new UninterpretedZ3Solver(quietReporter)
+    val uninterpretedZ3 = new UninterpretedZ3Solver(reporter)
     uninterpretedZ3.setProgram(p)
 
     var inPlace                        = false
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index bff15822072fda91043e820f34338af9e0cf73d3..d18bd0cb1c38a3684175f989258445e9e69a0519 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -39,7 +39,6 @@ class Synthesizer(val r: Reporter,
       for (p <- subProblems; r <- rules) yield {
         workList += new Task(this, task, p, r)
       }
-
     }
 
     if (generateDerivationTrees) {