1 files changed, 62 insertions, 0 deletions
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
new file mode 100644
index 00000000..cfefa7fa
--- /dev/null
+++ b/Test/dafny0/Modules1.dfy
@@ -0,0 +1,62 @@
+module A imports B {
+  class X {
+    function Fx(z: Z): int
+      requires z != null;
+      decreases 5, 4, 3;
+    { z.G() }  // fine; this goes to a different module
+  }
+  datatype Y {
+    Cons(int, Y);
+    Empty;
+  }
+}
+
+class C {
+  method M() { }
+  function F(): int { 818 }
+}
+
+method MyMethod() { }
+
+var MyField: int;
+
+module B {
+  class Z {
+    method K() { }
+    function G(): int
+      decreases 10, 8, 6;
+    { 25 }
+  }
+}
+
+static function MyFunction(): int { 5 }
+
+class D { }
+
+method Proc0(x: int)
+  decreases x;
+{
+  if (0 <= x) {
+    call Proc1(x - 1);
+  }
+}
+
+method Proc1(x: int)
+  decreases x;
+{
+  if (0 <= x) {
+    call Proc0(x - 1);
+  }
+}
+
+method Botch0(x: int)
+  decreases x;
+{
+  call Botch1(x - 1);  // error: failure to keep termination metric bounded
+}
+
+method Botch1(x: int)
+  decreases x;
+{
+  call Botch0(x);  // error: failure to decrease termination metric
+}