diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 439d0888c1eeed5a7264818255a84e8e8a6fa73e..bfbcf02676071f998fba1856555630f2801392c9 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -262,4 +262,10 @@ object Extractors {
     }
   }
 
+  object UnwrapTuplePattern {
+    def unapply(p : Pattern) : Option[Seq[Pattern]] = Option(p) map {
+      case TuplePattern(_,subs) => subs
+      case other => Seq(other)
+    }
+  }
 }
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b8ebf7c95acf921f0663df88364d01eee839219d..08dee1c712eed27f09037d393c9c043b38b341fb 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -321,7 +321,6 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
           p"($args)"
         }
 
-
       case FunctionInvocation(tfd, args) =>
         p"${tfd.id}"
 
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index d13b70d4449ecba8402e69f70de0be097923c3f8..e56eb59a894bd255701763aafab6e6bb2a286f17 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -5,13 +5,15 @@ package synthesis
 
 import leon.purescala.Trees._
 import leon.purescala.TreeOps._
+import leon.purescala.TypeTrees.TypeTree
 import leon.purescala.Common._
 import leon.purescala.Constructors._
 
 // Defines a synthesis triple of the form:
 // ⟦ as ⟨ C | phi ⟩ xs ⟧
 case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifier]) {
-  override def toString = "⟦ "+as.mkString(";")+", "+(if (pc != BooleanLiteral(true)) pc+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
+  override def toString = 
+    "⟦ "+as.mkString(";")+", " + (if (pc != BooleanLiteral(true)) pc+" ≺ " else "") + " ⟨ "+phi+" ⟩ " + xs.mkString(";") + " ⟧ "
 
   def getTests(sctx: SynthesisContext): Seq[Example] = {
     import purescala.Extractors._
@@ -81,13 +83,67 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
       case Tuple(is) => is.collect { case Variable(i) => i }.toList
       case _ => Nil
     }
+  
+
+    def toIOExamples(in: Expr, out : Expr, cs : MatchCase) : Seq[(Expr,Expr)] = {
+      import utils.ExpressionGrammars
+      import bonsai._
+      import bonsai.enumerators._
+
+      val examplesPerVariable = 5
+     
+      def doSubstitute(subs : Seq[(Identifier, Expr)], e : Expr) = 
+        subs.foldLeft(e) { 
+          case (from, (id, to)) => replaceFromIDs(Map(id -> to), from)
+        }
+
+      // The trivial example
+      if (cs.rhs == out)
+        Seq()
+      else {
+        // The pattern as expression (input expression)(may contain free variables)
+        val (pattExpr, ieMap) = patternToExpression(cs.pattern, in.getType)
+        val freeVars = variablesOf(pattExpr).toSeq
+
+        if (freeVars.isEmpty) {
+          // The input contains no free vars. Trivially return input-output pair
+          Seq((pattExpr, doSubstitute(ieMap,cs.rhs)))
+        } else {
+          // If the input contains free variables, it does not provide concrete examples. 
+          // We will instantiate them according to a simple grammar to get them.
+          val grammar = ExpressionGrammars.BaseGrammar
+          val enum = new MemoizedEnumerator[TypeTree, Expr](grammar.getProductions _)
+          val types = freeVars.map{ _.getType }
+          val typesWithValues = types.map { tp => (tp, enum.iterator(tp).take(examplesPerVariable).toSeq) }.toMap
+          val values = freeVars map { v => typesWithValues(v.getType) }
+          // Make all combinations of all possible instantiations
+          def combinations[A](s : Seq[Seq[A]]) : Seq[Seq[A]] = {
+            if (s.isEmpty) Seq(Seq())
+            else for {
+              h <- s.head
+              t <- combinations(s.tail)
+            } yield (h +: t)
+          }
+          val instantiations = combinations(values) map { freeVars.zip(_).toMap }
+          instantiations map { inst =>
+            (replaceFromIDs(inst, pattExpr), replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs)))  
+          }
+        }
+        
+      }
+    }
+
 
     val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
 
     val testClusters = collect[Map[Identifier, Expr]] {
-      case FunctionInvocation(tfd, List(in, out, FiniteMap(inouts))) if tfd.id.name == "passes" =>
-        val infos = extractIds(Tuple(Seq(in, out)))
-        val exs   = inouts.map{ case (i, o) =>
+
+      //case FunctionInvocation(tfd, List(in, out, FiniteMap(inouts))) if tfd.id.name == "passes" =>
+      case p@Passes(ins, out, cases) =>
+        
+        val ioPairs = cases flatMap { toIOExamples(ins,out,_) }
+        val infos = extractIds(p.scrutinee)
+        val exs   = ioPairs.map{ case (i, o) =>
           val test = Tuple(Seq(i, o))
           val ids = variablesOf(test)
           evaluator.eval(test, ids.map { (i: Identifier) => i -> i.toVariable }.toMap) match {
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index eeeadde942e1884d9b34490cc1d8cb68e6902a9c..89fe46ea027307e4be12f42e1022e5c79011e256 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -53,6 +53,10 @@ class SynthesisRegressionSuite extends LeonTestSuite {
     testSynthesis("Church", f, 200)
   }
 
+  forEachFileIn("regression/synthesis/Examples/") { f =>
+    testSynthesis("IOExamples", f, 200)
+  }
+
   forEachFileIn("regression/synthesis/List/") { f =>
     testSynthesis("List", f, 200)
   }