diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/refactor/Repairman.scala
index de119dbc2edc11b9ae17ee2b6ff3a752a405c25f..9edbe56b35208ade42ffaee0ea0e714d0abe18f0 100644
--- a/src/main/scala/leon/refactor/Repairman.scala
+++ b/src/main/scala/leon/refactor/Repairman.scala
@@ -32,7 +32,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
 
   var solutions: List[(Solution, Expr, List[FunDef])] = Nil
 
-  def getChooseInfo(): ChooseInfo = {
+  def getSynthesizer(): Synthesizer = {
     // Gather in/out tests
     val pre = fd.precondition.getOrElse(BooleanLiteral(true))
     val args = fd.params.map(_.id)
@@ -95,21 +95,20 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
       )) diff Seq(ADTInduction)
     );
 
-    ChooseInfo(ctx, program, fd, pre, gexpr, ch, soptions)
+    new Synthesizer(ctx, fd, program, p, soptions)
   }
 
   def repair(): Unit = {
-    val ci = getChooseInfo()
-    val p  = ci.problem
+    val synth = getSynthesizer()
+    val p     = synth.problem
 
-    val synthesizer = ci.synthesizer
 
-    synthesizer.synthesize() match {
+    synth.synthesize() match {
       case (search, sols) =>
         for (sol <- sols) {
           val expr = sol.toSimplifiedExpr(ctx, program)
 
-          val (npr, fds) = synthesizer.solutionToProgram(sol)
+          val (npr, fds) = synth.solutionToProgram(sol)
 
           if (!sol.isTrusted) {
             getVerificationCounterExamples(fds.head, npr) match {
@@ -126,7 +125,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
           }
         }
 
-        if (ci.options.generateDerivationTrees) {
+        if (synth.options.generateDerivationTrees) {
           val dot = new DotGenerator(search.g)
           dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
         }
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index b3959f35c6c7034124a5db1a3f6b8d3b5505a3ce..19f54d17120215df00486a4940ee6245b58eb093 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -12,7 +12,11 @@ import leon.purescala.Constructors._
 // Defines a synthesis triple of the form:
 // ⟦ as ⟨ ws && pc | phi ⟩ xs ⟧
 case class Problem(as: List[Identifier], ws: Expr, pc: Expr, phi: Expr, xs: List[Identifier]) {
-  override def toString = "⟦ "+as.mkString(";")+", "+(if (ws != BooleanLiteral(true)) ws+" - " else "")+(if (pc != BooleanLiteral(true)) pc+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+
+  override def toString = {
+    val pcws = and(ws, pc)
+    "⟦ "+as.mkString(";")+", "+(if (pcws != BooleanLiteral(true)) pcws+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+  }
 
   def getTests(sctx: SynthesisContext): Seq[Example] = {
     import purescala.Extractors._
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 7e5e20ea970985138bee90243fe3326d09d689ef..b36573bc719f4740e4b4127e5d02b2b9e0f2590b 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -26,7 +26,7 @@ object Rules {
     InequalitySplit,
     CEGIS,
     TEGIS,
-    //BottomUpTEGIS,
+    BottomUpTEGIS,
     rules.Assert,
     DetupleOutput,
     DetupleInput,