Factor out subfunction to find mutually recursive functions

epfl-lara · Jun 11, 2020 · 088ab0c · 088ab0c
1 parent cfe61d7
commit 088ab0c
Showing 1 changed file with 10 additions and 6 deletions.
diff --git a/core/src/main/scala/stainless/termination/MeasureInference.scala b/core/src/main/scala/stainless/termination/MeasureInference.scala
@@ -59,14 +59,18 @@ trait MeasureInference
       }
     }
 
+    def mutuallyRecursiveWithoutMeasure(id: Identifier): Option[Identifier] = {
+      symbols.dependencies(id).find(id2 =>
+        symbols.lookupFunction(id2).exists(fd2 =>
+          symbols.dependencies(id2).contains(id) &&
+          !fd2.measure(symbols).isEmpty
+        )
+      )
+    }
+
     def needsMeasure(fd: FunDef): Boolean = {
       if (symbols.isRecursive(fd.id) && fd.measure(symbols).isEmpty) {
-        symbols.dependencies(fd.id).find(id =>
-          symbols.lookupFunction(id).exists(fd2 =>
-            symbols.dependencies(fd2.id).contains(fd.id) &&
-            !fd2.measure(symbols).isEmpty
-          )
-        ) match {
+        mutuallyRecursiveWithoutMeasure(fd.id) match {
           case None =>
             true
           case Some(id) =>