Restore FunDef.orig

src/main/scala/leon/purescala/Definitions.scala

@@ -351,6 +351,9 @@ object Definitions {
     val defType : DefType
   ) extends Definition {
     
+    // A copy of the original function before Xlang elimination
+    var orig : Option[FunDef] = None
+    
     private var fullBody_ : Expr = NoTree(returnType)
     def fullBody = fullBody_
     def fullBody_= (e : Expr) {
@@ -385,8 +388,7 @@ object Definitions {
     
     def copyContentFrom(from : FunDef) {
       this.fullBody  = from.fullBody 
-      //this.parent   = from.parent
-      //this.orig    = from.orig
+      this.orig    = from.orig
       this.origOwner = from.origOwner
       this.addAnnotation(from.annotations.toSeq : _*)
     }

src/main/scala/leon/purescala/FunctionClosure.scala

@@ -64,7 +64,7 @@ object FunctionClosure extends TransformationPhase {
       newFunDef.addAnnotation(fd.annotations.toSeq:_*) //TODO: this is still some dangerous side effects
       newFunDef.setOwner(parent)
       fd       .setOwner(parent)
-      newFunDef.origOwner   = Some(fd)
+      newFunDef.orig = Some(fd)
 
       def introduceLets(expr: Expr, fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = {
         val (newExpr, _) = enclosingLets.foldLeft((expr, Map[Identifier, Identifier]()))((acc, p) => {

src/main/scala/leon/xlang/XlangAnalysisPhase.scala

@@ -21,8 +21,8 @@ object XlangAnalysisPhase extends LeonPhase[Program, VerificationReport] {
     val (pgm3, wasLoop) = ImperativeCodeElimination.run(ctx)(pgm2)
     val pgm4 = purescala.FunctionClosure.run(ctx)(pgm3)
 
-    def functionWasLoop(fd: FunDef): Boolean = fd.origOwner match {
-      case Some(nested : FunDef) => // was a nested function
+    def functionWasLoop(fd: FunDef): Boolean = fd.orig match {
+      case Some(nested) => // could have been a LetDef originally
         wasLoop.contains(nested)
       case _ => false //meaning, this was a top level function
     }