Add missing termination measure

viperproject · Feb 6, 2024 · 7624bea · 7624bea
1 parent 1f14160
commit 7624bea
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/utils/verify.gobra b/utils/verify.gobra
@@ -22,6 +22,7 @@ const Uncallable bool = false
 
 ghost
 requires false
+decreases _
 func Unreachable()
 
 ghost
@@ -36,7 +37,7 @@ func TODO()
 
 ghost
 requires b
-decreases
+decreases _
 pure func Asserting(ghost b bool) Unit {
 	return Unit{}
 }