diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index aceebf495ed23694dbbf8d351e132803f2e7c367..148f8d051139c7b772485b2960262d2d5e81f228 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -68,7 +68,7 @@ object Constructors {
   /** Will instantiate the type parameters of the function according to argument types */
   def functionInvocation(fd : FunDef, args : Seq[Expr]) = {
     
-    require(fd.params.length == args.length)
+    require(fd.params.length == args.length, "Invoking function with incorrect number of arguments")
     
     val formalType = tupleTypeWrap(fd.params map { _.getType })
     val actualType = tupleTypeWrap(args map { _.getType })
@@ -234,6 +234,8 @@ object Constructors {
 
   def application(fn: Expr, realArgs: Seq[Expr]) = fn match {
      case Lambda(formalArgs, body) =>
+      assert(realArgs.size == formalArgs.size, "Invoking lambda with incorrect number of arguments")
+
       var defs: Seq[(Identifier, Expr)] = Seq()
 
       val subst = formalArgs.zip(realArgs).map {
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index fc0826dbbc8bc78552e94a672d463c7ae7de6deb..0ee3997c6eec28b9cba5c1ebfdba7ee635776cd5 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -244,11 +244,19 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
           }
         }
 
-        case c @ Choose(cond) =>
-          val cid = FreshIdentifier("choose", c.getType, true)
-          storeExpr(cid)
-          storeGuarded(pathVar, application(cond, Seq(Variable(cid))))
-          Variable(cid)
+        case c @ Choose(Lambda(params, cond)) =>
+
+          val cs = params.map(_.id.freshen.toVariable)
+
+          for (c <- cs) {
+            storeExpr(c.id)
+          }
+
+          val freshMap = (params.map(_.id) zip cs).toMap
+
+          storeGuarded(pathVar, replaceFromIDs(freshMap, cond))
+
+          tupleWrap(cs)
 
         case l @ Lambda(args, body) =>
           val idArgs : Seq[Identifier] = lambdaArgs(l)
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 3d9183a7b3deef7c5ff42e6b5f50f443df68a658..4c27e9b96ca6d7cdbd3795d9cfb8285561e9212c 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -64,26 +64,33 @@ object ConvertHoles extends LeonPhase[Program, Program] {
             None
         }(body)
 
-        val asChoose = if (holes.nonEmpty) {
+        if (holes.nonEmpty) {
           val cids: List[Identifier] = holes.map(_.freshen)
-          val pred = post match {
-            case Some(post) =>
-              replaceFromIDs((holes zip cids.map(_.toVariable)).toMap, post)
-            case None =>
+          val hToFresh = (holes zip cids.map(_.toVariable)).toMap
+
+          val spec = post match {
+            case Some(post: Lambda) =>
+              val asLet = letTuple(post.args.map(_.id), withoutHoles, post.body)
+
+              Lambda(cids.map(ValDef(_)), replaceFromIDs(hToFresh, asLet))
+
+            case _ =>
               Lambda(cids.map(ValDef(_)), BooleanLiteral(true))
           }
 
-          letTuple(holes, Choose(pred), withoutHoles)
+          val choose = Choose(spec)
+
 
+          val valuations = letTuple(holes, choose, withoutHoles)
+
+          withPostcondition(withPrecondition(valuations, pre), post)
+
+        } else {
+          e
         }
-        else withoutHoles
 
-        withPostcondition(withPrecondition(asChoose, pre), post)
-      
       case None => e
     }
-
-
   }
 
    
diff --git a/src/test/resources/regression/synthesis/Misc/HolesBug.scala b/src/test/resources/regression/synthesis/Misc/HolesBug.scala
new file mode 100644
index 0000000000000000000000000000000000000000..47db91b9909f4a2f5f892cafb47394aeffff7ce0
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Misc/HolesBug.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object HolesBug {
+  def plop(a: BigInt, b: BigInt): BigInt = {
+    if (a < b) {
+      ???[BigInt]
+    } else {
+      ???[BigInt]
+    }
+  } ensuring { res =>
+    res > 0
+  }
+}
+
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 35513481a428f1faa1fd3fc394c654fa3eff456d..255781935cfc2864b82938fa999b58aabdab941d 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -64,6 +64,10 @@ class SynthesisRegressionSuite extends LeonTestSuite {
     testSynthesis("List", f, 200)
   }
 
+  forEachFileIn("regression/synthesis/Misc/") { f =>
+    testSynthesis("Miscellaneous", f, 1000)
+  }
+
   forEachFileIn("regression/synthesis/Holes/") { f =>
     testSynthesis("Holes", f, 1000)
   }