1 files changed, 11 insertions, 11 deletions
diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect
index 4b8e354f..04ec2f7d 100644
--- a/Test/dafny0/Superposition.dfy.expect
+++ b/Test/dafny0/Superposition.dfy.expect
@@ -10,19 +10,19 @@ Verifying CheckWellformed$$_0_M0.C.P ...
 
 Verifying CheckWellformed$$_0_M0.C.Q ...
   [5 proof obligations]  error
-Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy(28,26): Related location: This is the postcondition that might not hold.
+Superposition.dfy(27,14): Error BP5003: A postcondition might not hold on this return path.
+Superposition.dfy(28,25): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-    (0,0): anon5_Else
+    (0,0): anon7_Else
 
 Verifying CheckWellformed$$_0_M0.C.R ...
   [5 proof obligations]  error
-Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy(34,26): Related location: This is the postcondition that might not hold.
+Superposition.dfy(33,14): Error BP5003: A postcondition might not hold on this return path.
+Superposition.dfy(34,25): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-    (0,0): anon5_Else
+    (0,0): anon7_Else
 
 Verifying CheckWellformed$$_1_M1.C.M ...
   [0 proof obligations]  verified
@@ -32,13 +32,13 @@ Verifying Impl$$_1_M1.C.M ...
 
 Verifying CheckWellformed$$_1_M1.C.P ...
   [2 proof obligations]  error
-Superposition.dfy(50,25): Error BP5003: A postcondition might not hold on this return path.
-Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.
+Superposition.dfy(50,24): Error BP5003: A postcondition might not hold on this return path.
+Superposition.dfy[M1](22,25): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-    (0,0): anon7_Else
-    (0,0): anon9_Then
-    (0,0): anon6
+    (0,0): anon9_Else
+    (0,0): anon11_Then
+    (0,0): anon8
 
 Verifying CheckWellformed$$_1_M1.C.Q ...
   [0 proof obligations]  verified