fix a bug where local variables in methods were not correctly cleaned…

… up & added test case

src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraphMap.scala

@@ -167,6 +167,8 @@ case class VarAnalysisGraphMap(prog: Program,
 
         map = map + (returnVar -> specifiedInfluences)
       })
+      // Remove actual local variables, so we only see method argument and heap influences
+      map = map.map(entry => entry._1 -> entry._2.filter(v => method.formalArgs.contains(v) || v == heapVertex))
       methodAnalysisMap.put(method, map)
     }
     methodAnalysisStarted -= method

src/test/resources/reasoning/universal_introduction/ui_methods.vpr

@@ -267,23 +267,36 @@ method test9(x: Ref, y: Int)
 }
 
 
-method testRec1(x: Int)
+method testRec1(x: Ref)
     requires acc(x.f)
-    influenced heap by {heap}
+    influenced heap by {heap, x}
 {
-    if (y == 0) {
+    if (x.f == 0) {
         exhale acc(x.f)
     }
 }
 
 
-method testRec2(x: Int)
+method testRec2(x: Ref)
     requires acc(x.f)
-    influenced heap by {heap}
+    influenced heap by {heap, x}
 {
-    testAssumesAbstract1(x)
+    testAssumesAbstract(x)
     testRec1(x)
 }
 
-method testAssumesAbstract(x: Int)
-    assumesUsing {x}
+method testAssumesAbstract(x: Ref)
+    influenced assumes by {x}
+
+function f1(i1: Int, i2: Int): Int
+
+method test_local_var_resolve(i2: Int) returns (ret: Int){
+  var i1: Int
+  ret := f1(i1, i2)
+}
+
+method test_local_var_resolve_caller() {
+    prove forall x: Int assuming x != 0 implies x == 1 {
+        var i: Int := test_local_var_resolve(x)
+    }
+}