diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index e68e21f011f3936797157688901018923c2127bf..066b411dee3d74e405a731e33ece016a049daab5 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -32,12 +32,19 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
   val booleans = (for (b <- Set(true, false)) yield {
     b -> Constructor[Expr, TypeTree](List(), BooleanType, s => BooleanLiteral(b), ""+b)
   }).toMap
+  
+  val strings = (for (b <- Set("", "a", "Abcd")) yield {
+    b -> Constructor[Expr, TypeTree](List(), StringType, s => StringLiteral(b), b)
+  }).toMap
+
 
   def intConstructor(i: Int) = ints(i)
   
   def bigIntConstructor(i: Int) = bigInts(i)
 
   def boolConstructor(b: Boolean) = booleans(b)
+  
+  def stringConstructor(s: String) = strings(s)
 
   def cPattern(c: Constructor[Expr, TypeTree], args: Seq[VPattern[Expr, TypeTree]]) = {
     ConstructorPattern[Expr, TypeTree](c, args)
@@ -166,6 +173,9 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
     case (b: java.lang.Boolean, BooleanType) =>
       (cPattern(boolConstructor(b), List()), true)
 
+    case (b: java.lang.String, StringType) =>
+      (cPattern(stringConstructor(b), List()), true)
+
     case (cc: codegen.runtime.CaseClass, ct: ClassType) =>
       val r = cc.__getRead()
 
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c106d1393bcf793a7fe5d6944ecd533d84a42e36..9acca4069c262a7f744c69afad62bc8bba4fb8ce 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1100,6 +1100,7 @@ object ExprOps {
 
   /** Returns simplest value of a given type */
   def simplestValue(tpe: TypeTree) : Expr = tpe match {
+    case StringType                 => StringLiteral("")
     case Int32Type                  => IntLiteral(0)
     case RealType               	  => FractionalLiteral(0, 1)
     case IntegerType                => InfiniteIntegerLiteral(0)
@@ -1735,6 +1736,10 @@ object ExprOps {
         case UnitType =>
           // Anything matches ()
           ps.nonEmpty
+        
+        case StringType =>
+          // Can't possibly pattern match against all Strings one by one
+          ps exists (_.isInstanceOf[WildcardPattern])
 
         case Int32Type =>
           // Can't possibly pattern match against all Ints one by one