diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 133b00d4e15ce6fc3664870d68d731179439050e..a8d3022eefdea218e962c5f1bfa7c6dec15f7c3e 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -120,7 +120,7 @@ case object StringRender extends Rule("StringRender") {
     case _ => None
   }
   
-  /** Returns a stream of assignments compatible with input/output examples */
+  /** Returns a stream of assignments compatible with input/output examples for the given template */
   def findAssignments(p: Program, inputs: Seq[Identifier], examples: ExamplesBank, template: Expr)(implicit hctx: SearchContext): Stream[Map[Identifier, String]] = {
     //new Evaluator()
     val e = new StringTracingEvaluator(hctx.context, p)
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index a17df9db3bcc1dc0709473f19122c17b2aa27a6f..de3e4198550c98df3839f7115cfd760b90914817 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -46,26 +46,6 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
   def isInvalid = status.isInstanceOf[VCStatus.Invalid]
   def isInconclusive = !isValid && !isInvalid
 
-  def userDefinedString(v: Expr, orElse: =>String)(vctx: VerificationContext): String = {
-    //println(vctx.program.definedFunctions.map(fd => fd.id.name + "," + (fd.returnType == StringType) + ", " + (fd.params.length == 1) + "," + (fd.params.length == 1 && fd.params.head.getType == v.getType)).mkString("\n"))
-    (vctx.program.definedFunctions find {
-      case fd => fd.returnType == StringType && fd.params.length == 1 && fd.params.head.getType == v.getType && fd.id.name.toLowerCase().endsWith("tostring")
-    }) match {
-      case Some(fd) =>
-        println("Found fd: " + fd.id.name)
-        val ste = new StringTracingEvaluator(vctx.context, vctx.program)
-        val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
-        result.result match {
-          case Some((StringLiteral(res), _)) =>
-            res
-          case _ =>
-            orElse
-        }
-      case None =>
-        orElse
-    }
-  }
-  
   def report(vctx: VerificationContext) {
     import vctx.reporter
     import vctx.context
@@ -83,7 +63,7 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
         // is free to simplify
         val strings = cex.toSeq.sortBy(_._1.name).map {
           case (id, v) =>
-            (id.asString(context), userDefinedString(v, PrettyPrinter(v))(vctx))
+            (id.asString(context), VerificationReport.userDefinedString(v, PrettyPrinter(v))(vctx.context, vctx.program))
         }
 
         if (strings.nonEmpty) {
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 18ae32c8952eea57c46dfeb5698bd2a62430646d..701d0871863522a1ee14b30002adc5ae9f592641 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -4,6 +4,36 @@ package leon
 package verification
 
 import purescala.Definitions.Program
+import leon.evaluators.StringTracingEvaluator
+import purescala.Expressions._
+import purescala.Types.StringType
+import leon.utils.DebugSectionSynthesis
+import leon.utils.DebugSectionVerification
+import leon.purescala.TypeOps
+
+object VerificationReport {
+  /** If it can be computed, returns a user defined string for the given expression */
+  def userDefinedString(v: Expr, orElse: =>String)(ctx: LeonContext, program: Program): String = {
+    //println("Functions available:" + program.definedFunctions.map(fd => fd.id.name + "," + (fd.returnType == StringType) + ", " + (fd.params.length == 1) + "," + (fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType)) + ", " + (if(fd.params.length == 1) fd.params.head.getType + " == " + v.getType else "")).mkString("\n"))
+    (program.definedFunctions find {
+      case fd => fd.returnType == StringType && fd.params.length == 1 && TypeOps.isSubtypeOf(v.getType, fd.params.head.getType) && fd.id.name.toLowerCase().endsWith("tostring")
+    }) match {
+      case Some(fd) =>
+        //println("Found fd: " + fd.id.name)
+        val ste = new StringTracingEvaluator(ctx, program)
+        val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
+        result.result match {
+          case Some((StringLiteral(res), _)) =>
+            res
+          case _ =>
+            orElse
+        }
+      case None =>
+        //println("Function to render " + v + " not found")
+        orElse
+    }
+  }
+}
 
 case class VerificationReport(program: Program, results: Map[VC, Option[VCResult]]) {