diff options
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 10 |
2 files changed, 11 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 070aa6be..2463b0e5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -209,7 +209,7 @@ Execution trace: (0,0): anon15
(0,0): anon25_Else
-Dafny program verifier finished with 39 verified, 14 errors
+Dafny program verifier finished with 41 verified, 14 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index ef2049a3..a5f02dc6 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -308,3 +308,13 @@ method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int) assert x == y;
}
}
+
+// ----------------------- tests that involve sequences of boxed booleans --------
+
+ghost method M(zeros: seq<bool>, Z: bool)
+ requires 1 <= |zeros| && Z == false;
+ requires forall k :: 0 <= k && k < |zeros| ==> zeros[k] == Z;
+{
+ var x := [Z];
+ assert zeros[0..1] == [Z];
+}
|