1 files changed, 11 insertions, 11 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 40725691..7186f30f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -864,7 +864,7 @@ Execution trace:
     (0,0): anon89_Then
     (0,0): anon61
 
-Dafny program verifier finished with 20 verified, 10 errors
+Dafny program verifier finished with 22 verified, 10 errors
 
 -------------------- Termination.dfy --------------------
 Termination.dfy(356,47): Error: failure to decrease termination measure
@@ -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