diff --git a/src/main/scala/analysis/SSAForm.scala b/src/main/scala/analysis/SSAForm.scala
index c1d444460..f21892e1e 100644
--- a/src/main/scala/analysis/SSAForm.scala
+++ b/src/main/scala/analysis/SSAForm.scala
@@ -109,7 +109,8 @@ object SSAForm {
 
   def applySSA(program: Program): Unit = {
     val varMaxTracker = new mutable.HashMap[String, Int]()
-    val blockBasedMappings = new mutable.HashMap[(Block, String), Set[Int]]().withDefault(_ => Set())
+    val blockBasedMappings = new mutable.HashMap[(Block, String), mutable.Set[Int]]().withDefault(_ => mutable.Set())
+    val context = new mutable.HashMap[(Procedure, String), mutable.Set[Int]]().withDefault(_ => mutable.Set())
     for (proc <- program.procedures) {
       for (block <- proc.blocks) {
         for (stmt <- block.statements) {
@@ -117,39 +118,47 @@ object SSAForm {
           stmt match {
             case localAssign: LocalAssign => {
                 localAssign.rhs.variables.foreach(v => {
-                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), Set())
+                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), context.getOrElseUpdate((proc, v.name), mutable.Set()))
                 })
-                val maxVal = varMaxTracker.getOrElse(localAssign.lhs.name, 0)
-                blockBasedMappings((block, localAssign.lhs.name)) = Set(maxVal)
+                val maxVal = varMaxTracker.getOrElseUpdate(localAssign.lhs.name, 0)
+                blockBasedMappings((block, localAssign.lhs.name)) = mutable.Set(maxVal)
 
                 localAssign.lhs.ssa_id = blockBasedMappings((block, localAssign.lhs.name))
                 varMaxTracker(localAssign.lhs.name) = blockBasedMappings((block, localAssign.lhs.name)).max + 1
+                println("test")
             }
             case memoryAssign: MemoryAssign => {
                 memoryAssign.lhs.variables.foreach(v => {
-                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), Set())
+                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), context.getOrElseUpdate((proc, v.name), mutable.Set()))
                 })
                 memoryAssign.rhs.variables.foreach(v => {
-                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), Set())
+                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), context.getOrElseUpdate((proc, v.name), mutable.Set()))
                 })
             }
             case assume: Assume => {
                 assume.body.variables.foreach(v => {
-                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), Set())
+                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), context.getOrElseUpdate((proc, v.name), mutable.Set()))
                 })
             } // no required for analyses
             case assume: Assert => {
                 assume.body.variables.foreach(v => {
-                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), Set())
+                  v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), context.getOrElseUpdate((proc, v.name), mutable.Set()))
                 })
             } // no required for analyses
             case _ => throw new RuntimeException("No SSA form for " + stmt.getClass + " yet")
           }
         }
         block.jump match {
+          case directCall: DirectCall => {
+            varMaxTracker.keys.foreach(varr => {
+              //context((directCall.target, varr)) = context((directCall.target, varr)) ++ blockBasedMappings(block, varr)
+              context.getOrElseUpdate((directCall.target, varr), mutable.Set()) ++= blockBasedMappings((block, varr))
+            })
+            println(context)
+          }
           case indirectCall: IndirectCall => {
               indirectCall.target.variables.foreach(v => {
-                v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), Set())
+                v.ssa_id = blockBasedMappings.getOrElseUpdate((block, v.name), context.getOrElseUpdate((proc, v.name), mutable.Set()))
               })
           }
           case goTo: GoTo => {
diff --git a/src/main/scala/analysis/SteensgaardAnalysis.scala b/src/main/scala/analysis/SteensgaardAnalysis.scala
index e412106ac..a15b87b18 100644
--- a/src/main/scala/analysis/SteensgaardAnalysis.scala
+++ b/src/main/scala/analysis/SteensgaardAnalysis.scala
@@ -227,7 +227,6 @@ class SteensgaardAnalysis(
             // *X1 = X2: [[X1]] = ↑a ^ [[X2]] = a where a is a fresh term variable
             val X1_star = eval(memoryAssign.rhs.index, cmd)
             val X2 = evaluateExpression(memoryAssign.rhs.value, constantProp(n)).getOrElse(memoryAssign.rhs.value)
-            println(X2)
             val alpha = FreshVariable()
             unify(exprToStTerm(X1_star), PointerRef(alpha))
             unify(alpha, exprToStTerm(X2))
@@ -235,7 +234,6 @@ class SteensgaardAnalysis(
         }
       case _ => // do nothing
     }
-    //dump_file(stringArr, "any")
   }
 
   private def unify(t1: Term[StTerm], t2: Term[StTerm]): Unit = {
diff --git a/src/main/scala/ir/Expr.scala b/src/main/scala/ir/Expr.scala
index c4dbc2c0b..0a4b0e00c 100644
--- a/src/main/scala/ir/Expr.scala
+++ b/src/main/scala/ir/Expr.scala
@@ -2,8 +2,10 @@ package ir
 
 import boogie._
 
+import scala.collection.mutable
+
 trait Expr {
-  var ssa_id: Set[Int] = Set()
+  var ssa_id: mutable.Set[Int] = mutable.Set[Int]()
   def toBoogie: BExpr
   def toGamma: BExpr = {
     val gammaVars: Set[BExpr] = gammas.map(_.toGamma)