From 64f00591a133a65c6031e456da0bba28169be71b Mon Sep 17 00:00:00 2001
From: davidcok <davidcok@github.com>
Date: Tue, 16 May 2023 20:05:03 -0400
Subject: [PATCH] Changing forall ensures to assert-by to avoid deprecation
 warning

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

diff --git a/src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy b/src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy
index 21c4ed24..8a8def62 100644
--- a/src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy
+++ b/src/dafny/NonlinearArithmetic/Internals/ModInternals.dfy
@@ -91,7 +91,7 @@ module {:options "-functionSyntax:4"} Dafny.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"} Dafny.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"} Dafny.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"} Dafny.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); }
   }