diff options
| author |  MichalMoskal <unknown> | 2011-02-23 21:26:43 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-23 21:26:43 +0000 |
| commit | 398377309c2d242c1ecac7a3efaa981ab892ae30 (patch) | |
| tree | 6eabb880cf5693bb49284c7c9c29e09c16382a54 /Test/prover/Answer | |
| parent | e592f926a217885ea626685aca57a09570904898 (diff) | |
Add tests for -z3multipleErrors from Shuvendu.
Diffstat (limited to 'Test/prover/Answer')
| -rw-r--r-- | Test/prover/Answer | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/Test/prover/Answer b/Test/prover/Answer new file mode 100644 index 00000000..1ca6407c --- /dev/null +++ b/Test/prover/Answer @@ -0,0 +1,50 @@ +==================== -z3multipleErrors ========================
+
+-------------------- z3mutl.bpl --------------------
+z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ z3mutl.bpl(5,1): start
+ z3mutl.bpl(14,1): L3
+ z3mutl.bpl(20,1): L5
+z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ z3mutl.bpl(5,1): start
+ z3mutl.bpl(11,1): L2
+ z3mutl.bpl(20,1): L5
+z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ z3mutl.bpl(5,1): start
+ z3mutl.bpl(8,1): L1
+ z3mutl.bpl(20,1): L5
+
+Boogie program verifier finished with 0 verified, 3 errors
+
+-------------------- EQ_v2.Eval__v4.Eval_out.bpl --------------------
+EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
+ EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
+EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
+ EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
+EQ_v2.Eval__v4.Eval_out.bpl(2152,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(2120,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ EQ_v2.Eval__v4.Eval_out.bpl(2133,3): AA_INSTR_EQ_BODY
+EQ_v2.Eval__v4.Eval_out.bpl(2192,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(2167,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ EQ_v2.Eval__v4.Eval_out.bpl(2178,3): AA_INSTR_EQ_BODY
+
+Boogie program verifier finished with 6 verified, 4 errors
|