Restricting recursiveCallsAndSurroundingUnfoldings to look for recursive calls only (#896)

Author: marcoeilers

src/main/scala/viper/silver/ast/utility/Functions.scala

@@ -191,7 +191,9 @@ object Functions {
       case uf@Unfolding (_, body) =>
         recordCallsAndUnfoldings (body, ufs :+ uf) // note: acc is not recursively-processed - we may want to revisit this decision
       case fa@FuncApp (_, args) =>
-        result +:= (fa, ufs)
+        if (fa.funcname == f.name){
+          result +:= (fa, ufs)
+        }
         args.foreach ((n) => recordCallsAndUnfoldings (n, ufs) )
       }
     }

src/test/resources/all/issues/silver/0895.vpr

@@ -0,0 +1,23 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+predicate OhHi() { true }
+
+function mark(): Bool
+{
+  true
+}
+
+function make_your_own_matching_loop(n: Int): Bool
+  requires OhHi()
+{
+    n <= 0 ? true : (unfolding OhHi() in mark()) && make_your_own_matching_loop(n - 1)
+}
+
+method main()
+{
+  fold OhHi()
+  var f: Bool := make_your_own_matching_loop(49)
+  //:: ExpectedOutput(assert.failed:assertion.false)
+  assert f
+}