Merge

2 files changed, 17 insertions, 12 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1a9f0509..7186f30f 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

@@ -1672,36 +1672,36 @@ Execution trace:
 Dafny program verifier finished with 38 verified, 11 errors

 

 -------------------- Superposition.dfy --------------------

-
+

 Verifying CheckWellformed$$_0_M0.C.M ...

   [0 proof obligations]  verified

-
+

 Verifying Impl$$_0_M0.C.M ...

   [4 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_0_M0.C.P ...

   [4 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_0_M0.C.Q ...

   [3 proof obligations]  error

 Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-
+

 Verifying CheckWellformed$$_0_M0.C.R ...

   [3 proof obligations]  error

 Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-
+

 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

-
+

 Verifying Impl$$_1_M1.C.M ...

   [1 proof obligation]  verified

-
+

 Verifying CheckWellformed$$_1_M1.C.P ...

   [1 proof obligation]  error

 Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.

@@ -1710,10 +1710,10 @@ Execution trace:
     (0,0): anon7_Else

     (0,0): anon9_Then

     (0,0): anon6

-
+

 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified

-
+

 Verifying CheckWellformed$$_1_M1.C.R ...

   [0 proof obligations]  verified

 

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

+}