fix example of abrupt termination

OCamlPro · Jul 4, 2024 · aa20817 · aa20817
1 parent de635e6
commit aa20817
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/c/eacsl/not-yet-supported/abrupt termination/returns.c b/test/c/eacsl/not-yet-supported/abrupt termination/returns.c
@@ -5,7 +5,7 @@ int main(void) {
     owi_assume(x >= 0);
     owi_assume(x <= 20);
     while (x > 0) {
-    /*@ returns \result % 5 == 0 && (\result + 1) % 7 != 0 && (\result + 2) % 11 != 0 && \result == \at(x, Pre) - 2;
+    /*@ returns \result % 5 == 0 && (\result + 1) % 7 != 0 && (\result + 2) % 11 != 0 && \result == \old(x) - 2;
       @ ensures (x + 1) % 5 != 0 && (x + 2) % 7 != 0  && (x + 3) % 11 != 0 && x == \old(x) - 3;
     */
     {