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); }
   }