diff options
| author |  wuestholz <unknown> | 2011-12-02 16:13:22 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-12-02 16:13:22 +0100 |
| commit | cc250f5537c8d1d8ff797a9a9ee1183cac1f39c3 (patch) | |
| tree | c00843c92bf994cf249eb0f7577890c159df3d7b | |
| parent | 915bb458f688ed0d9546239a410300e3c4bf3fa5 (diff) | |
Updated the 'Answer' file for test2.
| -rw-r--r-- | Test/test2/Answer | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer index da75f4f5..9625c4db 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -381,6 +381,14 @@ Execution trace: Boogie program verifier finished with 1 verified, 3 errors
+-------------------- LambdaOldExpressions.bpl --------------------
+LambdaOldExpressions.bpl(27,1): Error BP5003: A postcondition might not hold on this return path.
+LambdaOldExpressions.bpl(21,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ LambdaOldExpressions.bpl(25,7): anon0
+
+Boogie program verifier finished with 2 verified, 1 error
+
-------------------- SelectiveChecking.bpl --------------------
SelectiveChecking.bpl(17,3): Error BP5001: This assertion might not hold.
Execution trace:
|