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, 3 insertions, 3 deletions

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index d45db684..37b73cba 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -61,10 +61,10 @@ class Benchmark3 {
     

     var n := 0;

 	while (n < |q.contents|)

-		invariant n <=|q.contents| ;

-		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);

+		invariant n <= |q.contents|;

 		invariant n == |p|;

-		decreases |q.contents| -n;

+		invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);

+		decreases |q.contents| - n;

    {

 		p := p + [n];

 		n := n + 1;