diff options
| author |  qunyanm <unknown> | 2016-02-02 15:36:36 -0800 |
|---|---|---|
| committer | qunyanm <unknown> | 2016-02-02 15:36:36 -0800 |
| commit | 0d003990dd503ceb9cc56e7fb590981e752b5cfa (patch) | |
| tree | df346ae8ea4724f406a1b030ecf4b7df6a538c8d /Test | |
| parent | 2be514ca20e1478b6df02ef2b4c2725c319ac934 (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')
| -rw-r--r-- | Test/dafny4/Bug129.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny4/Bug129.dfy.expect | 2 |
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
|