diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 1e5e120112330ca85fccfdded79f425c0035214b..81ebbdbec38e1484baf106eac9652d62297ae493 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -151,7 +151,7 @@ object DefOps {
         if (useUniqueIds) {
           List(d.id.uniqueName)
         } else {
-          List(d.id.name)
+          List(d.id.toString)
         }
     }
   }
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 04cf074d3c803d84afae79d70237b0aca1e3d1d9..3416a9851adf79d88771cb838a96f564894bcccf 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -211,7 +211,7 @@ case object StringRender extends Rule("StringRender") {
     
     def getMapping(fd: FunDef): FunDef = {
       transformMap.getOrElse(fd, {
-        val newfunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.params, fd.returnType) // With empty body
+        val newfunDef = new FunDef(fd.id.freshen, fd.tparams, fd.params, fd.returnType) // With empty body
         transformMap += fd -> newfunDef
         newfunDef.body = fd.body.map(mapExpr _)
         newfunDef
@@ -241,7 +241,7 @@ case object StringRender extends Rule("StringRender") {
     }
     val funName3 = funName2.replaceAll("[^a-zA-Z0-9_]","")
     val funName = funName3(0).toLower + funName3.substring(1) 
-    val funId = FreshIdentifier(funName, alwaysShowUniqueID = true)
+    val funId = FreshIdentifier(funName, alwaysShowUniqueID = false)
     val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx.context).toLowerCase()(0).toString, tpe.typeToConvert)
     val fd = new FunDef(funId, Nil, ValDef(argId) :: Nil, StringType) // Empty function.
     fd
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index de3e4198550c98df3839f7115cfd760b90914817..79fc62b455ea15cfb8ae147c920ca02136d14f5c 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -95,4 +95,5 @@ object VCStatus {
   case object Unknown extends VCStatus("unknown")
   case object Timeout extends VCStatus("timeout")
   case object Cancelled extends VCStatus("cancelled")
+  case object Crashed extends VCStatus("crashed")
 }
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 701d0871863522a1ee14b30002adc5ae9f592641..cffc4bae21bcd5267850fb0676d1c0b5eedb32c6 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -11,6 +11,18 @@ import leon.utils.DebugSectionSynthesis
 import leon.utils.DebugSectionVerification
 import leon.purescala.TypeOps
 
+import leon.purescala.Quantification._
+import purescala.Constructors._
+import purescala.ExprOps._
+import purescala.Expressions.Pattern
+import purescala.Extractors._
+import purescala.TypeOps._
+import purescala.Types._
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Definitions._
+import leon.solvers.{ HenkinModel, Model, SolverFactory }
+
 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 = {
@@ -21,13 +33,19 @@ object VerificationReport {
       case Some(fd) =>
         //println("Found fd: " + fd.id.name)
         val ste = new StringTracingEvaluator(ctx, program)
+        try {
         val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
+        
         result.result match {
-          case Some((StringLiteral(res), _)) =>
+          case Some((StringLiteral(res), _)) if res != "" =>
             res
           case _ =>
             orElse
         }
+        } catch {
+          case e: evaluators.ContextualEvaluator#EvalError =>
+            orElse
+        }
       case None =>
         //println("Function to render " + v + " not found")
         orElse
diff --git a/testcases/web/synthesis/22_String_List.scala b/testcases/web/synthesis/22_String_List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..089d57484e3b881a01852e2ae6fae156c27fdd93
--- /dev/null
+++ b/testcases/web/synthesis/22_String_List.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ListsToString {
+
+  def allListsAreEmpty(t: List[Int]): Boolean = (t.isEmpty || t.tail.isEmpty || t.tail.tail.isEmpty || t.tail.head == 0) holds
+  
+  def listToString(p : List[Int]): String =  {
+    ???
+  } ensuring {
+    (res : String) => (p, res) passes {
+      case Cons(1, Cons(2, Nil())) =>
+        "[1, 2]"
+    }
+  }
+}