From b6e07fdb92d601d26f74ac85653fb40316143ac6 Mon Sep 17 00:00:00 2001
From: "Mark R. Tuttle" <mrtuttle@amazon.com>
Date: Wed, 4 Oct 2023 17:56:28 -0400
Subject: [PATCH] Replace deprecated syntax 'forall ensures' -> 'assert ... by'

---
 src/NonlinearArithmetic/Internals/ModInternals.dfy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/NonlinearArithmetic/Internals/ModInternals.dfy b/src/NonlinearArithmetic/Internals/ModInternals.dfy
index 388b06f1..cd4753a9 100644
--- a/src/NonlinearArithmetic/Internals/ModInternals.dfy
+++ b/src/NonlinearArithmetic/Internals/ModInternals.dfy
@@ -91,7 +91,7 @@ module {:options "-functionSyntax:4"} ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
     var zp := (x + n) / n - x / n - 1;
-    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
+    assert 0 == n * zp + ((x + n) % n) - (x % n) by { LemmaMulAuto(); }
     if (zp > 0) { LemmaMulInequality(1, zp, n); }
     if (zp < 0) { LemmaMulInequality(zp, -1, n); }
   }
@@ -103,7 +103,7 @@ module {:options "-functionSyntax:4"} ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
     var zm := (x - n) / n - x / n + 1;
-    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
+    assert 0 == n * zm + ((x - n) % n) - (x % n) by { LemmaMulAuto(); }
     if (zm > 0) { LemmaMulInequality(1, zm, n); }
     if (zm < 0) { LemmaMulInequality(zm, -1, n); }
   }
@@ -115,7 +115,7 @@ module {:options "-functionSyntax:4"} ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x + n, n);
     var zp := (x + n) / n - x / n - 1;
-    forall ensures 0 == n * zp + ((x + n) % n) - (x % n) { LemmaMulAuto(); }
+    assert 0 == n * zp + ((x + n) % n) - (x % n) by { LemmaMulAuto(); }
     if (zp > 0) { LemmaMulInequality(1, zp, n); }
     if (zp < 0) { LemmaMulInequality(zp, -1, n); }
   }
@@ -127,7 +127,7 @@ module {:options "-functionSyntax:4"} ModInternals {
     LemmaFundamentalDivMod(x, n);
     LemmaFundamentalDivMod(x - n, n);
     var zm := (x - n) / n - x / n + 1;
-    forall ensures 0 == n * zm + ((x - n) % n) - (x % n) { LemmaMulAuto(); }
+    assert 0 == n * zm + ((x - n) % n) - (x % n) by { LemmaMulAuto(); }
     if (zm > 0) { LemmaMulInequality(1, zm, n); }
     if (zm < 0) { LemmaMulInequality(zm, -1, n); }
   }