From 088ab0c24b029423ea98babbcfc97bf44a68f25e Mon Sep 17 00:00:00 2001
From: Jad Hamza <jad.hamza@epfl.ch>
Date: Thu, 11 Jun 2020 17:19:33 +0200
Subject: [PATCH] Factor out subfunction to find mutually recursive functions

---
 .../stainless/termination/MeasureInference.scala | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/core/src/main/scala/stainless/termination/MeasureInference.scala b/core/src/main/scala/stainless/termination/MeasureInference.scala
index 6e6bb2f61e..7693a35880 100644
--- 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) =>