diff --git a/src/sphinx/synthesis.rst b/src/sphinx/synthesis.rst
index b70298a9bb949dbf42142bd07964a7dc605b1c25..17ed8eab14623f8fb09cc2ac04e73b55e4700209 100644
--- a/src/sphinx/synthesis.rst
+++ b/src/sphinx/synthesis.rst
@@ -104,7 +104,7 @@ this rule generates two sub-chooses, and combines them as follows:
    }
 
 
-Inequalite Split
+Inequality Split
 ^^^^^^^^^^^^^^^^
 
 Given two input variables `a` and `b` of numeric type, this rule
@@ -404,3 +404,45 @@ generally faster way of discovering candidate expressions. However, these
 expressions are not guaranteed to be valid since they have only been validated
 by tests. Leon's synthesis framework supports untrusted solutions which trigger
 an end-to-end validation step that relies on verification.
+
+
+String Conversion
+^^^^^^^^^^^^^^^^^
+
+This rule applies to pretty-printing problems given a non-empty list of examples, i.e. of the type:
+
+.. code-block:: scala
+
+  choose ((x: String) =>
+    (input, x) passes {
+       case InputExample1 => "Output Example1"
+       case InputExample2 => "Output Example2"
+    }
+  )
+
+It will create a set of functions and an expression that will be consistent with the example. The example need to ensure the following properties:
+
+* **Primitive display**: All primitive values (int, boolean, Bigint) present in the InputExample must appear in the OutputExample. The exception being Boolean which can also be rendered differently (e.g. as "yes" and "no")
+* **Linearization**: The output example must use the same order as the definition of InputExample; that is, no Set, Map or out of order rendering (e.g. ``case (1, 2) => "2, 1"`` will not work)
+
+To further optimize the search, it is also better to ensure the following property
+
+* **Constant case class display**: By default, if a hierarchy of case classes only contains parameterless variants, such as
+
+.. code-block:: scala
+
+  abstract class StackThread
+  case class T1() extends StackThread
+  case class T2() extends StackThread
+
+it will first try to render expressions with the following function:
+
+.. code-block:: scala
+
+  def StackThreadToString(t: StackThread) = t match {
+    case T1() => "T1"
+    case T2() => "T2"
+  }
+  CONST + StackThreadToString(t) + CONST
+
+where CONST will be inferred from the examples.
diff --git a/src/sphinx/verification.rst b/src/sphinx/verification.rst
index 10b27b6f73b1b96922d28a052414a3f77c12087e..eed3450933411c847f3d6a053b7bf112bd3be25e 100644
--- a/src/sphinx/verification.rst
+++ b/src/sphinx/verification.rst
@@ -215,3 +215,17 @@ As an example, the following code should issue a warning with Scala:
 
 But Leon will prove that the pattern matching is actually exhaustive,
 relying on the given precondition.
+
+Pretty-printing
+---------------
+
+If a global function name ends with "``toString``" with any case, has only one argument and returns a string, this function will be used when printing verification examples. This function can be synthesized (see the synthesis section). For example,
+
+.. code-block:: scala
+
+  def intToString(i: Int) = "#" + i.toString + ",..."
+  def allIntsAreLessThan9(i: Int) = i <= 9 holds
+
+It will display the counter example for ``allIntsAreLessThan9`` as:
+
+  Counter-example: ``#10,...``
diff --git a/testcases/stringrender/BinaryTreeRender.scala b/testcases/stringrender/BinaryTreeRender.scala
index 3805cbbeceb1db936ee253aed98f82f76991e13e..3e939217dee43b7963fc2d784a25b597e05bc3de 100644
--- a/testcases/stringrender/BinaryTreeRender.scala
+++ b/testcases/stringrender/BinaryTreeRender.scala
@@ -1,7 +1,7 @@
 /** 
   * Name:     BinaryTreeRender.scala
   * Creation: 14.10.2015
-  * Author:   Mika�l Mayer (mikael.mayer@epfl.ch)
+  * Author:   Mikael Mayer (mikael.mayer@epfl.ch)
   * Comments: Binary tree rendering specifications.
   */
 
@@ -13,7 +13,7 @@ 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 Node[T](left: Tree[T], i: T, right: Tree[T]) extends Tree[T]
   case class Leaf[T]() extends Tree[T]
   
   /** Synthesis by example specs */
@@ -73,35 +73,35 @@ object TreeRender {
   //////////////////////////////////////////////
   // Non-incremental examples: pure synthesis //
   //////////////////////////////////////////////
-  def synthesizeStandard(s: List[Int]): String = {
+  def synthesizeStandard(s: Tree[Int]): String = {
     ???[String]
   } ensuring psStandard(s)
 
-  def synthesizeRemoveNode(s: List[Int]): String = {
+  def synthesizeRemoveNode(s: Tree[Int]): String = {
     ???[String]
   } ensuring psRemoveNode(s)
   
-  def synthesizeRemoveLeaf(s: List[Int]): String = {
+  def synthesizeRemoveLeaf(s: Tree[Int]): String = {
     ???[String]
   } ensuring psRemoveLeaf(s)
   
-  def synthesizeRemoveComma(s: List[Int]): String = {
+  def synthesizeRemoveComma(s: Tree[Int]): String = {
     ???[String]
   } ensuring psRemoveComma(s)
   
-  def synthesizeRemoveParentheses(s: List[Int]): String = {
+  def synthesizeRemoveParentheses(s: Tree[Int]): String = {
     ???[String]
   } ensuring psRemoveParentheses(s)
   
-  def synthesizePrefix(s: List[Int]): String = {
+  def synthesizePrefix(s: Tree[Int]): String = {
     ???[String]
   } ensuring psPrefix(s)
   
-  def synthesizeLispLike(s: List[Int]): String = {
+  def synthesizeLispLike(s: Tree[Int]): String = {
     ???[String]
   } ensuring psLispLike(s)
   
-  def synthesizeSuffix(s: List[Int]): String = {
+  def synthesizeSuffix(s: Tree[Int]): String = {
     ???[String]
   } ensuring psSuffix(s)
 }
\ No newline at end of file