diff --git a/src/main/scala/viper/silver/utility/Caching.scala b/src/main/scala/viper/silver/utility/Caching.scala
index 8db077fe2..09a1875c8 100644
--- a/src/main/scala/viper/silver/utility/Caching.scala
+++ b/src/main/scala/viper/silver/utility/Caching.scala
@@ -40,7 +40,8 @@ trait DependencyAware {
             val func = p.findFunction(func_app.funcname)
             if (!marker.contains(func)) {
               markSubAST(func, marker)
-              Seq(func) ++ getDependenciesRec(p, func.pres ++ func.posts ++ extractOptionalNode(func.body), marker)
+              // `func` do not need to be returned because all functions are always considered as a dependency
+              getDependenciesRec(p, func.pres ++ func.posts ++ extractOptionalNode(func.body), marker)
             } else Nil
           case pred_access: PredicateAccess =>
             val pred = p.findPredicate(pred_access.predicateName)
@@ -57,6 +58,7 @@ trait DependencyAware {
     *
     * This method is imprecise, but practical. Here's a list of known imprecisions:
     * - axioms are considered as global dependencies (even if they don't influence the method);
+    * - functions are considered as global dependencies (even if they don't influence the method);
     * - fields are considered as global dependencies (even if they don't influence the method);
     * - concrete predicates used abstractly (w/o unfolding) bring transitive dependencies via their body.
     *
@@ -73,7 +75,7 @@ trait DependencyAware {
   def getDependencies(p: Program, m: Method): List[Hashable] = {
     val marker: mutable.Set[Hashable] = mutable.Set.empty
     markSubAST(m, marker)
-    Seq(m) ++ p.domains ++ p.fields ++
+    Seq(m) ++ p.domains ++ p.functions ++ p.fields ++
       (m.pres ++ m.posts ++ m.body.toSeq).flatMap {
         n => n.deepCollect {
           case method_call: MethodCall =>
@@ -83,8 +85,7 @@ trait DependencyAware {
                 method.pres ++ method.posts ++
                 getDependenciesRec(p, method.formalArgs ++ method.formalReturns ++ method.pres ++ method.posts, marker)
             } else Nil
-          case func_app: FuncApp =>
-            getDependenciesRec(p, Seq(func_app), marker)
+          // function calls do not need to be considered because all functions are always considered as a dependency
           case pred_access: PredicateAccess =>
             getDependenciesRec(p, Seq(pred_access), marker)
         } flatten
diff --git a/src/test/scala/MethodDependencyTests.scala b/src/test/scala/MethodDependencyTests.scala
index 497c7fc66..1088c7107 100644
--- a/src/test/scala/MethodDependencyTests.scala
+++ b/src/test/scala/MethodDependencyTests.scala
@@ -125,13 +125,13 @@ class MethodDependencyTests extends AnyFunSuite with Matchers {
 
 //  println(p)
 
-  val global_deps: List[Hashable] = List(D0, f0,f1,f2,f3,f4)
-  val via_pre_deps: List[Hashable] = List(fun0, p0)
-  val via_post_deps: List[Hashable] = List(fun1, p1)
-  val via_body_deps: List[Hashable] = List(fun2, p2) ++ m0.formalArgs ++ m0.formalReturns ++ m0.pres ++ m0.posts
-  val transitive_deps: List[Hashable] = List(fun4, p4)
+  val global_deps: List[Hashable] = List(D0, f0,f1,f2,f3,f4, fun0,fun1,fun2,fun3,fun4)
+  val via_pre_deps: List[Hashable] = List(p0)
+  val via_post_deps: List[Hashable] = List(p1)
+  val via_body_deps: List[Hashable] = List(p2) ++ m0.formalArgs ++ m0.formalReturns ++ m0.pres ++ m0.posts
+  val transitive_deps: List[Hashable] = List(p4)
   val must_be_deps: List[Hashable] = List(test) ++ global_deps ++ via_pre_deps ++ via_post_deps ++ via_body_deps ++ transitive_deps
-  val must_not_be_deps: List[Hashable] = List(fun3, p3, m0.body.get, m1)
+  val must_not_be_deps: List[Hashable] = List(p3, m0.body.get, m1)
 
   val computed_deps: List[Hashable] = p.getDependencies(p, test)