diff options
| author |  Jason Koenig <unknown> | 2012-07-11 16:18:30 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-11 16:18:30 -0700 |
| commit | 12497c67126499bc8c6a061d5840c711202ded28 (patch) | |
| tree | 2b07a87ffd9f6c1ce1c7bdc691add866256759db /Test/dafny0/Maps.dfy | |
| parent | 407cfc5cd9bddb106e60d55684a78e660af87f88 (diff) | |
Dafny: fixed translation bug in maps with objects in the domain, added test case
Diffstat (limited to 'Test/dafny0/Maps.dfy')
| -rw-r--r-- | Test/dafny0/Maps.dfy | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy index a49ac3c1..1c245952 100644 --- a/Test/dafny0/Maps.dfy +++ b/Test/dafny0/Maps.dfy @@ -180,3 +180,13 @@ method m14() assert u[1] == 1 && u[3] == 4;
assert domain(u) == {0, 1, 3, 4};
}
+
+class A { var x: int; }
+
+method m15(b: set<A>)
+ requires forall a | a in b :: a != null;
+{
+ var m := map a | a in b :: a.x;
+ var aa := new A;
+ assert aa !in m;
+}
\ No newline at end of file |