Suppress many warnings in the test suite.

We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.

1 files changed, 4 insertions, 4 deletions

diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy
index b0bb7527..fd64b45e 100644
--- a/Test/dafny4/Primes.dfy
+++ b/Test/dafny4/Primes.dfy
@@ -3,7 +3,7 @@
 

 predicate IsPrime(n: int)

 {

-  2 <= n && forall m :: 2 <= m < n ==> n % m != 0

+  2 <= n && forall m {:nowarn} :: 2 <= m < n ==> n % m != 0 // WISH It would be great to think about the status of modulo as a trigger

 }

 

 // The following theorem shows that there is an infinite number of primes

@@ -167,8 +167,8 @@ lemma Composite(c: int) returns (a: int, b: int)
   calc {

     true;

     !IsPrime(c);

-    !(2 <= c && forall m :: 2 <= m < c ==> c % m != 0);

-    exists m :: 2 <= m < c && c % m == 0;

+    !(2 <= c && forall m {:nowarn} :: 2 <= m < c ==> c % m != 0);

+    exists m {:nowarn} :: 2 <= m < c && c % m == 0;

   }

   a :| 2 <= a < c && c % a == 0;

   b := c / a;

@@ -194,7 +194,7 @@ lemma LargestElementExists(s: set<int>)
   var s' := s;

   while true

     invariant s' != {} && s' <= s;

-    invariant forall x,y :: x in s' && y in s - s' ==> y <= x;

+    invariant forall x,y {:nowarn} :: x in s' && y in s - s' ==> y <= x;

     decreases s';

   {

     var x :| x in s';  // pick something