4 files changed, 16 insertions, 10 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index f59b0c3e..d47c4d4d 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -96,7 +96,7 @@ class Benchmark3 {
       if x < m { k := j; m := x; }
       j := j+1;
     }
-    
+
     j := 0;
     while j < k
       invariant j <= k;
@@ -108,10 +108,16 @@ class Benchmark3 {
       RotationLemma(old(q.contents), j, qc0, q.contents);
       j := j+1;
     }
-  
+
     assert j == k;  
     assert q.contents == old(q.contents)[k..] + old(q.contents)[..k];
+    ghost var qq := q.contents;
     m := q.Dequeue();
+    assert q.contents == qq[1..] && m == qq[0];
+    assert [m] + q.contents == qq;
+    assert |old(q.contents)| == |q.contents| + 1;
+
+    assert q.contents == old(q.contents)[k+1..] + old(q.contents)[..k];  
   }
 
   lemma RotationLemma(O: seq, j: nat, A: seq, C: seq)
diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
index 4205035d..10ad2d3a 100644
--- a/Test/VerifyThis2015/Problem3.dfy
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t"
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino
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;