diff options
Diffstat (limited to 'Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect')
| -rw-r--r-- | Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect new file mode 100644 index 00000000..628a1fe4 --- /dev/null +++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect @@ -0,0 +1,28 @@ +EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path. +EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold. +Execution trace: + EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY + EQ_v2.Eval__v4.Eval_out.bpl(1864,3): inline$v2.Eval$0$label_11_case_2#2 + EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2 + EQ_v2.Eval__v4.Eval_out.bpl(1991,3): inline$v4.Eval$0$label_11_case_2#2 + EQ_v2.Eval__v4.Eval_out.bpl(2013,3): inline$v4.Eval$0$label_14_true#2 + EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2 +EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path. +EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold. +Execution trace: + EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY + EQ_v2.Eval__v4.Eval_out.bpl(1877,3): inline$v2.Eval$0$label_11_case_1#2 + EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2 + EQ_v2.Eval__v4.Eval_out.bpl(2034,3): inline$v4.Eval$0$label_11_case_1#2 + EQ_v2.Eval__v4.Eval_out.bpl(2056,3): inline$v4.Eval$0$label_13_true#2 + EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2 +EQ_v2.Eval__v4.Eval_out.bpl(2154,5): Error BP5003: A postcondition might not hold on this return path. +EQ_v2.Eval__v4.Eval_out.bpl(2122,3): Related location: This is the postcondition that might not hold. +Execution trace: + EQ_v2.Eval__v4.Eval_out.bpl(2135,3): AA_INSTR_EQ_BODY +EQ_v2.Eval__v4.Eval_out.bpl(2194,5): Error BP5003: A postcondition might not hold on this return path. +EQ_v2.Eval__v4.Eval_out.bpl(2169,3): Related location: This is the postcondition that might not hold. +Execution trace: + EQ_v2.Eval__v4.Eval_out.bpl(2180,3): AA_INSTR_EQ_BODY + +Boogie program verifier finished with 6 verified, 4 errors |