diff --git a/mytest/Assign1.scala b/mytest/Assign1.scala
index 864eb7bfcfefd717bd5db36ba3a517ff096ad27c..ef346a02c6f51f7a1fad605ef4a42cd11fe889a3 100644
--- a/mytest/Assign1.scala
+++ b/mytest/Assign1.scala
@@ -1,10 +1,17 @@
 object Assign1 {
 
   def foo(): Int = {
-    var a = 1
-    var b = a
-    a = a + 1
-    b = b + a
+    var a = 0
+    val tmp = a + 1
+    a = a + 2
+    a = a + 3
+    a = a + 4
+    //var j = 0
+    //var sortedArray = Map.empty[Int, Int]
+    //val tmp = sortedArray(j)
+    //sortedArray = sortedArray.updated(j, sortedArray(j+1))
+    //sortedArray = sortedArray.updated(j+1, tmp)
+    //sortedArray(j)
     a
   }
 
diff --git a/mytest/Bubble.scala b/mytest/Bubble.scala
index 1c6dc98bce5eb1138c90a0408724a098b5c99a19..9a1b8fd44617f38b7d429624ac4579553aa376c5 100644
--- a/mytest/Bubble.scala
+++ b/mytest/Bubble.scala
@@ -2,24 +2,36 @@ import leon.Utils._
 
 object Bubble {
 
-  def sort(a: Map[Int, Int], size: Int): Map[Int, Int] = {
-    require(isArray(a, size))
+  def sort(a: Map[Int, Int], size: Int, k: Int): Map[Int, Int] = ({
+    require(size > 0 && k < size - 1 && k >= 0)
     var i = size - 1
     var j = 0
     var sortedArray = a
     (while(i > 0) {
       j = 0
       (while(j < i) {
-        if(a(j) > a(j+1)) {
+        if(sortedArray(j) > sortedArray(j+1)) {
           val tmp = sortedArray(j)
-          sortedArray = sortedArray.updated(j, a(j+1))
+          sortedArray = sortedArray.updated(j, sortedArray(j+1))
           sortedArray = sortedArray.updated(j+1, tmp)
         }
         j = j + 1
-      }) invariant(isArray(sortedArray, size) && j >= 0 && j <= i && i < size && i >= 0)
+      }) invariant(j >= 0 && j <= i)
       i = i - 1
-    }) invariant(isArray(sortedArray, size) && i >= 0 && i < size)
+    }) invariant(i >= 0 && i < size && (k < i || sortedArray(k) <= sortedArray(k+1)))
     sortedArray
+  }) ensuring(res => res(k) <= res(k+1))
+  //ensuring(res => sorted(res, 0, size-1))
+
+  def sorted(a: Map[Int, Int], l: Int, u: Int): Boolean = {
+    var k = l
+    var sorted = true
+    while(k < u) {
+      if(a(k) > a(k+1))
+        sorted = false
+      k = k + 1
+    }
+    sorted
   }
 
 
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index f59479c740c1d272ebe79f5aad233805b16f12c7..b44e21cf4d30d0f79e248b0acf9d4935df920f3c 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -132,8 +132,8 @@ object ImperativeCodeElimination extends Pass {
           (scope, accFun ++ rFun)
         })
         val (lastRes, lastScope, lastFun) = toFunction(expr)
-        (replace(fun.map{ case (i1, i2) => (i1.toVariable, i2.toVariable) }, lastRes),
-         (body: Expr) => scope(lastScope(body)),
+        (lastRes,
+         (body: Expr) => scope(replace(fun.map{ case (i1, i2) => (i1.toVariable, i2.toVariable) }, lastScope(body))),
          fun ++ lastFun)
       }