diff --git a/testcases/stringrender/BinaryTreeRender.scala b/testcases/stringrender/BinaryTreeRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8bc109dd4351a07bcd7f56a9200989cef19ce01a
--- /dev/null
+++ b/testcases/stringrender/BinaryTreeRender.scala
@@ -0,0 +1,107 @@
+/** 
+  * Name:     BinaryTreeRender.scala
+  * Creation: 14.10.2015
+  * Author:   Mika�l Mayer (mikael.mayer@epfl.ch)
+  * Comments: First benchmark ever for solving string transformation problems. Tree specifications
+  */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object TreeRender {
+  sealed abstract class Tree[T]
+  case class Node[T](left: Node[T], i: T, right: Node[T]) extends Tree[T]
+  case class Leaf[T]() extends Tree[T]
+  
+  /** Synthesis by example specs */
+  @inline def psStandard(s: Tree[Int])(res: String) = (s, res) passes {
+    case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf))"
+    case Node(Leaf, 1, Leaf) => "Node(Leaf, 1, Leaf)"
+    case Leaf => "Leaf"
+  }
+  
+  @inline def psRemoveNode(s: Tree[Int])(res: String) = (s, res) passes {
+    case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "((Leaf, 2, Leaf), 1, (Leaf, -3, Leaf))"
+    case Node(Leaf, 1, Leaf) => "(Leaf, 1, Leaf)"
+    case Leaf => "Leaf"
+  }
+  
+  @inline def psRemoveLeaf(s: Tree[Int])(res: String) = (s, res) passes {
+    case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "((, 2, ), 1, (, -3, ))"
+    case Node(Leaf, 1, Leaf) => "(, 1, )"
+    case Leaf => ""
+  }
+  
+  @inline def psRemoveComma(s: Tree[Int])(res: String) = (s, res) passes {
+    case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "((2), 1, (-3))"
+    case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "(1, (2))"
+    case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "((2), 1)"
+    case Leaf => ""
+  }
+  
+  @inline def psRemoveParentheses(s: Tree[Int])(res: String) = (s, res) passes {
+    case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "(2), 1, (-3)"
+    case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "1, (2)"
+    case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "(2), 1"
+    case Leaf => ""
+  }
+  
+  @inline def psPrefix(s: Tree[Int])(res: String) = (s, res) passes {
+    case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "1 (2) (-3)"
+    case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "1 () (2)"
+    case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "1 (2) ()"
+    case Leaf => "()"
+  }
+  
+  @inline def psLispLike(s: Tree[Int])(res: String) = (s, res) passes {
+    case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "(1 (2) (-3))"
+    case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "(1 () (2))"
+    case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "(1 (2) ())"
+    case Leaf => "()"
+  }
+  
+  @inline def psSuffix(s: Tree[Int])(res: String) = (s, res) passes {
+    case Node(Node(Leaf, 2, Leaf), 1, Node(Leaf, -3, Leaf)) => "(2) (-3) 1"
+    case Node(Leaf, 1, Node(Leaf, 2, Leaf)) => "() (2) 1"
+    case Node(Node(Leaf, 2, Leaf), 1, Leaf) => "(2) () 1"
+    case Leaf => "()"
+  }
+  
+  //////////////////////////////////////////////
+  // Non-incremental examples: pure synthesis //
+  //////////////////////////////////////////////
+  def synthesizeStandard(s: List[Int]): String = {
+    ???[String]
+  } ensuring psStandard(s)
+
+  def synthesizeRemoveNode(s: List[Int]): String = {
+    ???[String]
+  } ensuring psRemoveNode(s)
+  
+  def synthesizeRemoveLeaf(s: List[Int]): String = {
+    ???[String]
+  } ensuring psRemoveLeaf(s)
+  
+  def synthesizeRemoveComma(s: List[Int]): String = {
+    ???[String]
+  } ensuring psRemoveComma(s)
+  
+  def synthesizeRemoveParentheses(s: List[Int]): String = {
+    ???[String]
+  } ensuring psRemoveParentheses(s)
+  
+  def synthesizePrefix(s: List[Int]): String = {
+    ???[String]
+  } ensuring psPrefix(s)
+  
+  def synthesizeLispLike(s: List[Int]): String = {
+    ???[String]
+  } ensuring psLispLike(s)
+  
+  def synthesizeSuffix(s: List[Int]): String = {
+    ???[String]
+  } ensuring psSuffix(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/ListRender.scala b/testcases/stringrender/ListRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..972ae273e8d7ad71728852805163b17cd31cea2b
--- /dev/null
+++ b/testcases/stringrender/ListRender.scala
@@ -0,0 +1,139 @@
+/** 
+  * Name:     ListRender.scala
+  * Creation: 14.10.2015
+  * Author:   Mika�l Mayer (mikael.mayer@epfl.ch)
+  * Comments: First benchmark ever for solving string transformation problems. List specifications.
+  */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ListRender {
+  /** Synthesis by example specs */
+  @inline def psStandard(s: List[Int])(res: String) = (s, res) passes {
+    case Cons(12, Cons(-1, Nil)) => "Cons(12, Cons(-1, Nil))"
+    case Cons(1, Nil) => "Cons(1, Nil)"
+    case Nil => "Nil"
+  }
+  
+  @inline def psRemoveCons(s: List[Int])(res: String) = (s, res) passes {
+    case Cons(12, Cons(-1, Nil)) => "(12, (-1, Nil))"
+    case Cons(1, Nil) => "(1, Nil)"
+    case Nil => "Nil"
+  }
+  
+  @inline def psRemoveNil(s: List[Int])(res: String) = (s, res) passes {
+    case Cons(12, Cons(-1, Nil)) => "(12, (-1, ))"
+    case Cons(1, Nil) => "(1, )"
+    case Nil => ""
+  }
+  
+  @inline def psRemoveLastComma(s: List[Int])(res: String) = (s, res) passes {
+    case Cons(12, Cons(-1, Nil)) => "(12, (-1))"
+    case Cons(1, Nil) => "(1)"
+    case Nil => "()"
+  }
+  
+  @inline def psRemoveParentheses(s: List[Int])(res: String) = (s, res) passes {
+    case Cons(12, Cons(-1, Nil)) => "12, -1"
+    case Cons(1, Nil) => "1"
+    case Nil => ""
+  }
+  
+  @inline def psWrapParentheses(s: List[Int])(res: String) = (s, res) passes {
+    case Cons(12, Cons(-1, Nil)) => "(12, -1)"
+    case Cons(1, Nil) => "(1)"
+    case Nil => "()"
+  }
+  
+  @inline def psList(s: List[Int])(res: String) = (s, res) passes {
+    case Nil => "List()"
+    case Cons(1, Nil) => "List(1)"
+    case Cons(12, Cons(-1, Nil)) => "List(12, -1)"
+  }
+
+  /** Each function's body is the solution of the previous problem.
+    * We want to check that the Leon can repair the programs and also find some ambiguities.*/
+  def render1RemoveCons(s: List[Int]): String = {
+    s match {
+      case Nil => "Nil"
+      case Cons(a, b) => "Cons(" + a + ", " + render1RemoveCons(b) + ")"
+    }
+  } ensuring psRemoveCons(s)
+  
+  def render2RemoveNil(s: List[Int]): String = {
+    s match {
+      case Nil => "Nil"
+      case Cons(a, b) => "(" + a + ", " + render2RemoveNil(b) + ")"
+    }
+  } ensuring psRemoveNil(s)
+  
+  def render3RemoveLastComma(s: List[Int]): String = {
+    s match {
+      case Nil => ""
+      case Cons(a, b) => "(" + a + ", " + render3RemoveLastComma(b) + ")"
+    }
+  } ensuring psRemoveLastComma(s)
+  
+  def render4RemoveParentheses(s: List[Int]): String = {
+    s match {
+      case Nil => ""
+      case Cons(a, Nil) => "(" + a +  ")"
+      case Cons(a, b) => "(" + a + ", " + render4RemoveParentheses(b) + ")"
+    }
+  } ensuring psRemoveParentheses(s)
+  
+  /* harder example: It needs to repair by wrapping the recursive call in a sub-method
+   * in order to add strings to the left and to the right (see render6List) */
+  def render5WrapParentheses(s: List[Int]): String = {
+    s match {
+      case Nil => ""
+      case Cons(a, Nil) => a.toString
+      case Cons(a, b) => a + ", " + render5WrapParentheses(b)
+    }
+  } ensuring psWrapParentheses(s)
+  
+  def render6List(s: List[Int]): String = {
+    def rec(s: List[Int]): String =
+      s match {
+        case Nil => ""
+        case Cons(a, Nil) => a
+        case Cons(a, b) => a + ", " + render6List(b)
+      }
+    "(" + rec(s) + ")"
+  } ensuring psList(s)
+  
+  //////////////////////////////////////////////
+  // Non-incremental examples: pure synthesis //
+  //////////////////////////////////////////////
+  def synthesizeStandard(s: List[Int]): String = {
+    ???[String]
+  } ensuring psStandard(s)
+
+  def synthesizeRemoveCons(s: List[Int]): String = {
+    ???[String]
+  } ensuring psRemoveCons(s)
+  
+  def synthesizeRemoveNil(s: List[Int]): String = {
+    ???[String]
+  } ensuring psRemoveNil(s)
+  
+  def synthesizeRemoveLastComma(s: List[Int]): String = {
+    ???[String]
+  } ensuring psRemoveLastComma(s)
+  
+  def synthesizeRemoveParentheses(s: List[Int]): String = {
+    ???[String]
+  } ensuring psRemoveParentheses(s)
+  
+  def synthesizeWrapParentheses(s: List[Int]): String = {
+    ???[String]
+  } ensuring psWrapParentheses(s)
+  
+  def synthesizeList(s: List[Int]): String = {
+    ???[String]
+  } ensuring psList(s)
+}
\ No newline at end of file