From f75149436835b10ebba203a7a72ba52e723be03b Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 20 Jun 2013 16:10:48 -0700
Subject: 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).

---
 Test/dafny0/Answer        | 2 +-
 Test/dafny0/Datatypes.dfy | 7 ++++++-
 2 files changed, 7 insertions(+), 2 deletions(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4a914de0..40725691 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1131,7 +1131,7 @@ Execution trace:
     (0,0): anon0
     (0,0): anon5_Then
 
-Dafny program verifier finished with 38 verified, 6 errors
+Dafny program verifier finished with 39 verified, 6 errors
 
 -------------------- Coinductive.dfy --------------------
 Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
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
+}
-- 
cgit v1.2.3