Dafny: Added definedness checks for all statements (previously, some were missing)

Boogie: Added {:subsumption <n>} attribute to assert statements, which overrides the /subsumption command-line setting

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index 457bc894..7d964061 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -17,7 +17,7 @@ class Benchmark2 {
     var high := a.Length();

 

     while (low < high)

-      invariant 0 <= low && high <= a.Length();

+      invariant 0 <= low && low <= high && high <= a.Length();

       invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);

       invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));

       decreases high - low;