diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index c5a5d448aa7bd1c62e22aaaae99c6d0e10c40226..ae3717d3cb1cfbc721a63bdc560e236426f1429b 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -62,7 +62,7 @@ class Synthesizer(val reporter: Reporter,
   }
 
   case class TaskRunRule(problem: Problem, rule: Rule, app: RuleApplication) extends AOAndTask[Solution] {
-    def cost = RuleApplicationCost(rule, app)
+    val cost = RuleApplicationCost(rule, app)
 
     def composeSolution(sols: List[Solution]): Solution = {
       app.onSuccess(sols)
@@ -72,7 +72,7 @@ class Synthesizer(val reporter: Reporter,
   }
 
   case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
-    def cost = ProblemCost(p)
+    val cost = ProblemCost(p)
 
     override def toString = p.toString
   }
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 6b5dc3aa77d6624068ba2f8b2b4495eec756286b..918efbca9864c68a95a62e90ded858a760bca735 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -35,8 +35,6 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
 
   abstract class OrTree extends Tree {
     override val task: OT
-
-    def isUnsolvable: Boolean = false
   }
 
 
@@ -170,6 +168,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
           minAlternative = sub
 
           notifyParent(solution.get)
+
         case None =>
           solution       = Some(sol)
           minAlternative = sub
@@ -183,8 +182,6 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
         parent.notifySolution(this, sol)
       }
     }
-
-    override def isUnsolvable: Boolean = alternatives.isEmpty
   }
 
   class OrLeaf(val parent: AndNode, val task: OT) extends OrTree with Leaf {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
index 3b8577a83a1b5eff8e814bfea6e26b10e2b911b7..d55039aa113537467203546dbbfb7e31474b6914 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
@@ -86,7 +86,7 @@ package leon.synthesis.search
       case l: g.OrLeaf =>
         (if (t.isSolved) "palegreen" else "white" , "filled,dashed")
       case n: g.OrNode =>
-        (if (t.isSolved) "palegreen" else if (t.isUnsolvable) "indianred1" else "white", "filled")
+        (if (t.isSolved) "palegreen" else "white", "filled")
     }
 
     drawNode(res, name, ot.cost, ot.toString, color, style)
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index a99a5be71c90e03d852b74b9a6ba7e2815f01a0a..2125097c430c4889279ca955144d53062ddbfd58 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -5,19 +5,34 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
                                 S <: AOSolution](val g: AndOrGraph[AT, OT, S]) {
 
   def nextLeaf: Option[g.Leaf] = {
-    var c: g.Tree = g.tree
+    import collection.mutable.PriorityQueue
+
+    case class WT(t: g.Tree, prefixCost: Cost) extends Ordered[WT] {
+      val cost = t.minCost + prefixCost
+
+      def compare(that: WT) = that.cost.compare(this.cost) // DESC
+    }
+
+    val q = new PriorityQueue[WT]()
+    q += WT(g.tree, Cost.zero)
+
     var res: Option[g.Leaf] = None
 
-    while(res.isEmpty) {
-      c match {
-        case l: g.Leaf =>
+    while(res.isEmpty && !q.isEmpty) {
+      q.dequeue() match {
+        case WT(l: g.Leaf, c) =>
           res = Some(l)
 
-        case an: g.AndNode =>
-          c = (an.subProblems -- an.subSolutions.keySet).values.minBy(_.minCost)
+        case WT(an: g.AndNode, c) =>
+          if (!an.isSolved) {
+            q ++= (an.subProblems -- an.subSolutions.keySet).values.map(n => WT(n, c + an.minCost))
+          }
+
+        case WT(on: g.OrNode, c) =>
+          if (!on.isSolved) {
+            q ++= on.alternatives.values.map(n => WT(n, c + on.minCost))
+          }
 
-        case on: g.OrNode =>
-          c = on.minAlternative
       }
     }
 
@@ -32,7 +47,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
   var continue = true
 
   def search(): Option[S] = {
-    while (!g.tree.isSolved && continue && !g.tree.isUnsolvable) {
+    while (!g.tree.isSolved && continue) {
       nextLeaf match {
         case Some(l) =>
           l match {
@@ -61,7 +76,6 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
           continue = false
       }
     }
-    
     g.tree.solution
   }