diff --git a/testcases/stringrender/DoubleListRender.scala b/testcases/stringrender/DoubleListRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ed28a264bea40ccd1e0655531f818d01f6a43983
--- /dev/null
+++ b/testcases/stringrender/DoubleListRender.scala
@@ -0,0 +1,35 @@
+/**
+  * Name:     DoubleListRender.scala
+  * Creation: 09.12.2015
+  * Author:   Mikael Mayer (mikael.mayer@epfl.ch)
+  * Comments: Double lists rendering specification (requires many disambiguation rounds)
+  */
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object DoubleListRender {
+  abstract class A
+  case class B(i: AA, a: A) extends A
+  case class N() extends A
+  
+  abstract class AA
+  case class BB(i: A, a: AA) extends AA
+  case class NN() extends AA
+  
+  // Obviously wrong, but it is useful to use the display function.
+  def twoOutOfThreeAsAreTheSame(a: A, b: A, c: A): Boolean = {
+    a == b || a == c || b == c
+  } holds
+
+  def AtoString(a : A): String =  {
+    ???
+  } ensuring {
+    (res : String) => (a, res) passes {
+      case B(BB(N(), BB(B(NN(), B(NN(), N())), NN())), N()) =>
+        "[([], [(), ()])]"
+    }
+  }
+}
\ No newline at end of file
diff --git a/testcases/web/synthesis/23_String_Grammar_Render.scala b/testcases/web/synthesis/23_String_Grammar.scala
similarity index 100%
rename from testcases/web/synthesis/23_String_Grammar_Render.scala
rename to testcases/web/synthesis/23_String_Grammar.scala
diff --git a/testcases/web/synthesis/24_String_DoubleList.scala b/testcases/web/synthesis/24_String_DoubleList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..eb66400e24b24a157e919c53bce0e636b51ddc80
--- /dev/null
+++ b/testcases/web/synthesis/24_String_DoubleList.scala
@@ -0,0 +1,29 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object DoubleListRender {
+  abstract class A
+  case class B(i: AA, a: A) extends A
+  case class N() extends A
+  
+  abstract class AA
+  case class BB(i: A, a: AA) extends AA
+  case class NN() extends AA
+  
+  // Obviously wrong, but it is useful to use the display function.
+  def twoOutOfThreeAsAreTheSame(a: A, b: A, c: A): Boolean = {
+    a == b || a == c || b == c
+  } holds
+
+  def AtoString(a : A): String =  {
+    ???
+  } ensuring {
+    (res : String) => (a, res) passes {
+      case B(BB(N(), BB(B(NN(), B(NN(), N())), NN())), N()) =>
+        "[([], [(), ()])]"
+    }
+  }
+}
\ No newline at end of file