diff options
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
+ }
+}
|