fixing some bug with the substitution of vars in the postcondition

mytest/Abs.scala

@@ -3,19 +3,22 @@ import leon.Utils._
 object Abs {
 
 
-  def abs(tab: Map[Int, Int], size: Int, j: Int): Map[Int, Int] = {
-    require(j >= 0 && j < size && tab.isDefinedAt(j) && size > 0)
+  def abs(tab: Map[Int, Int], size: Int, j: Int): Map[Int, Int] = ({
+    require(j >= 0 && j < size && size > 0)
     var k = 0
     var tabres = Map.empty[Int, Int]
     (while(k < size) {
-      if(tab(k) < 0)
-        tabres = tabres.updated(k, -tab(k))
-      else
-        tabres = tabres.updated(k, tab(k))
+      if(tab.isDefinedAt(k)) {
+        if(tab(k) < 0)
+          tabres = tabres.updated(k, -tab(k))
+        else
+          tabres = tabres.updated(k, tab(k))
+      } else {
+        tabres = tabres.updated(k, 0)
+      }
       k = k + 1
-    }) invariant(k >= 0)
+    }) invariant(k >= 0 && (if(j < k) tabres(j) >= 0 else true))
     tabres
-
-  }
+  }) ensuring(res => res(j) >= 0)
 
 }

src/main/scala/leon/ImperativeCodeElimination.scala

@@ -91,14 +91,15 @@ object ImperativeCodeElimination extends Pass {
               Map(whileFunVars.head.toVariable -> resVar)
             else
               whileFunVars.zipWithIndex.map{ case (v, i) => (v.toVariable, TupleSelect(resVar, i+1).setType(v.getType)) }.toMap
-          val modifiedVars2ResultVars: Map[Expr, Expr] = modifiedVars.map(v => (v.toVariable, modifiedVars2WhileFunVars(v.toVariable))).toMap
+          val modifiedVars2ResultVars: Map[Expr, Expr] = modifiedVars.map(v => (v.toVariable, whileFunVars2ResultVars(modifiedVars2WhileFunVars(v.toVariable)))).toMap
 
           val trivialPostcondition: Option[Expr] = Some(Not(replace(whileFunVars2ResultVars, whileFunCond)))
           val invariantPrecondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2WhileFunVars, expr))
+          val invariantPostcondition: Option[Expr] = wh.invariant.map(expr => replace(modifiedVars2ResultVars, expr))
           whileFunDef.precondition = invariantPrecondition
           whileFunDef.postcondition = trivialPostcondition.map(expr => 
-              And(expr, invariantPrecondition match { 
-                case Some(e) => replace(modifiedVars2ResultVars, e)
+              And(expr, invariantPostcondition match { 
+                case Some(e) => e
                 case None => BooleanLiteral(true)
               }))