prefix the looping functions with "looping" so that

the TerminationRegression test checks if counterexamples are found

src/test/resources/regression/termination/looping/LambdaCalculus.scala

@@ -22,16 +22,16 @@ object LambdaCalculus {
   }
   
   /* Termination checker (LoopProcessor) says:
-  ✗ Non-terminating for call: eval(App(Abs(0, App(Var(0), Var(0))), Abs(0, App(Var(0), Var(0)))))
+  ✗ Non-terminating for call: looping_eval(App(Abs(0, App(Var(0), Var(0))), Abs(0, App(Var(0), Var(0)))))
   i.e.
   (λx. x x)(λx. x x)
   This is the well-known "omega".
   */
-  // big step call-by-value evaluation
-  def eval(t: Term): Option[Term] = (t match {
-    case App(t1, t2) => eval(t1) match {
-      case Some(Abs(x, body)) => eval(t2) match {
-        case Some(v2) => eval(subst(x, v2, body))
+  // big step call-by-value looping_evaluation
+  def looping_eval(t: Term): Option[Term] = (t match {
+    case App(t1, t2) => looping_eval(t1) match {
+      case Some(Abs(x, body)) => looping_eval(t2) match {
+        case Some(v2) => looping_eval(subst(x, v2, body))
         case None() => None()
       }
       case _ => None() // stuck

src/test/resources/regression/termination/looping/OddEven.scala

 
 object Test {
 
-  def isOdd(n: BigInt): Boolean = {
-    isEven(n-1)
+  def looping_isOdd(n: BigInt): Boolean = {
+    looping_isEven(n-1)
   } ensuring { res => (n % 2 == 1) == res }
   
-  def isEven(n: BigInt): Boolean = {
-    isOdd(n-1)
+  def looping_isEven(n: BigInt): Boolean = {
+    looping_isOdd(n-1)
   } ensuring { res => (n % 2 == 0) == res }
   
   

src/test/resources/regression/termination/looping/UniversalEquality.scala

@@ -5,12 +5,12 @@ import leon._
 object test {
   
   def universalEquality(e1: BigInt, e2: BigInt): Boolean = {
-    val b = proveEquality(e1, e2)
+    val b = looping_proveEquality(e1, e2)
     e1 == e2
   }.holds
   
-  def proveEquality(a: BigInt, b: BigInt): Boolean = {
-    proveEquality(a, b)
+  def looping_proveEquality(a: BigInt, b: BigInt): Boolean = {
+    looping_proveEquality(a, b)
   } ensuring { res => res == (a == b) && res }
 
 }

src/test/resources/regression/termination/looping/WrongFibonacci.scala

 
 object Test {
   
-  def fib(n: BigInt): BigInt = {
-    fib(n-1) + fib(n-2)
+  def looping_fib(n: BigInt): BigInt = {
+    looping_fib(n-1) + looping_fib(n-2)
   } ensuring {res => res == (5*n + 1)*(5*n - 1)}
   
 }