diff options
| author |  Jason Koenig <unknown> | 2011-07-13 13:20:05 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-13 13:20:05 -0700 |
| commit | dae4b7981cc7af0c10dde91b0d095ad828f9c706 (patch) | |
| tree | d8fd9dd9bc7278bbfef7a4d8ce82b8c513587d7e /Test/dafny0/AdvancedLHS.dfy | |
| parent | 53d03a352082eeffe52dd6d2ec92f83cbf0b14b1 (diff) | |
Added multiset from sequence axioms, removed array range RHSs. Fixed issue with duplicate array.Length functions in generated Boogie file.
Diffstat (limited to 'Test/dafny0/AdvancedLHS.dfy')
| -rw-r--r-- | Test/dafny0/AdvancedLHS.dfy | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy index cc07cbb5..f1fc7d48 100644 --- a/Test/dafny0/AdvancedLHS.dfy +++ b/Test/dafny0/AdvancedLHS.dfy @@ -34,7 +34,6 @@ class C { if (a != null && 10 <= a.Length) {
a[2] := new C;
- a[4..8] := null;
a[3] := *;
}
if (b != null && 10 <= b.Length0 && 20 <= b.Length1) {
|