diff --git a/src/main/scala/leon/datagen/SolverDataGen.scala b/src/main/scala/leon/datagen/SolverDataGen.scala
index 3a222bd6b75cffe2909d6276c24019e9a7682963..34d94c1a9013edc2c1d2e3f923e5a754e2934862 100644
--- a/src/main/scala/leon/datagen/SolverDataGen.scala
+++ b/src/main/scala/leon/datagen/SolverDataGen.scala
@@ -11,8 +11,7 @@ import purescala.Constructors._
 import solvers._
 import utils._
 
-
-class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program) => SolverFactory[Solver])) extends DataGenerator {
+class SolverDataGen(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver]) extends DataGenerator {
   implicit val ctx0 = ctx
 
   def generate(tpe: TypeTree): FreeableIterator[Expr] = {
@@ -73,7 +72,6 @@ class SolverDataGen(ctx: LeonContext, pgm: Program, sff: ((LeonContext, Program)
         ModuleDef(FreshIdentifier("new"), fds.values.toSeq, false)
       )))
 
-      val sf = sff(ctx, pgm1)
       val modelEnum = new ModelEnumerator(ctx, pgm1, sf)
 
       val enum = modelEnum.enumVarying(ins, satisfying, sizeOf, 5)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 38644fc4a896cb2f84eefac53eb6652dd041e8a1..0dbf1aba944dfbba2350a43163b6fa852e16ad2e 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -634,6 +634,7 @@ class PrettyPrinter(opts: PrinterOptions,
     case Assert(_, _, bd) => Seq(bd)
     case Let(_, _, bd) => Seq(bd)
     case LetDef(_, bd) => Seq(bd)
+    case LetPattern(_, _, bd) => Seq(bd)
     case Require(_, bd) => Seq(bd)
     case IfExpr(_, t, e) => Seq(t, e) // if-else always has braces anyway
     case Ensuring(bd, pred) => Seq(bd, pred)
@@ -669,6 +670,7 @@ class PrettyPrinter(opts: PrinterOptions,
       _: Ensuring | _: Assert | _: Require | _: Definition | _: MatchExpr | _: MatchCase |
       _: Let | _: LetDef | _: IfExpr | _ : CaseClass | _ : Lambda | _ : Choose | _ : Tuple
     )) => false
+    case (_:Pattern, _) => false
     case (ex: StringConcat, Some(_: StringConcat)) => false
     case (b1 @ BinaryMethodCall(_, _, _), Some(b2 @ BinaryMethodCall(_, _, _))) if precedence(b1) > precedence(b2) => false
     case (BinaryMethodCall(_, _, _), Some(_: FunctionInvocation)) => true
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index c7c9989899a61216efeeab61fe6aaa33ed13578d..628a9201ac5544b3d7f23dcaa1b04da279a3a1d1 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -116,12 +116,13 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
     ExamplesBank(examples.filter(isValidExample), Seq())
   }
 
-  def generateForPC(ids: List[Identifier], pc: Expr, maxValid: Int = 400, maxEnumerated: Int = 1000): ExamplesBank = {
+  def generateForPC(ids: List[Identifier], pc: Expr, ctx: LeonContext, maxValid: Int = 400, maxEnumerated: Int = 1000): ExamplesBank = {
     //println(program.definedClasses)
 
     val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
     val datagen   = new GrammarDataGen(evaluator, ValueGrammar)
-    val solverDataGen = new SolverDataGen(ctx, program, (ctx, pgm) => SolverFactory.getFromSettings(ctx, pgm))
+    val solverF   = SolverFactory.getFromSettings(ctx, program)
+    val solverDataGen = new SolverDataGen(ctx, program, solverF)
 
     val generatedExamples = datagen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample)
 
diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
index cf6063da0ae32c95e6028feaddcdfee43bf10598..0e9a22fd3bd79e7bbb40fd3347650e007e68c828 100644
--- a/src/main/scala/leon/synthesis/SourceInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -63,7 +63,7 @@ object SourceInfo {
 
       val p = Problem.fromSpec(ch.pred, and(path, term), outerEb, Some(fd))
 
-      val pcEb = eFinder.generateForPC(p.as, path, 20)
+      val pcEb = eFinder.generateForPC(p.as, path, ctx, 20)
       val chooseEb = eFinder.extractFromProblem(p)
       val eb = (outerEb union chooseEb) union pcEb
 
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 28d567e1b868a61980809ef84f9aaecdc2d2bd12..771899a7c924fcca1fe67ce2007fc839d7a856ca 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -112,11 +112,10 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
       val sub = Problem(newAs, subWs, subPc, subProblem, p.xs, eb).withWs(hints)
 
       val s = { (e: Expr) =>
-        LetPattern(
-          tuplePatternWrap(patts),
-          tupleWrap(as map Variable),
-          simplePostTransform(revMap)(e)
-        )
+        val body = simplePostTransform(revMap)(e)
+        (patts zip as).foldRight(body) { case ((patt, a), bd) =>
+          LetPattern(patt, a.toVariable, bd)
+        }
       }
      
       Some(decomp(List(sub), forwardMap(s), s"Detuple ${as.mkString(", ")}"))
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 775b496be24f105b83cb8af536cd193b7260c5ba..6a688b1201f1184d104fbfec5a40d0e97c4c0b25 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -45,7 +45,7 @@ case object OptimisticGround extends Rule("Optimistic Ground") {
                     predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
 
                   case (Some(false), _) =>
-                    // Model apprears valid, but it might be a fake expression (generic values)
+                    // Model appears valid, but it might be a fake expression (generic values)
                     val outExpr = tupleWrap(p.xs.map(valuateWithModel(satModel)))
 
                     if (!isRealExpr(outExpr)) {