diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index ac635c2f41ca3f2e688b915557ac3829add21125..489568a889f3bf9b56f1a45643286e44ed7e8383 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -47,7 +47,7 @@ object FunctionClosure extends Pass {
       val extraVarDecls = freshVars.map{ case (_, v2) => VarDecl(v2, v2.getType) }
       val newVarDecls = varDecl ++ extraVarDecls
       val newFunId = FreshIdentifier(id.name)
-      val newFunDef = new FunDef(newFunId, rt, newVarDecls)
+      val newFunDef = new FunDef(newFunId, rt, newVarDecls).setPosInfo(fd)
 
       val freshPrecondition = precondition.map(expr => replace(freshVarsExpr, expr))
       val freshConstraints = constraints.map(expr => replace(freshVarsExpr, expr))
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index b44e21cf4d30d0f79e248b0acf9d4935df920f3c..9b03daa9994bc6237c1589a191b2df1ea134786a 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -76,7 +76,7 @@ object ImperativeCodeElimination extends Pass {
           val whileFunVars = modifiedVars.map(id => FreshIdentifier(id.name).setType(id.getType))
           val whileFunVarDecls = whileFunVars.map(id => VarDecl(id, id.getType))
           val whileFunReturnType = if(whileFunVars.size == 1) whileFunVars.head.getType else TupleType(whileFunVars.map(_.getType))
-          val whileFunDef = new FunDef(FreshIdentifier("while"), whileFunReturnType, whileFunVarDecls)
+          val whileFunDef = new FunDef(FreshIdentifier("while"), whileFunReturnType, whileFunVarDecls).setPosInfo(wh)
           
           val modifiedVars2WhileFunVars: Map[Expr, Expr] = modifiedVars.zip(whileFunVars).map(p => (p._1.toVariable, p._2.toVariable)).toMap
           val whileFunCond = replace(modifiedVars2WhileFunVars, cond)
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index 96be8f02148fb64e8c027da0530cd00a5fbecaaa..7200a26ecb6f9d913971fbe29897efb4daa33529 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -19,7 +19,7 @@ object UnitElimination extends Pass {
     //first introduce new signatures without Unit parameters
     allFuns.foreach(fd => {
       if(fd.returnType != UnitType && fd.args.exists(vd => vd.tpe == UnitType)) {
-        val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType))
+        val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
         freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
         freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
         fun2FreshFun += (fd -> freshFunDef)
@@ -85,7 +85,7 @@ object UnitElimination extends Pass {
           removeUnit(b)
         else {
           val (newFd, rest) = if(fd.args.exists(vd => vd.tpe == UnitType)) {
-            val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType))
+            val freshFunDef = new FunDef(FreshIdentifier(fd.id.name), fd.returnType, fd.args.filterNot(vd => vd.tpe == UnitType)).setPosInfo(fd)
             freshFunDef.precondition = fd.precondition //TODO: maybe removing unit from the conditions as well..
             freshFunDef.postcondition = fd.postcondition//TODO: maybe removing unit from the conditions as well..
             fun2FreshFun += (fd -> freshFunDef)
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index ad6fed2a9e111ff7ac9155d26dbf1275aff78b5e..f60580d6de723fc3f4dc30b1aebbb66e4a571ebf 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -486,16 +486,16 @@ trait CodeExtraction extends Extractors {
             throw ImpureCodeEncounteredException(tr)
           }
         }
-        case ExWhile(cond, body) => {
+        case wh@ExWhile(cond, body) => {
           val condTree = rec(cond)
           val bodyTree = rec(body)
-          While(condTree, bodyTree)
+          While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
         }
-        case ExWhileWithInvariant(cond, body, inv) => {
+        case wh@ExWhileWithInvariant(cond, body, inv) => {
           val condTree = rec(cond)
           val bodyTree = rec(body)
           val invTree = rec(inv)
-          val w = While(condTree, bodyTree)
+          val w = While(condTree, bodyTree).setPosInfo(wh.pos.line,wh.pos.column)
           w.invariant = Some(invTree)
           w
         }
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 10410e0e5c646d39377dd2113cff13617bf8f8e6..5276766f5eaa365693f2c3b3266dba591fef4a1f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -26,7 +26,7 @@ object Trees {
   case class Assignment(varId: Identifier, expr: Expr) extends Expr with FixedType {
     val fixedType = UnitType
   }
-  case class While(cond: Expr, body: Expr) extends Expr with FixedType {
+  case class While(cond: Expr, body: Expr) extends Expr with FixedType with ScalacPositional {
     val fixedType = UnitType
     var invariant: Option[Expr] = None