diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index ca65c78bd6efd112cc73bbe134b582a530b33077..f6e084cdac1cdc9dfc6bf20999aeb0c2aaf529dc 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -9,6 +9,8 @@ package object annotation {
   class library    extends StaticAnnotation
   @ignore
   class verified   extends StaticAnnotation
+  @ignore
+  class repair     extends StaticAnnotation
 
   @ignore
   class induct     extends StaticAnnotation
diff --git a/src/main/scala/leon/refactor/Repairman.scala b/src/main/scala/leon/refactor/Repairman.scala
index c9bd7e9fcc131f4d13bf76b2c0d89c1cbacf3363..bbaec332e25a34dec8f39d53e11986da318019f3 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 repair(): Unit = {
+  def getChooseInfo(): ChooseInfo = {
     // Gather in/out tests
     val pre = fd.precondition.getOrElse(BooleanLiteral(true))
     val args = fd.params.map(_.id)
@@ -78,6 +78,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
     // Synthesis from the ground up
     val p = Problem(fd.params.map(_.id).toList, pc, spec, List(out))
     val ch = Choose(List(out), spec)
+    // do we really want to do that?
     fd.body = Some(ch)
 
     val soptions0 = SynthesisPhase.processOptions(ctx);
@@ -91,7 +92,14 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
       )) diff Seq(ADTInduction)
     );
 
-    val synthesizer = new Synthesizer(ctx, fd, program, p, soptions)
+    ChooseInfo(ctx, program, fd, pc, gexpr, ch, soptions)
+  }
+
+  def repair(): Unit = {
+    val ci = getChooseInfo()
+    val p  = ci.problem
+
+    val synthesizer = ci.synthesizer
 
     synthesizer.synthesize() match {
       case (search, sols) =>
@@ -115,7 +123,7 @@ class Repairman(ctx: LeonContext, program: Program, fd: FunDef) {
           }
         }
 
-        if (soptions.generateDerivationTrees) {
+        if (ci.options.generateDerivationTrees) {
           val dot = new DotGenerator(search.g)
           dot.writeFile("derivation"+DotGenerator.nextId()+".dot")
         }
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index a6a6b29890ff76ff3b869ca743182facbfacdfb8..4da0c9dc73fa3244ad32e8e4ee8529317fd7b4c4 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -9,6 +9,7 @@ import purescala.TypeTrees.{TypeTree,TupleType}
 import purescala.Definitions._
 import purescala.TreeOps._
 import purescala.ScopeSimplifier
+import purescala.Constructors._
 import solvers.z3._
 import solvers._
 
@@ -70,6 +71,10 @@ object Solution {
     new Solution(BooleanLiteral(true), Set(), Choose(p.xs, p.phi))
   }
 
+  def chooseComplete(p: Problem): Solution = {
+    new Solution(BooleanLiteral(true), Set(), Choose(p.xs, and(p.pc, p.phi)))
+  }
+
   // Generate the simplest, wrongest solution, used for complexity lowerbound
   def basic(p: Problem): Solution = {
     new Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(id => simplestValue(id.getType))))