diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index b62d73254fc0f13b32d463f78498943b5b0eda0e..8571c7648e9760e10297bf7738041cfbb98baeed 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -6,6 +6,6 @@ import leon.purescala.Common._
 
 // Defines a synthesis triple of the form:
 // ⟦ as ⟨ phi ⟩ xs ⟧
-case class Problem(as: Set[Identifier], phi: Expr, xs: Set[Identifier]) {
+case class Problem(as: List[Identifier], phi: Expr, xs: List[Identifier]) {
   override def toString = "⟦ "+as.mkString(";")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
 }
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 30e19b2efed7bd26d2fac900b66cc8666144b98c..f59c8b693e0b1fd17f482d551e3eb3c9f15dedda 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -1,7 +1,7 @@
 package leon
 package synthesis
 
-import leon.purescala.Trees.Expr
+import leon.purescala.Trees._
 
 // Defines a synthesis solution of the form:
 // ⟨ P | T ⟩
@@ -10,6 +10,5 @@ case class Solution(pre: Expr, term: Expr) {
 }
 
 object Solution {
-  def fromProblem(p: Problem): Solution =
-    null
+  def choose(p: Problem): Solution = Solution(BooleanLiteral(true), Choose(p.xs, p.phi))
 }
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 6699bc080167b435a854733214d0dd19ce1385d5..ba4c3c4f1a387d6cd6c64ac3fb442bd0d48242cd 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -26,9 +26,24 @@ class Synthesizer(rules: List[Rule]) {
 
       task.subProblems match {
         case Nil =>
-          task.onSuccess()
+          throw new Exception("Such tasks shouldbe handled immediately")
         case subProblems =>
-          workList ++= subProblems.flatMap(applyRules(_, task))
+          for (sp <- subProblems) {
+            val alternatives = applyRules(sp, task)
+
+            alternatives.find(_.isSuccess) match {
+              case Some(ss) =>
+                ss.onSuccess()
+              case None =>
+                workList ++= alternatives
+            }
+
+            // We are stuck
+            if (alternatives.isEmpty) {
+              // I give up
+              task.onSuccess(sp, Solution.choose(sp))
+            }
+          }
       }
 
     }