diff --git a/testcases/stringrender/ChoiceRender.scala b/testcases/stringrender/ChoiceRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3547d6fdcdc45dc00539f28b8610d80de798af38
--- /dev/null
+++ b/testcases/stringrender/ChoiceRender.scala
@@ -0,0 +1,31 @@
+/**
+  * Name:     TupleWrapperRender.scala
+  * Creation: 15.10.2015
+  * Author:   Mikaël Mayer (mikael.mayer@epfl.ch)
+  * Comments: Tuple rendering specifications.
+  */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ChoiceRender {
+  sealed abstract class Thread
+  case class T1() extends Thread
+  case class T2() extends Thread
+  case class T3() extends Thread
+  
+  sealed abstract class Action
+  case class Call(t: Thread, args: Option[Int]) extends Action
+
+  @inline def psStandard(s: Action) = (res: String) => (s, res) passes {
+    case Call(T1(),None()) => "T1 call"
+    case Call(T1(),Some(2)) => "T1 -> 2"
+  }
+  
+  def synthesizeStandard(s: Action): String = {
+     ???[String]
+  } ensuring psStandard(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/ConstantRender.scala b/testcases/stringrender/ConstantRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f208fdb2b09a09846307340fc79c778f8fa8392b
--- /dev/null
+++ b/testcases/stringrender/ConstantRender.scala
@@ -0,0 +1,43 @@
+/**
+  * Name:     TupleWrapperRender.scala
+  * Creation: 15.10.2015
+  * Author:   Mikaël Mayer (mikael.mayer@epfl.ch)
+  * Comments: Tuple rendering specifications.
+  */
+
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ConstantRender {
+  sealed abstract class Thread
+  case class T1() extends Thread
+  case class T2() extends Thread
+  case class T3() extends Thread
+
+  @inline def psStandard(s: Thread) = (res: String) => (s, res) passes {
+    case T1() => "T1"
+  }
+  
+  @inline def psSuffix(s: Thread) = (res: String) => (s, res) passes {
+    case T1() => "T1()"
+  }
+  
+  @inline def psPrefix(s: Thread) = (res: String) => (s, res) passes {
+    case T1() => "Call: T1()"
+  }
+  
+  def synthesizeStandard(s: Thread): String = {
+     ???[String]
+  } ensuring psStandard(s)
+  
+  def synthesizeSuffix(s: Thread): String = {
+     ???[String]
+  } ensuring psSuffix(s)
+  
+  def synthesizePrefix(s: Thread): String = {
+     ???[String]
+  } ensuring psPrefix(s)
+}
\ No newline at end of file
diff --git a/testcases/stringrender/Example-Stack.scala b/testcases/stringrender/Example-Stack.scala
index 1f5024671e8e7c73c899f688d6da81e85ae5f12a..bb9f64d1f83bf2f91a03a0c6fbf581f03083971b 100644
--- a/testcases/stringrender/Example-Stack.scala
+++ b/testcases/stringrender/Example-Stack.scala
@@ -326,6 +326,39 @@ object AtomicStack {
   
   }  holds
   
+  def threadToStringSimplest(p: StackTid): String = {
+    ???[String]
+  } ensuring {
+    res => (p, res) passes {
+      case T1()
+      =>
+     "T1: call Push(5)"
+    }
+  }
+  
+  def threadToStringSimple0(p: Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]): String = {
+    ???[String]
+  } ensuring {
+    res => (p, res) passes {
+      case CallEvent(T1(), Push(), Some(BigInt(5)))
+      =>
+     "T1: call Push(5)"
+    }
+  }
+  
+  def threadToStringSimple1(p: List[Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]]): String = {
+    ???[String]
+  } ensuring {
+    res => (p, res) passes {
+      case Cons(CallEvent(T1(), Push(), Some(BigInt(5))),
+           Cons(InternalEvent(T1()), Nil()))
+      =>
+     "T1: call Push(5)\nT1: internal"
+    }
+  }
+  
+  
+  /** This is THE method we want to render */
   def threadToString(p: List[Event[StackTid,StackMethodName,Option[BigInt],Option[BigInt]]]): String = {
     ???[String]
   } ensuring {