Merge

1 files changed, 29 insertions, 10 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 085ef78a..8f138bcd 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1701,37 +1701,56 @@ Execution trace:
 

 Dafny program verifier finished with 1 verified, 4 errors

 

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

+-------------------- Computations.dfy --------------------

+

+Dafny program verifier finished with 46 verified, 0 errors

+

+-------------------- ComputationsNeg.dfy --------------------

+ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon3_Else

+ComputationsNeg.dfy(8,1): Error BP5003: A postcondition might not hold on this return path.

+ComputationsNeg.dfy(7,17): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+ComputationsNeg.dfy(20,1): Error BP5003: A postcondition might not hold on this return path.

+ComputationsNeg.dfy(19,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 3 verified, 3 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.

@@ -1740,10 +1759,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