diff --git a/src/main/scala/leon/datagen/SolverDataGen.scala b/src/main/scala/leon/datagen/SolverDataGen.scala
index dfbf50aa68fee0beba9437dc16a2909aeb0c0c9f..78b3753cfff8887d438477c2ad1176b8218254b1 100644
--- a/src/main/scala/leon/datagen/SolverDataGen.scala
+++ b/src/main/scala/leon/datagen/SolverDataGen.scala
@@ -84,8 +84,6 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program)
       val sf = sff(ctx, pgm1)
       val modelEnum = new ModelEnumerator(ctx, pgm1, sf)
 
-      println("Generating for "+ins.map(_.getType.asString)+", satisfying "+satisfying.asString)
-
       val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
 
       try {
diff --git a/src/main/scala/leon/synthesis/ExamplesBank.scala b/src/main/scala/leon/synthesis/ExamplesBank.scala
index 1f34fe87d8f48e9de1ff39e018bdcb0c63eaad59..a0ed2936a5f9c27e525fef16a08b772a05e4d427 100644
--- a/src/main/scala/leon/synthesis/ExamplesBank.scala
+++ b/src/main/scala/leon/synthesis/ExamplesBank.scala
@@ -50,11 +50,25 @@ case class ExamplesBank(valids: Seq[Example], invalids: Seq[Example]) {
 
   def union(that: ExamplesBank) = {
     ExamplesBank(
-      (this.valids union that.valids).distinct,
-      (this.invalids union that.invalids).distinct
+      distinctIns((this.valids union that.valids)),
+      distinctIns((this.invalids union that.invalids))
     )
   }
 
+  private def distinctIns(s: Seq[Example]): Seq[Example] = {
+    val insOuts = (s.collect {
+      case InOutExample(ins, outs) => ins -> outs
+    }).toMap
+
+    s.map(_.ins).distinct.map {
+      case ins =>
+        insOuts.get(ins) match {
+          case Some(outs) => InOutExample(ins, outs)
+          case _ => InExample(ins)
+        }
+    }
+  }
+
   def map(f: Example => List[Example]) = {
     ExamplesBank(valids.flatMap(f), invalids.flatMap(f))
   }
diff --git a/src/main/scala/leon/utils/ModelEnumerator.scala b/src/main/scala/leon/utils/ModelEnumerator.scala
index 81bacf1623c37a83ed484004b9e84b4cbcbbb339..7429c247f78d69e4a70036d88d3b29471127d14f 100644
--- a/src/main/scala/leon/utils/ModelEnumerator.scala
+++ b/src/main/scala/leon/utils/ModelEnumerator.scala
@@ -95,7 +95,7 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
   case object Up   extends SearchDirection
   case object Down extends SearchDirection
 
-  private[this] def enumOptimizing(ids: Seq[Identifier], satisfying: Expr, measure: Expr, dir: SearchDirection): FreeableIterator[Map[Identifier, Expr]] = {
+  private[this] def enumOptimizing(ids: Seq[Identifier], satisfying: Expr, measure: Expr, dir: SearchDirection): Iterator[Map[Identifier, Expr]] = {
     assert(measure.getType == IntegerType)
 
     val s = sf.getNewSolver