From 3d6b2b77830f7f2bc4f3e61d4d3c8a163123dd31 Mon Sep 17 00:00:00 2001 From: leino Date: Thu, 25 Jun 2015 18:10:42 -0700 Subject: Removed unneeded :heapQuantifier from test case (rendinging this attribute currently unused in the test suite) --- Test/hofs/WhileLoop.dfy | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'Test/hofs/WhileLoop.dfy') 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; + 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; -- cgit v1.2.3