diff --git a/build.sbt b/build.sbt
index 111613dd1cc2dbcc2c069b031b1866b302b8cd98..618d4f2bab69b8b23f9ddf54210c8736f1ac4918 100644
--- a/build.sbt
+++ b/build.sbt
@@ -111,7 +111,7 @@ sourceGenerators in Compile <+= Def.task {
                       |object Build {
                       |  val baseDirectory = \"\"\"${baseDirectory.value.toString}\"\"\"
                       |  val libFiles = List(
-                      |    ${libFiles.mkString("\"\"\"", "\"\"\",\n    \"\"\"", "\"\"\"")}
+                      |    ${libFiles.mkString("\"\"\"", "\"\"\",\n    \"\"\"", "\"\"\"").replaceAll("\\\\"+"u","\\\\\"\"\"+\"\"\"u")}
                       |  )
                       |}""".stripMargin)
   Seq(build)
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 69c30d39fdede10c93a2fea69093f6b8a6503c99..61089979b2aec6afbc6437d2f2e81158bfe67892 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -552,7 +552,6 @@ sealed abstract class List[T] {
   def toSet: Set[T] = foldLeft(Set[T]()){ 
     case (current, next) => current ++ Set(next)
   }
-
 }
 
 @isabelle.constructor(name = "List.list.Cons")
@@ -577,6 +576,18 @@ object List {
     else Cons[T](x, fill[T](n-1)(x))
   } ensuring(res => (res.content == (if (n <= BigInt(0)) Set.empty[T] else Set(x))) &&
                     res.size == (if (n <= BigInt(0)) BigInt(0) else n))
+  
+  @library
+  def mkString[A](l: List[A], pre: String, mid: String, post: String, f : A => String) = {
+    def rec(l: List[A]): String = l match {
+      case Nil() => ""
+      case Cons(a, b) => mid + f(a) + rec(b)
+    }
+    pre + (l match {
+      case Nil() => ""
+      case Cons(a, b) => f(a) + rec(b)
+    }) + post
+  }
 }
 
 @library
diff --git a/library/lang/Map.scala b/library/lang/Map.scala
index 2a08449cc50d0b7a032a826a5aea563f6f284181..5f6ee3bafd5d77be79d80025a506e649a31220e8 100644
--- a/library/lang/Map.scala
+++ b/library/lang/Map.scala
@@ -12,6 +12,11 @@ object Map {
   def apply[A,B](elems: (A,B)*) = {
     new Map[A,B](scala.collection.immutable.Map[A,B](elems : _*))
   }
+  
+  @extern @library
+  def mkString[A, B](map: Map[A, B], pre: String, inkv: String, betweenkv: String, post: String, fA : A => String, fB: B => String) = {
+    pre + map.theMap.map{ case (k, v) => fA(k) + inkv + fB(v)}.mkString(betweenkv) + post
+  }
 }
 
 @ignore
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 4d70063fb60939a6bf24e7bfc71922a138f53780..28843738b14a1fde11154f5cddd456d8d60e8f9c 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -107,6 +107,20 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
          case _ => throw EvalError(typeErrorMsg(input, StringType))
        }
 
+    case FunctionInvocation(TypedFunDef(fd, Seq(ta, tb)), Seq(mp, pre, inkv, betweenkv, post, fk, fv)) if fd == program.library.mapMkString.get =>
+      val pre_str = e(pre) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(pre, StringType)) }
+      val inkv_str = e(inkv) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(inkv, StringType)) }
+      val post_str = e(post) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(post, StringType)) }
+      val betweenkv_str = e(betweenkv) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(betweenkv, StringType)) }
+      val (mp_map, keyType, valueType) = e(mp) match { case FiniteMap(theMap, keyType, valueType) => (theMap, keyType, valueType) case _ => throw EvalError(typeErrorMsg(mp, MapType(ta, tb))) }
+      
+      val res = pre_str + mp_map.map{ case (k, v) =>
+        (e(application(fk, Seq(k))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) }) +
+        inkv_str +
+        (e(application(fv, Seq(v))) match { case StringLiteral(s) => s case _ => throw EvalError(typeErrorMsg(k, StringType)) })}.mkString(betweenkv_str) + post_str
+      
+      StringLiteral(res)
+
     case FunctionInvocation(tfd, args) =>
       if (gctx.stepsLeft < 0) {
         throw RuntimeError("Exceeded number of allocated methods calls ("+gctx.maxSteps+")")
diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala
index 6bff50527120342bd5610c7e3ba9576a4bf2af95..1fc502212b66d709d8dcd41efc726b264e59dec2 100644
--- a/src/main/scala/leon/utils/Library.scala
+++ b/src/main/scala/leon/utils/Library.scala
@@ -26,6 +26,8 @@ case class Library(pgm: Program) {
   
   lazy val escape = lookup("leon.lang.StrOps.escape").collectFirst { case fd : FunDef => fd }
 
+  lazy val mapMkString = lookup("leon.lang.Map.mkString").collectFirst { case fd : FunDef => fd }
+
   def lookup(name: String): Seq[Definition] = {
     pgm.lookupAll(name)
   }
diff --git a/testcases/stringrender/MapRender.scala b/testcases/stringrender/MapRender.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a5b27ad09a03be750caf6eacd19719fe7f640261
--- /dev/null
+++ b/testcases/stringrender/MapRender.scala
@@ -0,0 +1,25 @@
+import leon.collection._
+import leon.collection.List
+import leon.lang._
+import leon.proof.check
+import leon.lang.synthesis._
+import scala.language.postfixOps
+import leon.annotation._
+
+object MapRender {
+  
+  def f(i: Int): Map[Int, Int] = {
+    Map(1 -> i)
+  } ensuring {
+    (m: Map[Int, Int]) => m(1) == 2
+  }
+  
+  def g(m: Map[Int, Int]): Boolean = {
+    !m.contains(0) || !m.contains(1)
+  } holds
+  
+  def mapIntIntToString(in : Map[Int, Int]): String =  {
+    Map.mkString(in, "MyMap(\n  "," -> ", ",\n  ", ")", (i:Int) => i.toString, (i:Int) => i.toString)
+  }
+}
+