diff --git a/src/main/scala/leon/synthesis/DerivationTree.scala b/src/main/scala/leon/synthesis/DerivationTree.scala
index 0b7d7bf384048e06b4edfcc76d9d2955ed9c9c33..927d69179900cbd17139af6271a185037ca47ddf 100644
--- a/src/main/scala/leon/synthesis/DerivationTree.scala
+++ b/src/main/scala/leon/synthesis/DerivationTree.scala
@@ -10,6 +10,8 @@ class DerivationTree(root: RootTask)  {
     _nextID
   }
 
+  def escapeHTML(str: String) = str.replaceAll("<", "&lt;").replaceAll(">", "&gt;")
+
   def toDot: String = {
     val res = new StringBuffer()
 
@@ -35,7 +37,7 @@ class DerivationTree(root: RootTask)  {
 
       t.solverTask match {
         case Some(decompTask) =>
-          res append " "+node+" [ label = <<TABLE BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"><TR><TD BORDER=\"0\">"+decompTask.rule.name+"</TD></TR><TR><TD BGCOLOR=\"indianred1\">"+t.problem+"</TD></TR><TR><TD BGCOLOR=\"greenyellow\">"+t.solution.getOrElse("?")+"</TD></TR></TABLE>> shape = \"none\" ];\n"
+          res append " "+node+" [ label = <<TABLE BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"><TR><TD BORDER=\"0\">"+decompTask.rule.name+"</TD></TR><TR><TD BGCOLOR=\"indianred1\">"+escapeHTML(t.problem.toString)+"</TD></TR><TR><TD BGCOLOR=\"greenyellow\">"+escapeHTML(t.solution.map(_.toString).getOrElse("?"))+"</TD></TR></TABLE>> shape = \"none\" ];\n"
 
           for (t <- decompTask.subTasks) {
             printTask(t)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 0dbdc5dbfd88144900d2abc427547edbc25f5728..3f7bda5f6cb6461f54f67edf824940c737f9712a 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -2,10 +2,11 @@ package leon
 package synthesis
 
 import leon.purescala.Trees._
+import leon.purescala.TreeOps.simplifyLets
 
 // Defines a synthesis solution of the form:
 // ⟨ P | T ⟩
-case class Solution(pre: Expr, term: Expr) {
+class Solution(val pre: Expr, val term: Expr) {
   override def toString = "⟨ "+pre+" | "+term+" ⟩" 
 
   def toExpr = {
@@ -27,4 +28,12 @@ object Solution {
   }
 
   def none: Solution = throw new Exception("Unexpected failure to construct solution")
+
+  def simplify(e: Expr) = simplifyLets(e)
+
+  def apply(pre: Expr, term: Expr) = {
+    new Solution(simplify(pre), simplify(term))
+  }
+
+  def unapply(s: Solution): Option[(Expr, Expr)] = if (s eq null) None else Some((s.pre, s.term))
 }
diff --git a/testcases/synthesis/DrSuter.scala b/testcases/synthesis/DrSuter.scala
index 0ce54f5b575fe3a1a3b987f903d11aeba01e00c4..12b7dac716b63fd3876b01377e74772c2a684efd 100644
--- a/testcases/synthesis/DrSuter.scala
+++ b/testcases/synthesis/DrSuter.scala
@@ -6,10 +6,8 @@ object DrSuter {
   case class Nil() extends List
   case class Cons(head : Int, tail : List) extends List
 
-  
-
   def myChoose(a : List) : (Int,Int,List) = {
-    choose { (x: Int, y: Int, ys: List) => 
+    choose { (x: Int, y: Int, ys: List) =>
       Cons(x, Cons(y, ys)) == a && x == y ||
       Cons(x, ys) == a          && x < 0
     }
diff --git a/testcases/synthesis/SortedList.scala b/testcases/synthesis/SortedList.scala
index 09f664a12f57c5506d72fcd7615f2093d9938f99..9fde7d0548d1e494d419f3345d9969a5167857ed 100644
--- a/testcases/synthesis/SortedList.scala
+++ b/testcases/synthesis/SortedList.scala
@@ -27,6 +27,8 @@ object SortedList {
   def tailSynth(in: List) = choose{out: List => size(out)+1 == size(in)}
   def consSynth(in: List) = choose{out: List => size(out) == size(in)+1}
 
+  def listOfSizeSynth(i: Int) = choose{out: List => size(out) == i }
+
   def insert1(l: List, v: Int) = (
     Cons(v, l)
   ) ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l))