From 053ec97ade4f70f1b66346582150cceb97c50ce4 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Thu, 6 Nov 2014 13:08:02 +0100
Subject: Extracted a separate class to generate fresh variable names.

---
 Test/VSI-Benchmarks/b3.dfy | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'Test/VSI-Benchmarks')

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();
-- 
cgit v1.2.3