diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 250b96211088026a6216276c5d753f888af5d437..720aef3199ca51f6f2e5e59868a19d0fd000a90d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -898,7 +898,7 @@ trait CodeExtraction extends ASTExtractors {
 
         case chs @ ExHole(tpe) =>
           val cTpe  = extractType(tpe)
-          Hole().setType(cTpe)
+          Hole().setType(cTpe).setPos(chs.pos)
 
         case chs @ ExChooseExpression(args, tpe, body, select) =>
           val cTpe  = extractType(tpe)
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 686c5e4b1c905242d1e6aa9c4e66457520c263df..57cc7bf5993b6ec23fdbfe5439cf06d1083e9133 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -51,17 +51,17 @@ object ConvertHoles extends LeonPhase[Program, Program] {
         holes = holes.reverse
 
         if (holes.nonEmpty) {
-          val res = FreshIdentifier("b", true).setType(body.getType)
+          val res = FreshIdentifier("b", true).copiedFrom(body)
           val (pid, pbody) = fd.postcondition.get
 
           val c = Choose(holes, Let(res, body, replaceFromIDs(Map(pid -> res.toVariable), pbody)))
 
           if (holes.size > 1) {
             val newHoles = holes.map(_.freshen)
-            fd.body = Some(LetTuple(newHoles, c, replaceFromIDs((holes zip newHoles.map(_.toVariable)).toMap, body)))
+            fd.body = Some(LetTuple(newHoles, c.setPos(body), replaceFromIDs((holes zip newHoles.map(_.toVariable)).toMap, body)).setPos(body))
           } else {
             fd.body = Some(preMap {
-              case h @ Hole() => Some(c)
+              case h @ Hole() => Some(c.setPos(h))
               case _ => None
             }(fd.body.get))
           }