1 files changed, 5 insertions, 5 deletions

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index f0eb6a60..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;

 {

@@ -18,9 +18,9 @@ method FindZero(a: array<int>) returns (r: int)
   r := -1;

 }

 

-ghost method Lemma(a: array<int>, k: int, m: 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 @@ ghost method 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;

 {