diff options
Diffstat (limited to 'Test/dafny0/Superposition.dfy.expect')
| -rw-r--r-- | Test/dafny0/Superposition.dfy.expect | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect index b3f2d9ad..2e988bfb 100644 --- a/Test/dafny0/Superposition.dfy.expect +++ b/Test/dafny0/Superposition.dfy.expect @@ -3,13 +3,13 @@ Verifying CheckWellformed$$_0_M0.C.M ... [0 proof obligations] verified
Verifying Impl$$_0_M0.C.M ...
- [4 proof obligations] verified
+ [5 proof obligations] verified
Verifying CheckWellformed$$_0_M0.C.P ...
- [4 proof obligations] verified
+ [6 proof obligations] verified
Verifying CheckWellformed$$_0_M0.C.Q ...
- [3 proof obligations] error
+ [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.
Execution trace:
@@ -17,7 +17,7 @@ Execution trace: (0,0): anon5_Else
Verifying CheckWellformed$$_0_M0.C.R ...
- [3 proof obligations] error
+ [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.
Execution trace:
@@ -31,7 +31,7 @@ Verifying Impl$$_1_M1.C.M ... [1 proof obligation] verified
Verifying CheckWellformed$$_1_M1.C.P ...
- [1 proof obligation] error
+ [2 proof obligations] error
Superposition.dfy(50,15): 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.
Execution trace:
|