Minor change to a test case

1 files changed, 5 insertions, 5 deletions

diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy
index d4c98424..aa131f98 100644
--- a/Test/dafny0/SeqFromArray.dfy
+++ b/Test/dafny0/SeqFromArray.dfy
@@ -58,7 +58,7 @@ method L(a: array<int>, c: array<int>, n: nat)
 

 method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)

   requires a != null && c != null

-  requires k + m <= a.Length;

+  requires k + m <= a.Length

   requires l + n <= c.Length

 {

   if {

@@ -79,12 +79,12 @@ method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)
         } else if * {

           assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];

         }

-      } 

-    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];

+      }

     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];

   }

 }