diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 6b5f47c0a1c714c054ef14632757c2b7ce7761af..b58d15cee91b71a849fb9d3a43e5d953258534ae 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -61,7 +61,7 @@ class SimpleSearch(synth: Synthesizer,
   }
 
   def search(): Option[Solution] = {
-    while (!g.tree.isSolved && continue) {
+    while (!g.tree.isSolved && !isStopped) {
       nextLeaf() match {
         case Some(l)  =>
           l match {
@@ -73,7 +73,7 @@ class SimpleSearch(synth: Synthesizer,
               onExpansion(ol, sub)
           }
         case None =>
-          continue = false
+          stop()
       }
     }
     g.tree.solution
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index b669335b96b9427e65413df5e4bab79d9940f61a..97fc75e77ffbd1f82231908ad537cd8b0c0baf26 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -64,7 +64,12 @@ class Synthesizer(val context : LeonContext,
       new AndOrGraphDotConverter(search.g, firstOnly).writeFile("derivation.dot")
     }
 
-    res.getOrElse(Solution.choose(problem))
+    res match {
+      case Some(solution) =>
+        solution
+      case None =>
+        new AndOrGraphPartialSolution(search.g, (task: TaskRunRule) => Solution.choose(task.problem)).getSolution
+    }
   }
 
 }
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
index 8e8da90a5ba390f6586a78e56b799f715d770077..03bb85e401eaad2b8cf0b2fa8fa7c805c5ad8f32 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
@@ -1,9 +1,9 @@
 package leon.synthesis.search
 
 
- class AndOrGraphDotConverter[AT <: AOAndTask[S],
-                              OT <: AOOrTask[S],
-                              S <: AOSolution](val g: AndOrGraph[AT, OT, S], firstOnly: Boolean) {
+class AndOrGraphDotConverter[AT <: AOAndTask[S],
+                             OT <: AOOrTask[S],
+                             S <: AOSolution](val g: AndOrGraph[AT, OT, S], firstOnly: Boolean) {
 
 
   private[this] var _nextID = 0
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala b/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
new file mode 100644
index 0000000000000000000000000000000000000000..151f40ae5a0ee47f4a02d27062c550083cdbb4e7
--- /dev/null
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
@@ -0,0 +1,37 @@
+package leon.synthesis.search
+
+class AndOrGraphPartialSolution[AT <: AOAndTask[S],
+                                OT <: AOOrTask[S],
+                                S <: AOSolution](val g: AndOrGraph[AT, OT, S], missing: AT => S) {
+
+
+  def getSolution: S = {
+    solveOr(g.tree)
+  }
+
+  def solveAnd(t: g.AndTree): S = {
+    if (t.isSolved) {
+      t.solution.get
+    } else {
+      t match {
+      case l: g.AndLeaf =>
+        missing(t.task)
+      case n: g.AndNode =>
+        n.task.composeSolution(n.subProblems.values.map(solveOr(_)).toList)
+      }
+    }
+  }
+
+  def solveOr(t: g.OrTree): S = {
+    if (t.isSolved) {
+      t.solution.get
+    } else {
+      t match {
+        case l: g.OrLeaf =>
+          missing(l.parent.task)
+        case n: g.OrNode =>
+          solveAnd(n.minAlternative)
+      }
+    }
+  }
+}
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index f0116e1f45faea251713b12a0333a52c8476360e..01aff5047dc0cde1353b8bdded8c9e3f8fd6901b 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -56,10 +56,10 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
   case class ExpandSuccess[T <: AOTask[S]](sol: S) extends ExpandResult[T]
   case class ExpandFailure[T <: AOTask[S]]() extends ExpandResult[T]
 
-  var continue = true
+  var isStopped = false
 
   def stop() {
-    continue = false
+    isStopped = true
   }
 
   def search(): Option[S]