diff --git a/.gitignore b/.gitignore
index ef2d597a52fd3c709f822ffae558db110263d543..391915fd711dcf54462e02b2ebfb060312770225 100644
--- a/.gitignore
+++ b/.gitignore
@@ -63,3 +63,5 @@ out-classes
 /scalaz3.lib
 /vcomp100.dll
 /z3.exe
+/libz3java.dll
+/libz3java.lib
diff --git a/library/leon/lang/package.scala b/library/leon/lang/package.scala
index 9c3c72d42efee9268251c2bf9d63091c8460608e..12e18c5235be1a06f8bef03e86b5f40aa95afa96 100644
--- a/library/leon/lang/package.scala
+++ b/library/leon/lang/package.scala
@@ -92,7 +92,7 @@ package object lang {
     }
   }
 
-  @extern
+  @extern @library
   def print(x: String): Unit = {
     scala.Predef.print(x)
   }
diff --git a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
index bba2315256a982a507819c6dba61a5cad7da5a85..cc142d858a181555ff8232cd74680067484ffc77 100644
--- a/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/SelfPrettyPrinter.scala
@@ -64,7 +64,6 @@ trait PrettyPrinterFinder[T, U >: T] {
   def buildLambda(inputType: TypeTree, fd: FunDef, slu: Stream[List[U]]): Stream[T]
   
   def prettyPrinterFromCandidate(fd: FunDef, inputType: TypeTree)(implicit ctx: LeonContext, program: Program): Stream[T] = {
-    println("Considering pretty printer " + fd.id.name + " with arg " + fd.params.head.getType + " for type " + inputType)
     TypeOps.canBeSubtypeOf(inputType, fd.tparams.map(_.tp), fd.params.head.getType) match {
       case Some(genericTypeMap) =>
         println("Found a mapping")
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 57b56f24a28945d979879d2c7d9a99e7fe31dd15..b0bb9d50586264ce71665cf1e56da1fee0756100 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -416,8 +416,8 @@ case object StringRender extends Rule("StringRender") {
           val exprs1s = (new SelfPrettyPrinter)
             .allowFunction(hctx.functionContext)
             .excludeFunction(hctx.functionContext)
-            .prettyPrintersForType(input.getType)(hctx, hctx.program)
-            .map(l => (application(l, Seq(input)), List[Identifier]())) // Use already pre-defined pretty printers.
+            .withPossibleParameters.prettyPrintersForType(input.getType)(hctx, hctx.program)
+            .map{ case (l, identifiers) => (application(l, Seq(input)), identifiers) } // Use already pre-defined pretty printers.
           val exprs1 = exprs1s.toList.sortBy{ case (Lambda(_, FunctionInvocation(tfd, _)), _) if tfd.fd == hctx.functionContext => 0 case _ => 1}
           val exprs2 = ctx.abstractStringConverters.getOrElse(input.getType, Nil).map(f => (f(input), List[Identifier]()))
           val defaultConverters: Stream[WithIds[Expr]] = exprs1.toStream #::: exprs2.toStream
@@ -493,6 +493,13 @@ case object StringRender extends Rule("StringRender") {
               } else {
                 gatherInputs(ctx, q, result += mergeResults(Stream.empty))
               }
+              
+            case t: SetType =>
+              gatherInputs(ctx, q, result += defaultConverters)
+            case t: BagType =>
+              gatherInputs(ctx, q, result += defaultConverters)
+            case t: MapType =>
+              gatherInputs(ctx, q, result += defaultConverters)
             case tpe => 
               hctx.reporter.fatalError("Could not handle class type for string rendering " + tpe)
           }
diff --git a/testcases/stringrender/MapSetBagListMkString.scala b/testcases/stringrender/MapSetBagListMkString.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3d79aad5962fc97e904944248d738550fd47ead6
--- /dev/null
+++ b/testcases/stringrender/MapSetBagListMkString.scala
@@ -0,0 +1,51 @@
+import leon.lang._
+import leon.collection._
+import leon.annotation._
+import leon.lang.synthesis._
+ 
+object StringTest {
+  
+  def listToString(in : List[String]): String =  {
+    ???[String]
+  } ensuring {
+    (res : String) => (in, res) passes {
+      case s if s == List("1", "2", "0") =>
+        "[1 ## 2 ## 0]"
+      case s if s == List[String]() =>
+        "[]"
+    }
+  }
+  
+  def setToString(in : Set[String]): String =  {
+    ???[String]
+  } ensuring {
+    (res : String) => (in, res) passes {
+      case s if s == Set[String]("1", "2", "0") =>
+        "{0 | 1 | 2}"
+      case s if s == Set[String]() =>
+        "{}"
+    }
+  }
+  
+  def mapToString(in : Map[String, String]): String =  {
+    ???[String]
+  } ensuring {
+    (res : String) => (in, res) passes {
+      case s if s == Map[String,String]("Title" -> "Modular Printing", "Abstract" -> "We discuss...", "Year" -> "2016") =>
+        "[Abstract --> We discuss..., Title --> Modular Printing, Year --> 2016]"
+      case s if s == Map[String,String]() =>
+        "[]"
+    }
+  }
+  
+  def bagToString(in : Bag[String]): String =  {
+    ???[String]
+  } ensuring {
+    (res : String) => (in, res) passes {
+      case s if s == Bag[String]("3" -> BigInt(2), "2" -> BigInt(1), "5" -> BigInt(3)) =>
+        "2*3*3*5*5*5"
+      case s if s == Bag[String]() =>
+        ""
+    }
+  }
+}