diff options
| author |  Rustan Leino <unknown> | 2014-04-19 21:28:06 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-19 21:28:06 -0700 |
| commit | dbb415aa6de3b15b44d18924b0078a02c7af7a75 (patch) | |
| tree | 2b676536bc83462d13b4a641f8f8c484362b0a4a /Test/dafny0/Modules1.dfy | |
| parent | a05be61a3b45bbabc0c038190d15c48c85f21822 (diff) | |
Fixed bug #33.
Diffstat (limited to 'Test/dafny0/Modules1.dfy')
| -rw-r--r-- | Test/dafny0/Modules1.dfy | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index e9c432f3..3f24212b 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -113,3 +113,20 @@ module Q_M { var q := new Q.Klassy.Init();
}
}
+
+// ----- regression test -----------------------------------------
+
+abstract module Regression {
+ module A
+ {
+ predicate p(m: map)
+
+ lemma m(m: map)
+ ensures exists m :: p(m);
+ }
+
+ abstract module B
+ {
+ import X as A
+ }
+}
|