Extracted a separate class to generate fresh variable names.

1 files changed, 1 insertions, 2 deletions

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 91044397..5a2b6e13 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -86,8 +86,8 @@ class Benchmark3 {
    

     while (j < n)

       invariant j <= n;

+      invariant 0 <= k < n && old(q.contents)[k] == m;

       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated

-      invariant 0 <= k < |old(q.contents)| && old(q.contents)[k] == m;

       invariant forall i :: 0 <= i < j ==> m <= old(q.contents)[i]; //m is min so far

     {

       var x := q.Dequeue();

@@ -104,7 +104,6 @@ class Benchmark3 {
       var x := q.Dequeue();

       q.Enqueue(x);

       j := j+1;

-      assert q.contents == old(q.contents)[j..] + old(q.contents)[..j];

     }

 

     m := q.Dequeue();