From 1975381d81aabbc16ae552685b5976cad531122a Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Sun, 5 Apr 2015 22:20:53 -0700
Subject: Fixed missing case in previous check-in

---
 Source/Dafny/Compiler.cs | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 7b63f65b..d43c57c6 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -796,8 +796,12 @@ namespace Microsoft.Dafny {
             }
           } else if (f.IsGhost) {
             // nothing to compile, but we do check for assumes
-            var v = new CheckHasNoAssumes_Visitor(this);
-            v.Visit(f.Body);
+            if (f.Body == null) {
+              Contract.Assert(c is TraitDecl && !f.IsStatic);
+            } else {
+              var v = new CheckHasNoAssumes_Visitor(this);
+              v.Visit(f.Body);
+            }
           } else if (c is TraitDecl && !forCompanionClass) {
             // include it, unless it's static
             if (!f.IsStatic) {
@@ -832,8 +836,12 @@ namespace Microsoft.Dafny {
             }
           } else if (m.IsGhost) {
             // nothing to compile, but we do check for assumes
-            var v = new CheckHasNoAssumes_Visitor(this);
-            v.Visit(m.Body);
+            if (m.Body == null) {
+              Contract.Assert(c is TraitDecl && !m.IsStatic);
+            } else {
+              var v = new CheckHasNoAssumes_Visitor(this);
+              v.Visit(m.Body);
+            }
           } else if (c is TraitDecl && !forCompanionClass) {
             // include it, unless it's static
             if (!m.IsStatic) {
-- 
cgit v1.2.3