1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
==================== -z3multipleErrors ========================
-------------------- z3mutl.bpl --------------------
z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(7,1): start
z3mutl.bpl(10,1): L1
z3mutl.bpl(22,1): L5
z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(7,1): start
z3mutl.bpl(13,1): L2
z3mutl.bpl(22,1): L5
z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(7,1): start
z3mutl.bpl(16,1): L3
z3mutl.bpl(22,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(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
|
