Obligations | Alt-Ergo (1.01) | CVC4 (1.4) |
VC for l_mdl_ok | 0.03 | --- |
VC for m_mdl_ok | 0.03 | --- |
VC for lm_mdl_ok | 0.04 | --- |
VC for lm_mdl_same | 0.08 | --- |
VC for l_compare_zero | 0.03 | --- |
VC for m_collapse_ok | --- | --- |
split_goal_wp | | |
| 1. postcondition | --- | 0.05 |
2. postcondition | --- | 0.06 |
3. precondition | 0.01 | --- |
4. assertion | 0.16 | --- |
5. postcondition | 0.39 | --- |
6. postcondition | --- | 0.08 |
7. postcondition | 2.87 | --- |
8. postcondition | --- | 0.06 |
VC for lm_collapse_ok | 0.09 | --- |
VC for cat_rev_ok | 0.09 | --- |
VC for lm_dump_ok | 0.16 | --- |
VC for lm_merge_ok | --- | --- |
split_goal_wp | | |
| 1. precondition | 0.02 | --- |
2. precondition | 0.02 | --- |
3. precondition | 0.02 | --- |
4. precondition | 0.02 | --- |
5. postcondition | 0.02 | --- |
6. postcondition | 0.28 | --- |
7. precondition | 0.02 | --- |
8. precondition | 0.02 | --- |
9. precondition | 0.03 | --- |
10. precondition | 0.03 | --- |
11. variant decrease | 0.03 | --- |
12. precondition | 0.02 | --- |
13. precondition | 0.03 | --- |
14. postcondition | 0.02 | --- |
15. postcondition | --- | 1.87 |
VC for cat_ok | 0.12 | --- |
VC for m_mul_ok | 0.11 | --- |
VC for m_distribute_ok | 0.08 | --- |
VC for lm_distribute_ok | 0.19 | --- |
VC for lm_opp_ok | --- | --- |
split_goal_wp | | |
| 1. postcondition | 0.02 | --- |
2. postcondition | 0.03 | --- |
3. variant decrease | 0.03 | --- |
4. precondition | 0.03 | --- |
5. precondition | 0.03 | --- |
6. precondition | 0.04 | --- |
7. postcondition | 0.03 | --- |
8. postcondition | --- | 0.13 |
extends_rw | 0.02 | --- |
VC for symb_env | 0.02 | --- |
VC for symb_reg | 0.07 | --- |
VC for symb_opp | 0.03 | --- |
VC for symb_add | 0.10 | --- |
VC for symb_sub | 0.04 | --- |
VC for symb_mul | 0.03 | --- |
VC for harness | --- | --- |
split_goal_wp | | |
| 1. precondition | --- | --- |
compute_specified | | |
| 1. precondition | --- | --- |
simplify_trivial_quantification_in_goal | | |
| 1. precondition | --- | --- |
compute_specified | | |
| 1. precondition | --- | --- |
introduce_premises | | |
| 1. precondition | 0.03 | --- |
2. precondition | 0.06 | --- |
3. precondition | --- | --- |
compute_specified | | |
| 1. precondition | --- | --- |
simplify_trivial_quantification_in_goal | | |
| 1. precondition | --- | --- |
compute_specified | | |
| 1. precondition | --- | --- |
introduce_premises | | |
| 1. precondition | 0.02 | --- |
4. precondition | 0.07 | --- |
5. precondition | 0.04 | --- |
6. precondition | 0.06 | --- |
7. precondition | --- | --- |
compute_specified | | |
| 1. precondition | --- | --- |
simplify_trivial_quantification_in_goal | | |
| 1. precondition | --- | --- |
compute_specified | | |
| 1. precondition | --- | --- |
introduce_premises | | |
| 1. precondition | 0.02 | --- |
8. precondition | 0.07 | --- |
9. precondition | 0.06 | --- |
10. precondition | 0.05 | --- |
11. precondition | --- | --- |
compute_specified | | |
| 1. precondition | --- | --- |
simplify_trivial_quantification_in_goal | | |
| 1. precondition | --- | --- |
compute_specified | | |
| 1. precondition | --- | --- |
introduce_premises | | |
| 1. precondition | 0.02 | --- |
12. precondition | 0.10 | --- |
13. precondition | 0.05 | --- |
14. precondition | 0.05 | --- |
15. precondition | 0.06 | --- |
16. precondition | 0.06 | --- |
17. precondition | 0.06 | --- |
18. precondition | 0.07 | --- |
19. precondition | 0.07 | --- |
20. precondition | 0.06 | --- |
21. precondition | 0.07 | --- |
22. precondition | 0.07 | --- |
23. precondition | 0.07 | --- |
24. precondition | 0.07 | --- |
25. precondition | 0.08 | --- |
26. precondition | 0.07 | --- |
27. precondition | 0.07 | --- |
28. precondition | 0.08 | --- |
29. precondition | 0.08 | --- |
30. precondition | 0.08 | --- |
31. precondition | 0.09 | --- |
32. precondition | 0.07 | --- |
33. assertion | --- | --- |
compute_specified | | |
| 1. assertion | --- | --- |
simplify_trivial_quantification_in_goal | | |
| 1. assertion | --- | --- |
compute_specified | | |
|