From f7ab307779e4d21d706be13acad670d63d0e6537 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Wed, 2 Dec 2015 12:35:54 -0800
Subject: Fix issue 110. Set useImport to true when trying to
 registerTopLevelDecls in MakeAbstractSignature.

---
 Source/Dafny/Resolver.cs      |  2 +-
 Test/dafny4/Bug110.dfy        | 31 +++++++++++++++++++++++++++++++
 Test/dafny4/Bug110.dfy.expect |  2 ++
 3 files changed, 34 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny4/Bug110.dfy
 create mode 100644 Test/dafny4/Bug110.dfy.expect

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 52845c3f..9dc0f829 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1269,7 +1269,7 @@ namespace Microsoft.Dafny
       foreach (var kv in p.TopLevels) {
         mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name));
       }
-      var sig = RegisterTopLevelDecls(mod, false);
+      var sig = RegisterTopLevelDecls(mod, true);
       sig.Refines = p.Refines;
       sig.CompileSignature = p;
       sig.IsAbstract = p.IsAbstract;
diff --git a/Test/dafny4/Bug110.dfy b/Test/dafny4/Bug110.dfy
new file mode 100644
index 00000000..239f18d3
--- /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 as Host
+}
diff --git a/Test/dafny4/Bug110.dfy.expect b/Test/dafny4/Bug110.dfy.expect
new file mode 100644
index 00000000..42fd56a5
--- /dev/null
+++ b/Test/dafny4/Bug110.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 8 verified, 0 errors
-- 
cgit v1.2.3