From 0d003990dd503ceb9cc56e7fb590981e752b5cfa Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Tue, 2 Feb 2016 15:36:36 -0800
Subject: Fix issue 129. When looking for a constructor for which Dafny knows
 how to instantiate all it arguments, don't stop as soon as one instantiable
 constructor is found. Instead, figure out all instantiable constructors and
 then pick the best among these. A simple and reasonable "best" is an
 instantiable constructor that requires a minimal number of already
 constructed type arguments, and to break ties among these, pick the first one
 listed.

---
 Test/dafny4/Bug129.dfy | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 Test/dafny4/Bug129.dfy

(limited to 'Test/dafny4/Bug129.dfy')

diff --git a/Test/dafny4/Bug129.dfy b/Test/dafny4/Bug129.dfy
new file mode 100644
index 00000000..f6cf0fe8
--- /dev/null
+++ b/Test/dafny4/Bug129.dfy
@@ -0,0 +1,12 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Maybe<T> = Some(v:T) | None
+datatype B = B(b:Maybe<B>)
+
+datatype List<T> = Nil | Cons(T, List<T>)
+datatype Tree<T> = Nodes(children: List<Tree<T>>)
+
+
+
+
-- 
cgit v1.2.3