1 files changed, 31 insertions, 0 deletions
diff --git a/Test/dafny4/Bug110.dfy b/Test/dafny4/Bug110.dfy
new file mode 100644
index 00000000..aa808669
--- /dev/null
+++ b/Test/dafny4/Bug110.dfy
@@ -0,0 +1,31 @@
+// RUN: %dafny /compile:0  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Io {
+  predicate AdvanceTime(oldTime:int) { oldTime > 2 }
+  class Time
+  {
+    static method GetTime()
+        ensures AdvanceTime(1);        
+  }
+
+  function MaxPacketSize() : int { 65507 }
+
+  class UdpClient
+  {
+    method Receive()        
+        ensures AdvanceTime(3);       
+
+    method Send() returns(ok:bool)
+        requires 0 <= MaxPacketSize();       
+  }
+}
+
+abstract module Host {
+    import opened Io // Doesn't work.   
+    //import Io          // Works
+}
+
+abstract module Main {
+    import H : Host
+}