From dde9e3560e445addc6cbcfc5bfb219b0bc5cc79f Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Thu, 26 Apr 2012 19:00:08 -0700
Subject: Dafny: fixed bug that had omitted the computation of .DefaultCtor for
 some inductive datatypes

---
 Dafny/Resolver.cs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Dafny')

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 8ab946dc..233f5415 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -497,8 +497,10 @@ namespace Microsoft.Dafny {
         allTypeParameters.PopMarker();
 
         if (dt is IndDatatypeDecl) {
+          var idt = (IndDatatypeDecl)dt;
+          dependencies.AddVertex(idt);
           foreach (Formal p in ctor.Formals) {
-            AddDatatypeDependencyEdge((IndDatatypeDecl)dt, p.Type, dependencies);
+            AddDatatypeDependencyEdge(idt, p.Type, dependencies);
           }
         }
       }
-- 
cgit v1.2.3