One more test case for the "datatype constructor cases" axiom, namely the example given in Issue 18 on dafny.codeplex.com (which was fixed in the previous check-in).

1 files changed, 6 insertions, 1 deletions

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index f2884b6a..5598844d 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -246,7 +246,7 @@ function FwdBugFunction(f: Fwd): bool
   // There was once a bug in Dafny, where this had caused an ill-defined Boogie program.

 }

 

-datatype Fwd = FwdNil | FwdCons(int, w: Fwd);

+datatype Fwd = FwdNil | FwdCons(k: int, w: Fwd);

 

 method TestAllCases(f: Fwd)

 {

@@ -267,3 +267,8 @@ class ContainsFwd {
     assert fwd.FwdNil? || fwd.FwdCons?;

   }

 }

+

+function foo(f: Fwd): int

+{

+  if f.FwdNil? then 0 else f.k

+}