diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index c1b392774c2f61bd88a7d395691c1c44fdf8deed..fa641566bf7a0205aab3c9c5b72940e35531ed87 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -56,7 +56,7 @@ class OnePoint(synth: Synthesizer) extends Rule("One-point", synth) {
             case _ => Solution.none
           }
 
-          List(new DecomposedTask(synth, task.parent, p, 100, this, List(newProblem), onSuccess))
+          List(task.decompose(this, List(newProblem), onSuccess, 100))
         } else {
           Nil
         }
@@ -78,17 +78,9 @@ class Ground(synth: Synthesizer) extends Rule("Ground", synth) {
 
       synth.solveSAT(p.phi) match {
         case (Some(true), model) =>
-          val onSuccess: List[Solution] => Solution = { 
-            case Nil => Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe), 200)
-          }
-
-          List(new DecomposedTask(synth, task.parent, p, 200, this, Nil, onSuccess))
+          List(task.solveUsing(this, Solution(BooleanLiteral(true), Tuple(p.xs.map(model)).setType(tpe), 200), 200))
         case (Some(false), model) =>
-          val onSuccess: List[Solution] => Solution = { 
-            case Nil => Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200)
-          }
-
-          List(new DecomposedTask(synth, task.parent, p, 200, this, Nil, onSuccess))
+          List(task.solveUsing(this, Solution(BooleanLiteral(false), Error(p.phi+" is UNSAT!").setType(tpe), 200), 200))
         case _ =>
           Nil
       }
@@ -111,7 +103,7 @@ class CaseSplit(synth: Synthesizer) extends Rule("Case-Split", synth) {
           case _ => Solution.none
         }
 
-        List(new DecomposedTask(synth, task.parent, p, 100, this, List(sub1, sub2), onSuccess))
+        List(task.decompose(this, List(sub1, sub2), onSuccess, 100))
       case _ =>
         Nil
     }
@@ -130,12 +122,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
 
         if (!exprsA.isEmpty) {
           if (others.isEmpty) {
-            val onSuccess: List[Solution] => Solution = { 
-              case Nil => Solution(And(exprsA), BooleanLiteral(true), 150)
-              case _ => Solution.none
-            }
-
-            List(new DecomposedTask(synth, task.parent, p, 150, this, Nil, onSuccess))
+            List(task.solveUsing(this, Solution(And(exprsA), BooleanLiteral(true), 150), 150))
           } else {
             val onSuccess: List[Solution] => Solution = { 
               case List(s) => Solution(And(s.pre +: exprsA), s.term, 150)
@@ -144,7 +131,7 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth) {
 
             val sub = p.copy(phi = And(others))
 
-            List(new DecomposedTask(synth, task.parent, p, 150, this, List(sub), onSuccess))
+            List(task.decompose(this, List(sub), onSuccess, 150))
           }
         } else {
           Nil
@@ -168,7 +155,7 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
           case _ => Solution.none
         }
 
-        List(new DecomposedTask(synth, task.parent, p, 300, this, List(sub), onSuccess))
+        List(task.decompose(this, List(sub), onSuccess, 300))
     } else {
       Nil
     }
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index 53e09bc9862937a2e53771ff4d86416e9fb63b0f..73858e295b2a98ab8ac35b11a00cd31dbfbade64 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -8,6 +8,14 @@ class Task(val synth: Synthesizer,
 
   def compare(that: Task) = this.score - that.score
 
+  def decompose(rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Solution, score: Score): DecomposedTask = {
+    new DecomposedTask(this.synth, this.parent, this.problem, score, rule, subProblems, onSuccess)
+  }
+
+  def solveUsing(rule: Rule, onSuccess: => Solution, score: Score): DecomposedTask = {
+    new DecomposedTask(this.synth, this.parent, this.problem, 1000, rule, Nil, { case _ => onSuccess })
+  }
+
   override def toString = " Task("+score+"): " +problem
 }