summaryrefslogtreecommitdiff
path: root/Test/dafny4
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2016-02-02 15:36:36 -0800
committerGravatar qunyanm <unknown>2016-02-02 15:36:36 -0800
commit0d003990dd503ceb9cc56e7fb590981e752b5cfa (patch)
treedf346ae8ea4724f406a1b030ecf4b7df6a538c8d /Test/dafny4
parent2be514ca20e1478b6df02ef2b4c2725c319ac934 (diff)
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.
Diffstat (limited to 'Test/dafny4')
-rw-r--r--Test/dafny4/Bug129.dfy12
-rw-r--r--Test/dafny4/Bug129.dfy.expect2
2 files changed, 14 insertions, 0 deletions
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>>)
+
+
+
+
diff --git a/Test/dafny4/Bug129.dfy.expect b/Test/dafny4/Bug129.dfy.expect
new file mode 100644
index 00000000..a1c1f7b9
--- /dev/null
+++ b/Test/dafny4/Bug129.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 0 verified, 0 errors