Removed unneeded :heapQuantifier from test case (rendinging this attribute currently unused in the test suite)

2 files changed, 7 insertions, 7 deletions

diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy
index aa131f98..3a8760ba 100644
--- a/Test/dafny0/SeqFromArray.dfy
+++ b/Test/dafny0/SeqFromArray.dfy
@@ -83,8 +83,8 @@ method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)
     case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>

       assert a[..m] == c[l..l+m];

     case l+a.Length <= c.Length && forall i :: k <= i < a.Length ==> a[i] == c[l+i] =>

-      assert a[k..] == c[l+k..l+a.Length];	   

+      assert a[k..] == c[l+k..l+a.Length];

     case l+k+m <= c.Length && forall i :: k <= i < k+m ==> a[i] == c[l+i] =>

-	  assert a[k..k+m] == c[l+k..l+k+m];

+      assert a[k..k+m] == c[l+k..l+k+m];

   }

 }

diff --git a/Test/hofs/WhileLoop.dfy b/Test/hofs/WhileLoop.dfy
index f79562e9..2c91a8cc 100644
--- a/Test/hofs/WhileLoop.dfy
+++ b/Test/hofs/WhileLoop.dfy
@@ -34,14 +34,14 @@ method OneShot(n: int) {
 
 method HeapQuant(n: int) {
   var f : int -> int := x => x;
-  var i := new Ref<int>;
+  var i := new Ref;
   ghost var r := 0;
   i.val := 0;
-  while (i.val < n)
-    invariant forall u {:heapQuantifier} :: f.requires(u);
-    invariant forall u {:heapQuantifier} :: f.reads(u) == {};
+  while i.val < n
+    invariant forall u :: f.requires(u);
+    invariant forall u :: f.reads(u) == {};
     invariant r == i.val;
-    invariant forall u {:heapQuantifier} :: f(u) == u + r;
+    invariant forall u :: f(u) == u + r;
   {
     i.val, r := i.val + 1, r + 1;
     f := x => f(x) + 1;