1 files changed, 82 insertions, 0 deletions
diff --git a/Test/dafny4/Bug125.dfy b/Test/dafny4/Bug125.dfy
new file mode 100644
index 00000000..916dd3f8
--- /dev/null
+++ b/Test/dafny4/Bug125.dfy
@@ -0,0 +1,82 @@
+// RUN: %dafny /compile:0  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+abstract module AbstractModuleA 
+{
+  type T
+} 
+
+abstract module AbstractModuleB 
+{
+  import opened AMA : AbstractModuleA
+
+  method Foo(t:T)
+} 
+
+abstract module AbstractModuleC refines AbstractModuleB 
+{
+  import opened AMA2 : AbstractModuleA
+}
+
+module LibA {
+  class G { 
+    static function f(x:int) : bool {
+      x >= 10
+    }
+  }
+
+  function g() : bool {
+     true
+  }
+}
+
+module LibB {
+  class G { 
+    static function f(x:int) : bool {
+      x < 10
+    }
+  }
+
+  function g() : bool {
+     false
+  }
+}
+
+module R {
+  import opened LibA
+}
+
+module S refines R {
+  import opened LibB
+  method m() {
+    assert g();  // should be LibA.g
+  }
+
+  method m1() {
+   assert G.f(20); // should be LibA.G.f
+  }
+} 
+
+
+module Library {
+
+  class T { }
+
+}
+
+ 
+
+module A {
+
+  import opened Library
+	class T {
+	}
+}
+
+ 
+
+module B refines A {
+
+  datatype T = MakeT(int)  // illegal for the same reason as above, but Dafny fails to issue an error
+
+}