Obligations | Alt-Ergo (1.30) | Eprover (1.9.1-001) | Z3 (4.5.0) |
VC for interp_builtin | 0.06 | --- | --- |
VC for interp_term | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | --- | 0.24 | --- |
2. postcondition | --- | 0.24 | --- |
3. exceptional postcondition | --- | 0.27 | --- |
4. exceptional postcondition | 0.32 | --- | --- |
5. exceptional postcondition | 0.08 | --- | --- |
6. exceptional postcondition | 0.08 | --- | --- |
7. exceptional postcondition | 0.07 | --- | --- |
8. exceptional postcondition | 0.17 | --- | --- |
9. exceptional postcondition | 0.07 | --- | --- |
10. exceptional postcondition | 0.08 | --- | --- |
11. exceptional postcondition | 0.08 | --- | --- |
12. postcondition | --- | 43.18 | --- |
13. exceptional postcondition | --- | 0.60 | --- |
14. postcondition | --- | 44.14 | --- |
15. exceptional postcondition | --- | 0.65 | --- |
16. postcondition | 1.81 | --- | --- |
17. exceptional postcondition | 1.89 | --- | --- |
18. exceptional postcondition | 1.80 | --- | --- |
19. exceptional postcondition | 1.81 | --- | --- |
20. exceptional postcondition | 0.12 | --- | --- |
21. exceptional postcondition | 0.33 | --- | --- |
22. exceptional postcondition | 0.32 | --- | --- |
23. postcondition | --- | --- | 0.49 |
24. exceptional postcondition | --- | --- | 0.46 |
25. exceptional postcondition | --- | --- | 0.44 |
26. exceptional postcondition | --- | --- | 0.48 |
27. postcondition | 1.88 | --- | --- |
28. exceptional postcondition | 1.43 | --- | --- |
29. exceptional postcondition | 1.90 | --- | --- |
30. exceptional postcondition | 1.85 | --- | --- |
31. exceptional postcondition | 0.32 | --- | --- |
32. exceptional postcondition | 0.33 | --- | --- |
33. postcondition | 0.06 | --- | --- |
34. exceptional postcondition | 0.06 | --- | --- |
35. exceptional postcondition | 0.06 | --- | --- |
36. exceptional postcondition | 0.05 | --- | --- |
37. postcondition | --- | --- | 0.06 |
38. exceptional postcondition | --- | --- | 0.06 |
39. exceptional postcondition | --- | --- | 0.06 |
40. exceptional postcondition | --- | --- | 0.07 |
41. postcondition | 2.01 | --- | --- |
42. postcondition | 1.69 | --- | --- |
43. exceptional postcondition | --- | --- | 0.07 |
44. exceptional postcondition | --- | --- | 0.07 |
45. exceptional postcondition | 0.11 | --- | --- |
46. exceptional postcondition | 0.35 | --- | --- |
47. exceptional postcondition | 0.32 | --- | --- |
48. postcondition | 0.06 | --- | --- |
49. exceptional postcondition | 0.07 | --- | --- |
50. postcondition | 0.06 | --- | --- |
51. exceptional postcondition | 0.06 | --- | --- |
52. exceptional postcondition | 0.05 | --- | --- |
53. postcondition | 0.07 | --- | --- |
54. postcondition | 0.06 | --- | --- |
55. postcondition | 0.47 | --- | --- |
56. exceptional postcondition | 0.49 | --- | --- |
57. exceptional postcondition | 0.51 | --- | --- |
58. exceptional postcondition | 0.53 | --- | --- |
59. postcondition | 0.55 | --- | --- |
60. exceptional postcondition | 0.48 | --- | --- |
61. exceptional postcondition | 0.50 | --- | --- |
62. exceptional postcondition | 0.47 | --- | --- |
63. postcondition | 0.53 | --- | --- |
64. exceptional postcondition | 0.48 | --- | --- |
65. exceptional postcondition | 0.55 | --- | --- |
66. exceptional postcondition | 0.50 | --- | --- |
67. postcondition | 0.52 | --- | --- |
68. exceptional postcondition | 0.49 | --- | --- |
69. exceptional postcondition | 0.50 | --- | --- |
70. exceptional postcondition | 0.51 | --- | --- |
VC for interp_for | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | --- | 0.28 | --- |
2. postcondition | 0.18 | --- | --- |
3. exceptional postcondition | 0.12 | --- | --- |
4. exceptional postcondition | 0.14 | --- | --- |
5. exceptional postcondition | 0.14 | --- | --- |
6. postcondition | --- | --- | 0.12 |
7. exceptional postcondition | --- | --- | 0.12 |
8. exceptional postcondition | --- | --- | 0.12 |
9. exceptional postcondition | --- | --- | 0.11 |
10. exceptional postcondition | 0.15 | --- | --- |
11. exceptional postcondition | --- | --- | 0.11 |
12. exceptional postcondition | 2.05 | --- | --- |
VC for interp_call | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | --- | 0.31 | --- |
2. postcondition | 0.07 | --- | --- |
3. exceptional postcondition | 0.07 | --- | --- |
4. exceptional postcondition | 0.07 | --- | --- |
5. postcondition | 0.08 | --- | --- |
6. exceptional postcondition | 0.07 | --- | --- |
7. exceptional postcondition | 0.08 | --- | --- |
8. postcondition | 0.40 | --- | --- |
9. exceptional postcondition | 0.39 | --- | --- |
10. exceptional postcondition | 0.24 | --- | --- |
11. postcondition | 0.32 | --- | --- |
12. exceptional postcondition | 0.42 | --- | --- |
13. exceptional postcondition | 0.26 | --- | --- |
VC for interp_sexpr | 0.09 | --- | --- |
VC for interp_sexpr_aux | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.04 | --- | --- |
2. postcondition | --- | --- | --- |
eliminate_let | | | |
| 1. VC for interp_sexpr_aux | --- | --- | --- |
split_all_full | | | |
| 1. VC for interp_sexpr_aux | 0.10 | --- | --- |
2. VC for interp_sexpr_aux | 0.04 | --- | --- |
3. VC for interp_sexpr_aux | 0.42 | --- | --- |
4. VC for interp_sexpr_aux | 0.16 | --- | --- |
5. VC for interp_sexpr_aux | 0.48 | --- | --- |
6. VC for interp_sexpr_aux | 0.51 | --- | --- |
7. VC for interp_sexpr_aux | 0.14 | --- | --- |
8. VC for interp_sexpr_aux | 0.54 | --- | --- |
VC for interp_sfrag_aux | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.05 | --- | --- |
2. postcondition | 0.04 | --- | --- |
3. postcondition | --- | --- | 0.06 |
4. postcondition | --- | --- | 0.06 |
5. postcondition | --- | --- | --- |
inversion_pr | | | |
| 1. postcondition | 0.06 | --- | --- |
2. postcondition | 0.05 | --- | --- |
3. postcondition | 0.05 | --- | --- |
4. postcondition | 0.06 | --- | --- |
5. postcondition | 0.06 | --- | --- |
6. postcondition | 0.05 | --- | --- |
7. postcondition | 0.05 | --- | --- |
8. postcondition | 0.05 | --- | --- |
9. postcondition | 0.06 | --- | --- |
10. postcondition | 0.06 | --- | --- |
11. postcondition | 0.06 | --- | --- |
12. postcondition | 0.06 | --- | --- |
13. postcondition | 0.05 | --- | --- |
14. postcondition | 0.06 | --- | --- |
15. postcondition | 0.06 | --- | --- |
16. postcondition | 0.06 | --- | --- |
17. postcondition | 0.06 | --- | --- |
18. postcondition | --- | --- | 2.39 |
19. postcondition | 0.06 | --- | --- |
20. postcondition | 0.05 | --- | --- |
21. postcondition | 0.05 | --- | --- |
22. postcondition | 0.05 | --- | --- |
VC for interp_lexpr | 0.07 | --- | --- |
VC for interp_lexpr_aux | 3.70 | --- | --- |
VC for interp_lfrag_aux | 0.08 | --- | --- |
VC for interp_process | 0.80 | --- | --- |
Obligations | Alt-Ergo (1.30) | CVC4 (1.5-prerelease) | Z3 (4.5.0) |
VC for interp_builtin | 0.04 | --- | --- |
VC for interp_term | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 1.66 | --- | --- |
2. postcondition | 1.12 | --- | --- |
3. exceptional postcondition | 1.74 | --- | --- |
4. precondition | 2.54 | --- | --- |
5. variant decrease | 0.09 | --- | --- |
6. precondition | 1.94 | --- | --- |
7. exceptional postcondition | 0.71 | --- | --- |
8. exceptional postcondition | 0.14 | --- | --- |
9. exceptional postcondition | 0.13 | --- | --- |
10. exceptional postcondition | 0.13 | --- | --- |
11. precondition | 2.44 | --- | --- |
12. variant decrease | 0.09 | --- | --- |
13. precondition | 1.95 | --- | --- |
14. exceptional postcondition | 0.69 | --- | --- |
15. exceptional postcondition | 0.12 | --- | --- |
16. exceptional postcondition | 0.13 | --- | --- |
17. exceptional postcondition | 0.11 | --- | --- |
18. precondition | 2.49 | --- | --- |
19. variant decrease | 0.10 | --- | --- |
20. precondition | 1.82 | --- | --- |
21. postcondition | --- | --- | 1.86 |
22. exceptional postcondition | --- | --- | 1.02 |
23. precondition | 2.69 | --- | --- |
24. variant decrease | 0.08 | --- | --- |
25. precondition | 1.86 | --- | --- |
26. postcondition | --- | --- | 1.31 |
27. exceptional postcondition | --- | --- | 1.23 |
28. precondition | 1.75 | --- | --- |
29. variant decrease | 0.05 | --- | --- |
30. precondition | 3.31 | --- | --- |
31. precondition | --- | --- | 0.74 |
32. variant decrease | 0.15 | --- | --- |
33. precondition | --- | --- | 3.16 |
34. postcondition | --- | --- | 0.52 |
35. exceptional postcondition | --- | --- | 0.55 |
36. exceptional postcondition | --- | --- | 0.52 |
37. exceptional postcondition | --- | --- | 0.55 |
38. exceptional postcondition | --- | --- | 0.64 |
39. exceptional postcondition | --- | --- | 1.69 |
40. exceptional postcondition | --- | --- | 1.88 |
41. precondition | 1.91 | --- | --- |
42. variant decrease | 0.07 | --- | --- |
43. precondition | --- | --- | 0.44 |
44. precondition | --- | --- | 1.24 |
45. variant decrease | 0.06 | --- | --- |
46. precondition | --- | --- | 2.39 |
47. postcondition | --- | --- | 0.51 |
48. exceptional postcondition | --- | --- | 0.49 |
49. exceptional postcondition | --- | --- | 0.48 |
50. exceptional postcondition | --- | --- | 0.45 |
51. precondition | --- | --- | 1.52 |
52. variant decrease | 0.07 | --- | --- |
53. precondition | --- | --- | 1.18 |
54. postcondition | --- | --- | 0.44 |
55. exceptional postcondition | --- | --- | 0.41 |
56. exceptional postcondition | --- | --- | 0.48 |
57. exceptional postcondition | --- | --- | 0.48 |
58. exceptional postcondition | --- | --- | 1.97 |
59. exceptional postcondition | --- | --- | 1.97 |
60. precondition | 2.70 | --- | --- |
61. variant decrease | 0.09 | --- | --- |
62. precondition | 1.87 | --- | --- |
63. variant decrease | 0.09 | --- | --- |
64. precondition | --- | --- | 3.20 |
65. postcondition | 0.08 | --- | --- |
66. exceptional postcondition | 0.07 | --- | --- |
67. exceptional postcondition | 0.05 | --- | --- |
68. exceptional postcondition | 0.05 | --- | --- |
69. precondition | 0.91 | --- | --- |
70. variant decrease | 0.20 | --- | --- |
71. precondition | --- | --- | 0.46 |
72. precondition | --- | --- | 0.90 |
73. variant decrease | 0.25 | --- | --- |
74. precondition | --- | --- | 1.54 |
75. precondition | --- | --- | 2.58 |
76. variant decrease | 0.23 | --- | --- |
77. precondition | --- | --- | 2.86 |
78. postcondition | --- | --- | 0.48 |
79. exceptional postcondition | --- | --- | 0.51 |
80. exceptional postcondition | --- | --- | 0.56 |
81. exceptional postcondition | --- | --- | 0.57 |
82. postcondition | --- | --- | 4.23 |
83. postcondition | --- | --- | 4.14 |
84. exceptional postcondition | --- | --- | 2.03 |
85. exceptional postcondition | --- | --- | 2.15 |
86. exceptional postcondition | --- | --- | 0.63 |
87. exceptional postcondition | --- | --- | 1.97 |
88. exceptional postcondition | --- | --- | 1.93 |
89. precondition | 2.76 | --- | --- |
90. variant decrease | 0.06 | --- | --- |
91. precondition | 1.69 | --- | --- |
92. postcondition | 0.11 | --- | --- |
93. exceptional postcondition | 0.14 | --- | --- |
94. exceptional postcondition | 0.09 | --- | --- |
95. postcondition | 0.15 | --- | --- |
96. exceptional postcondition | 0.14 | --- | --- |
97. postcondition | 0.09 | --- | --- |
98. exceptional postcondition | 0.14 | --- | --- |
99. precondition | 2.52 | --- | --- |
100. variant decrease | 0.08 | --- | --- |
101. precondition | 2.18 | --- | --- |
102. variant decrease | 0.09 | --- | --- |
103. precondition | --- | --- | 2.50 |
104. postcondition | 0.06 | --- | --- |
105. exceptional postcondition | 0.05 | --- | --- |
106. exceptional postcondition | 0.06 | --- | --- |
107. postcondition | 1.45 | --- | --- |
108. postcondition | 2.15 | --- | --- |
109. precondition | 2.70 | --- | --- |
110. variant decrease | 0.10 | --- | --- |
111. precondition | 2.60 | --- | --- |
112. variant decrease | 0.16 | --- | --- |
113. precondition | --- | --- | 2.45 |
114. postcondition | 1.75 | --- | --- |
115. exceptional postcondition | 1.87 | --- | --- |
116. exceptional postcondition | 1.95 | --- | --- |
117. exceptional postcondition | 1.82 | --- | --- |
118. variant decrease | 0.14 | --- | --- |
119. precondition | --- | --- | 1.06 |
120. postcondition | 1.86 | --- | --- |
121. exceptional postcondition | 2.03 | --- | --- |
122. exceptional postcondition | 1.94 | --- | --- |
123. exceptional postcondition | 1.85 | --- | --- |
124. variant decrease | 0.16 | --- | --- |
125. precondition | --- | --- | 2.47 |
126. postcondition | 1.90 | --- | --- |
127. exceptional postcondition | 2.04 | --- | --- |
128. exceptional postcondition | 2.02 | --- | --- |
129. exceptional postcondition | 1.95 | --- | --- |
130. variant decrease | 0.14 | --- | --- |
131. precondition | --- | --- | 2.69 |
132. postcondition | 1.75 | --- | --- |
133. exceptional postcondition | 1.89 | --- | --- |
134. exceptional postcondition | 1.84 | --- | --- |
135. exceptional postcondition | 1.84 | --- | --- |
VC for interp_for | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.15 | --- | --- |
2. precondition | 0.29 | --- | --- |
3. variant decrease | 0.07 | --- | --- |
4. precondition | 0.43 | --- | --- |
5. postcondition | 0.16 | --- | --- |
6. exceptional postcondition | 0.15 | --- | --- |
7. exceptional postcondition | 0.13 | --- | --- |
8. exceptional postcondition | 0.13 | --- | --- |
9. precondition | 0.17 | --- | --- |
10. variant decrease | 0.07 | --- | --- |
11. precondition | 0.45 | --- | --- |
12. precondition | --- | 0.22 | --- |
13. variant decrease | 0.14 | --- | --- |
14. precondition | --- | 0.20 | --- |
15. postcondition | 10.85 | --- | --- |
16. exceptional postcondition | --- | 0.47 | --- |
17. exceptional postcondition | 12.33 | --- | --- |
18. exceptional postcondition | 12.03 | --- | --- |
19. exceptional postcondition | 17.01 | --- | --- |
20. exceptional postcondition | 17.31 | --- | --- |
21. exceptional postcondition | 16.76 | --- | --- |
VC for interp_call | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.43 | --- | --- |
2. postcondition | 0.26 | --- | --- |
3. exceptional postcondition | 0.24 | --- | --- |
4. exceptional postcondition | 0.29 | --- | --- |
5. postcondition | 0.25 | --- | --- |
6. exceptional postcondition | 0.25 | --- | --- |
7. exceptional postcondition | 0.34 | --- | --- |
8. precondition | 0.70 | --- | --- |
9. variant decrease | 0.07 | --- | --- |
10. precondition | 2.03 | --- | --- |
11. postcondition | --- | --- | 0.06 |
12. exceptional postcondition | --- | --- | 0.05 |
13. exceptional postcondition | 0.73 | --- | --- |
14. postcondition | --- | --- | 0.06 |
15. exceptional postcondition | --- | --- | 0.05 |
16. exceptional postcondition | 0.75 | --- | --- |
VC for interp_sexpr | 0.76 | --- | --- |
VC for interp_sexpr_aux | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.09 | --- | --- |
2. precondition | 0.13 | --- | --- |
3. variant decrease | 0.07 | --- | --- |
4. precondition | 0.10 | --- | --- |
5. variant decrease | 0.08 | --- | --- |
6. precondition | --- | 0.27 | --- |
7. postcondition | --- | 0.23 | --- |
VC for interp_sfrag_aux | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.11 | --- | --- |
2. postcondition | 0.05 | --- | --- |
3. postcondition | 0.26 | --- | --- |
4. postcondition | 0.27 | --- | --- |
5. precondition | 0.17 | --- | --- |
6. variant decrease | 0.05 | --- | --- |
7. precondition | 0.28 | --- | --- |
8. postcondition | 1.02 | --- | --- |
9. postcondition | 0.11 | --- | --- |
10. postcondition | 1.08 | --- | --- |
11. postcondition | 1.07 | --- | --- |
VC for interp_lexpr | 0.78 | --- | --- |
VC for interp_lexpr_aux | --- | --- | --- |
split_goal_wp | | | |
| 1. postcondition | 0.07 | --- | --- |
2. precondition | 0.10 | --- | --- |
3. variant decrease | 0.06 | --- | --- |
4. precondition | 0.10 | --- | --- |
5. variant decrease | 0.08 | --- | --- |
6. precondition | --- | 0.21 | --- |
7. postcondition | --- | --- | 1.94 |
VC for interp_lfrag_aux | 1.17 | --- | --- |
VC for interp_process | --- | --- | --- |
split_goal_wp | | | |
| 1. precondition | 2.51 | --- | --- |
2. variant decrease | 0.09 | --- | --- |
3. precondition | 1.71 | --- | --- |
4. postcondition | 2.40 | --- | --- |
5. postcondition | 0.13 | --- | --- |
6. postcondition | 1.64 | --- | --- |
7. postcondition | 1.66 | --- | --- |