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.

4 files changed, 25 insertions, 23 deletions

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index 0940d9e7..374555b0 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -3,7 +3,7 @@
 

 method FindZero(a: array<int>) returns (r: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

   ensures 0 <= r ==> r < a.Length && a[r] == 0;

   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;

 {

@@ -20,7 +20,7 @@ method FindZero(a: array<int>) returns (r: int)
 

 lemma Lemma(a: array<int>, k: int, m: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

   requires 0 <= k;

   requires k < a.Length ==> m <= a[k];

   ensures forall i :: k <= i < k+m && i < a.Length ==> a[i] != 0;

@@ -36,7 +36,7 @@ lemma Lemma(a: array<int>, k: int, m: int)
 

 method FindZero_GhostLoop(a: array<int>) returns (r: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

   ensures 0 <= r ==> r < a.Length && a[r] == 0;

   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;

 {

@@ -63,7 +63,7 @@ method FindZero_GhostLoop(a: array<int>) returns (r: int)
 

 method FindZero_Assert(a: array<int>) returns (r: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

-  requires forall i :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];

+  requires forall i {:nowarn} :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];

   ensures 0 <= r ==> r < a.Length && a[r] == 0;

   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;

 {

diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index 319bb8d0..bd654db5 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -83,12 +83,12 @@ lemma LemmaOne(n: int)
 {

 }

 

-lemma LemmaAll_Neg()

-  ensures forall n :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

+lemma LemmaAll_Neg() //FIXME I don't understand the comment below; what trigger?

+  ensures forall n {:nowarn} :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

 {

 }

 

-lemma LemmaOne_Neg(n: int)

+lemma LemmaOne_Neg(n: int) //FIXME What trigger?

   ensures NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

 {

 }

diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect
index 5de0ace6..7da5e2ec 100644
--- a/Test/dafny1/MoreInduction.dfy.expect
+++ b/Test/dafny1/MoreInduction.dfy.expect
@@ -1,5 +1,6 @@
 MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.

 MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.

+MoreInduction.dfy(77,32): Related location

 Execution trace:

     (0,0): anon0

 MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.

@@ -8,6 +9,7 @@ Execution trace:
     (0,0): anon0

 MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.

 MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.

+MoreInduction.dfy(87,43): Related location

 Execution trace:

     (0,0): anon0

 MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 94223cba..3d2a5d78 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -12,7 +12,7 @@ class PriorityQueue {
     reads this, Repr;

   {

     MostlyValid() &&

-    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])

+    (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])

   }

 

   predicate MostlyValid()

@@ -50,8 +50,8 @@ class PriorityQueue {
   method SiftUp(k: int)

     requires 1 <= k && k <= n;

     requires MostlyValid();

-    requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);

-    requires (forall j :: 1 <= j && j <= n ==> j/2 != k);  // k is a leaf

+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);

+    requires (forall j {:nowarn} :: 1 <= j && j <= n ==> j/2 != k);  // k is a leaf

     modifies a;

     ensures Valid();

   {

@@ -59,8 +59,8 @@ class PriorityQueue {
     assert MostlyValid();

     while (1 < i)

       invariant i <= k && MostlyValid();

-      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       if (a[i/2] <= a[i]) {

         return;

@@ -85,8 +85,8 @@ class PriorityQueue {
   method SiftDown(k: int)

     requires 1 <= k;

     requires MostlyValid();

-    requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);

-    requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);

+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);

+    requires (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);

     // Alternatively, the line above can be expressed as:

     //     requires (forall j :: 1 <= k/2 && j/2 == k && j <= n ==> a[j/2/2] <= a[j]);

     modifies a;

@@ -95,8 +95,8 @@ class PriorityQueue {
     var i := k;

     while (2*i <= n)  // while i is not a leaf

       invariant 1 <= i && MostlyValid();

-      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);

     {

       var smallestChild;

       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {

@@ -127,7 +127,7 @@ class PriorityQueue_Alternative {
     reads this, Repr;

   {

     MostlyValid() &&

-    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])

+    (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])

   }

 

   predicate MostlyValid()

@@ -164,7 +164,7 @@ class PriorityQueue_Alternative {
 

   method SiftUp()

     requires MostlyValid();

-    requires (forall j :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);

+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);

     modifies a;

     ensures Valid();

   {

@@ -172,8 +172,8 @@ class PriorityQueue_Alternative {
     assert MostlyValid();

     while (1 < i)

       invariant i <= n && MostlyValid();

-      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       if (a[i/2] <= a[i]) {

         return;

@@ -197,15 +197,15 @@ class PriorityQueue_Alternative {
 

   method SiftDown()

     requires MostlyValid();

-    requires (forall j :: 4 <= j && j <= n ==> a[j/2] <= a[j]);

+    requires (forall j {:nowarn} :: 4 <= j && j <= n ==> a[j/2] <= a[j]);

     modifies a;

     ensures Valid();

   {

     var i := 1;

     while (2*i <= n)  // while i is not a leaf

       invariant 1 <= i && MostlyValid();

-      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       var smallestChild;

       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {