diff --git a/src/main/scala/leon/purescala/FunctionClosure.scala b/src/main/scala/leon/purescala/FunctionClosure.scala
index 63529f34a2b3d9504965bd382991fdf373cf5719..61e6af5c567b25c55ff7695c5a5805ad4b6af279 100644
--- a/src/main/scala/leon/purescala/FunctionClosure.scala
+++ b/src/main/scala/leon/purescala/FunctionClosure.scala
@@ -78,7 +78,7 @@ object FunctionClosure extends TransformationPhase {
       val newPrecondition = simplifyLets(introduceLets(and((capturedConstraints ++ fd.precondition).toSeq :_*), fd2FreshFd))
       newFunDef.precondition = if(newPrecondition == BooleanLiteral(true)) None else Some(newPrecondition)
 
-      val freshPostcondition = fd.postcondition.map{ post => introduceLets(post, fd2FreshFd) }
+      val freshPostcondition = fd.postcondition.map{ post => introduceLets(post, fd2FreshFd).setPos(post) }
       newFunDef.postcondition = freshPostcondition
       
       pathConstraints = fd.precondition.getOrElse(BooleanLiteral(true)) :: pathConstraints
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index 7b340a12ae62d51c2fb1a3ce0e3aa6f3044d5593..a4d8b18c22db9b0bf47d045c52d08a50a76d91be 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -181,9 +181,11 @@ object ImperativeCodeElimination extends LeonPhase[Program, (Program, Set[FunDef
           whileFunDef.precondition = invariantPrecondition
           whileFunDef.postcondition = trivialPostcondition.map(expr => 
               Lambda(Seq(ValDef(resVar.id)), and(expr, invariantPostcondition match { 
-                case Some(e) => e
-                case None => BooleanLiteral(true)
-              })))
+                  case Some(e) => e
+                  case None => BooleanLiteral(true)
+                }).setPos(wh)
+              ).setPos(wh)
+            )
 
           val finalVars = modifiedVars.map(_.freshen)
           val finalScope = (body: Expr) => {
diff --git a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
index f6d53576741a6dd12da4a05344559d5ecc95d471..28ff7349b5d586b2156537d1b31e4e8179b067e6 100644
--- a/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XLangAnalysisPhase.scala
@@ -87,7 +87,7 @@ object XLangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
                        case VCKinds.Precondition => VCXLangKinds.InvariantInd
                        case _ => vc.kind
                      },
-                     vc.tactic)
+                     vc.tactic).setPos(vc.getPos)
 
         nvc -> ovr
       } else {