diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index ae3717d3cb1cfbc721a63bdc560e236426f1429b..96eccf1d1a1ac7984305a6db21cdbeb2dfbd42ef 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -72,7 +72,7 @@ class Synthesizer(val reporter: Reporter,
   }
 
   case class TaskTryRules(p: Problem) extends AOOrTask[Solution] {
-    val cost = ProblemCost(p)
+    val cost = Cost.zero
 
     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 918efbca9864c68a95a62e90ded858a760bca735..74659050bc917b8a36f3bbbcc3e933a3217d95e5 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -25,6 +25,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
     def minCost: Cost
 
     var solution: Option[S] = None
+    var isUnsolvable: Boolean = false
 
     def isSolved: Boolean = solution.isDefined
   }
@@ -60,7 +61,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
         case Some(s) =>
           s.cost
         case _ =>
-          val subCosts = subProblems.map { case (t, ot) => subSolutions.get(t).map(_.cost).getOrElse(ot.minCost) }
+          val subCosts = subProblems.values.map(_.minCost)
 
           subCosts.foldLeft(task.cost)(_ + _)
       }
@@ -71,6 +72,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
 
 
     def unsolvable(l: OrTree) {
+      isUnsolvable = true
       parent.unsolvable(this)
     }
 
@@ -123,19 +125,19 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
   class OrNode(val parent: AndNode, var alternatives: Map[AT, AndTree], val task: OT) extends OrTree with Node[AndTree] {
     var triedAlternatives    = Map[AT, AndTree]()
     var minAlternative: Tree = _
-    var minCost              = Cost.zero
+    var minCost              = task.cost
 
     def updateMin() {
       if (!alternatives.isEmpty) {
         minAlternative = alternatives.values.minBy(_.minCost)
         val old = minCost 
-        minCost        = minAlternative.minCost
+        minCost        = minAlternative.minCost + task.cost
         if (minCost != old) {
           Option(parent).foreach(_.updateMin())
         }
       } else {
         minAlternative = null
-        minCost        = Cost.zero
+        minCost        = task.cost
       }
     }
 
@@ -145,6 +147,7 @@ class AndOrGraph[AT <: AOAndTask[S], OT <: AOOrTask[S], S <: AOSolution](val roo
 
 
       if (alternatives.isEmpty) {
+        isUnsolvable = true
         parent.unsolvable(this)
       } else {
         updateMin()
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
index d55039aa113537467203546dbbfb7e31474b6914..b88b7ac945e0bd9bf17576c5965f561d0d4b539d 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
@@ -84,28 +84,28 @@ package leon.synthesis.search
     val ot = t.task
     val (color, style) = t match {
       case l: g.OrLeaf =>
-        (if (t.isSolved) "palegreen" else "white" , "filled,dashed")
+        (if (t.isSolved) "palegreen" else if (t.isUnsolvable) "firebrick" else "white" , "filled,dashed")
       case n: g.OrNode =>
-        (if (t.isSolved) "palegreen" else "white", "filled")
+        (if (t.isSolved) "palegreen" else if (t.isUnsolvable) "firebrick" else "white", "filled")
     }
 
-    drawNode(res, name, ot.cost, ot.toString, color, style)
+    drawNode(res, name, t.minCost, ot.cost, ot.toString, color, style)
   }
 
-  def drawNode(res: StringBuffer, name: String, cost: Cost, content: String, color: String, style: String) {
-    res append "  "+name+" [label=\""+cost.value+" | "+content+"\", shape=box, fillcolor=\""+color+"\", style=\""+style+"\"]\n"
+  def drawNode(res: StringBuffer, name: String, allCost: Cost, selfCost: Cost, content: String, color: String, style: String) {
+    res append "  "+name+" [label=\""+allCost.value+" | "+selfCost.value+" | "+content+"\", shape=box, fillcolor=\""+color+"\", style=\""+style+"\"]\n"
   }
 
   def drawAndNode(res: StringBuffer, name: String, t: g.AndTree) {
     val at = t.task
     val (color, style) = t match {
       case l: g.AndLeaf =>
-        (if (t.isSolved) "palegreen" else "white" , "filled,dashed")
+        (if (t.isSolved) "palegreen" else if (t.isUnsolvable) "firebrick" else "white", "filled,dashed")
       case n: g.AndNode =>
-        (if (t.isSolved) "palegreen" else "white", "filled")
+        (if (t.isSolved) "palegreen" else if (t.isUnsolvable) "firebrick" else "white", "filled")
     }
 
-    drawNode(res, name, at.cost, at.toString, color, style)
+    drawNode(res, name, t.minCost, at.cost, at.toString, color, style)
   }
 
   /** Writes the graph to a file readable with GraphViz. */
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index 2125097c430c4889279ca955144d53062ddbfd58..0dbf5d73d507e33e2df5d60fb1c25abddc6b5652 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -59,6 +59,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
                   al.solution = Some(sol)
                   al.parent.notifySolution(al, sol)
                 case _ =>
+                  al.isUnsolvable = true
                   al.parent.unsolvable(al)
               }
             case ol: g.OrLeaf =>
@@ -69,6 +70,7 @@ abstract class AndOrGraphSearch[AT <: AOAndTask[S],
                   ol.solution = Some(sol)
                   ol.parent.notifySolution(ol, sol)
                 case _ =>
+                  ol.isUnsolvable = true
                   ol.parent.unsolvable(ol)
               }
           }
diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/ADTInduction.scala
index 23db0bb0111d5673f296cf6b4c4f2bac8dbf2e68..bf7d8b16da99ee33830617c4e4bd6a4a71c0a67d 100644
--- a/testcases/synthesis/ADTInduction.scala
+++ b/testcases/synthesis/ADTInduction.scala
@@ -32,6 +32,11 @@ object SortedList {
       (content(out) == (content(in) -- Set(v)))
   }
 
+  def concatSynth(in1: List, in2: List) = choose {
+    (out : List) =>
+      content(out) == content(in1) ++ content(in2)
+  }
+
   def isSorted(l: List): Boolean = l match {
     case Nil() => true
     case Cons(x, Nil()) => true