- fixed an issue regarding including ghost functions in the compiled interface

- added one more test

1 files changed, 3 insertions, 3 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 7be7f58f..220b5561 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -221,7 +221,7 @@ namespace Microsoft.Dafny {
               List<MemberDecl> members = new List<MemberDecl>();

               foreach (MemberDecl mem in trait.Members)

               {

-                  if (mem.IsStatic)

+                  if (mem.IsStatic && !mem.IsGhost)

                   {

                       if (mem is Function)

                       {

@@ -790,7 +790,7 @@ namespace Microsoft.Dafny {
               {

                   Error("Function {0} has no body", f.FullName);

               }

-              else if (!member.IsStatic) //static members are not included in the target trait

+              else if (!member.IsStatic && !member.IsGhost) //static and ghost members are not included in the target trait

               {

                   Indent(indent);

                   wr.Write("{0} @{1}", TypeName(f.ResultType), f.CompileName);

@@ -836,7 +836,7 @@ namespace Microsoft.Dafny {
               {

                   Error("Method {0} has no body", m.FullName);

               }

-              else if (!member.IsStatic) //static members are not included in the target trait

+              else if (!member.IsStatic && !member.IsGhost) //static and ghost members are not included in the target trait

               {

                   Indent(indent);

                   wr.Write("void @{0}", m.CompileName);