Update HOTest.scala

I think the decreases annotation is not necessary here.
epfl-lara · May 14, 2024 · 924f987 · 924f987
1 parent d3e7f44
commit 924f987
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/frontends/benchmarks/termination/valid/HOTest.scala b/frontends/benchmarks/termination/valid/HOTest.scala
@@ -11,7 +11,6 @@ import math._
 object HOTest {
   def hoRecur(x: BigInt, f: BigInt => BigInt): BigInt = {
     require(x >= 0 && forall((x: BigInt) => f(x) < x && f(x) >= 0))
-    decreases(abs(x))
     if (x <= 0) BigInt(0)
     else
       hoRecur(f(x), f)