Why3 Proof Results for Project "interpreter"

Theory "interpreter.CorrectTermInterpreter": fully verified in 138.96 s

ObligationsAlt-Ergo (1.30)Eprover (1.9.1-001)Z3 (4.5.0)
VC for interp_builtin0.06------
VC for interp_term---------
split_goal_wp
  1. postcondition---0.24---
2. postcondition---0.24---
3. exceptional postcondition---0.27---
4. exceptional postcondition0.32------
5. exceptional postcondition0.08------
6. exceptional postcondition0.08------
7. exceptional postcondition0.07------
8. exceptional postcondition0.17------
9. exceptional postcondition0.07------
10. exceptional postcondition0.08------
11. exceptional postcondition0.08------
12. postcondition---43.18---
13. exceptional postcondition---0.60---
14. postcondition---44.14---
15. exceptional postcondition---0.65---
16. postcondition1.81------
17. exceptional postcondition1.89------
18. exceptional postcondition1.80------
19. exceptional postcondition1.81------
20. exceptional postcondition0.12------
21. exceptional postcondition0.33------
22. exceptional postcondition0.32------
23. postcondition------0.49
24. exceptional postcondition------0.46
25. exceptional postcondition------0.44
26. exceptional postcondition------0.48
27. postcondition1.88------
28. exceptional postcondition1.43------
29. exceptional postcondition1.90------
30. exceptional postcondition1.85------
31. exceptional postcondition0.32------
32. exceptional postcondition0.33------
33. postcondition0.06------
34. exceptional postcondition0.06------
35. exceptional postcondition0.06------
36. exceptional postcondition0.05------
37. postcondition------0.06
38. exceptional postcondition------0.06
39. exceptional postcondition------0.06
40. exceptional postcondition------0.07
41. postcondition2.01------
42. postcondition1.69------
43. exceptional postcondition------0.07
44. exceptional postcondition------0.07
45. exceptional postcondition0.11------
46. exceptional postcondition0.35------
47. exceptional postcondition0.32------
48. postcondition0.06------
49. exceptional postcondition0.07------
50. postcondition0.06------
51. exceptional postcondition0.06------
52. exceptional postcondition0.05------
53. postcondition0.07------
54. postcondition0.06------
55. postcondition0.47------
56. exceptional postcondition0.49------
57. exceptional postcondition0.51------
58. exceptional postcondition0.53------
59. postcondition0.55------
60. exceptional postcondition0.48------
61. exceptional postcondition0.50------
62. exceptional postcondition0.47------
63. postcondition0.53------
64. exceptional postcondition0.48------
65. exceptional postcondition0.55------
66. exceptional postcondition0.50------
67. postcondition0.52------
68. exceptional postcondition0.49------
69. exceptional postcondition0.50------
70. exceptional postcondition0.51------
VC for interp_for---------
split_goal_wp
  1. postcondition---0.28---
2. postcondition0.18------
3. exceptional postcondition0.12------
4. exceptional postcondition0.14------
5. exceptional postcondition0.14------
6. postcondition------0.12
7. exceptional postcondition------0.12
8. exceptional postcondition------0.12
9. exceptional postcondition------0.11
10. exceptional postcondition0.15------
11. exceptional postcondition------0.11
12. exceptional postcondition2.05------
VC for interp_call---------
split_goal_wp
  1. postcondition---0.31---
2. postcondition0.07------
3. exceptional postcondition0.07------
4. exceptional postcondition0.07------
5. postcondition0.08------
6. exceptional postcondition0.07------
7. exceptional postcondition0.08------
8. postcondition0.40------
9. exceptional postcondition0.39------
10. exceptional postcondition0.24------
11. postcondition0.32------
12. exceptional postcondition0.42------
13. exceptional postcondition0.26------
VC for interp_sexpr0.09------
VC for interp_sexpr_aux---------
split_goal_wp
  1. postcondition0.04------
2. postcondition---------
eliminate_let
  1. VC for interp_sexpr_aux---------
split_all_full
  1. VC for interp_sexpr_aux0.10------
2. VC for interp_sexpr_aux0.04------
3. VC for interp_sexpr_aux0.42------
4. VC for interp_sexpr_aux0.16------
5. VC for interp_sexpr_aux0.48------
6. VC for interp_sexpr_aux0.51------
7. VC for interp_sexpr_aux0.14------
8. VC for interp_sexpr_aux0.54------
VC for interp_sfrag_aux---------
split_goal_wp
  1. postcondition0.05------
2. postcondition0.04------
3. postcondition------0.06
4. postcondition------0.06
5. postcondition---------
inversion_pr
  1. postcondition0.06------
2. postcondition0.05------
3. postcondition0.05------
4. postcondition0.06------
5. postcondition0.06------
6. postcondition0.05------
7. postcondition0.05------
8. postcondition0.05------
9. postcondition0.06------
10. postcondition0.06------
11. postcondition0.06------
12. postcondition0.06------
13. postcondition0.05------
14. postcondition0.06------
15. postcondition0.06------
16. postcondition0.06------
17. postcondition0.06------
18. postcondition------2.39
19. postcondition0.06------
20. postcondition0.05------
21. postcondition0.05------
22. postcondition0.05------
VC for interp_lexpr0.07------
VC for interp_lexpr_aux3.70------
VC for interp_lfrag_aux0.08------
VC for interp_process0.80------

Theory "interpreter.TerminatingTermInterpreter": fully verified in 278.04 s

ObligationsAlt-Ergo (1.30)CVC4 (1.5-prerelease)Z3 (4.5.0)
VC for interp_builtin0.04------
VC for interp_term---------
split_goal_wp
  1. postcondition1.66------
2. postcondition1.12------
3. exceptional postcondition1.74------
4. precondition2.54------
5. variant decrease0.09------
6. precondition1.94------
7. exceptional postcondition0.71------
8. exceptional postcondition0.14------
9. exceptional postcondition0.13------
10. exceptional postcondition0.13------
11. precondition2.44------
12. variant decrease0.09------
13. precondition1.95------
14. exceptional postcondition0.69------
15. exceptional postcondition0.12------
16. exceptional postcondition0.13------
17. exceptional postcondition0.11------
18. precondition2.49------
19. variant decrease0.10------
20. precondition1.82------
21. postcondition------1.86
22. exceptional postcondition------1.02
23. precondition2.69------
24. variant decrease0.08------
25. precondition1.86------
26. postcondition------1.31
27. exceptional postcondition------1.23
28. precondition1.75------
29. variant decrease0.05------
30. precondition3.31------
31. precondition------0.74
32. variant decrease0.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. precondition1.91------
42. variant decrease0.07------
43. precondition------0.44
44. precondition------1.24
45. variant decrease0.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 decrease0.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. precondition2.70------
61. variant decrease0.09------
62. precondition1.87------
63. variant decrease0.09------
64. precondition------3.20
65. postcondition0.08------
66. exceptional postcondition0.07------
67. exceptional postcondition0.05------
68. exceptional postcondition0.05------
69. precondition0.91------
70. variant decrease0.20------
71. precondition------0.46
72. precondition------0.90
73. variant decrease0.25------
74. precondition------1.54
75. precondition------2.58
76. variant decrease0.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. precondition2.76------
90. variant decrease0.06------
91. precondition1.69------
92. postcondition0.11------
93. exceptional postcondition0.14------
94. exceptional postcondition0.09------
95. postcondition0.15------
96. exceptional postcondition0.14------
97. postcondition0.09------
98. exceptional postcondition0.14------
99. precondition2.52------
100. variant decrease0.08------
101. precondition2.18------
102. variant decrease0.09------
103. precondition------2.50
104. postcondition0.06------
105. exceptional postcondition0.05------
106. exceptional postcondition0.06------
107. postcondition1.45------
108. postcondition2.15------
109. precondition2.70------
110. variant decrease0.10------
111. precondition2.60------
112. variant decrease0.16------
113. precondition------2.45
114. postcondition1.75------
115. exceptional postcondition1.87------
116. exceptional postcondition1.95------
117. exceptional postcondition1.82------
118. variant decrease0.14------
119. precondition------1.06
120. postcondition1.86------
121. exceptional postcondition2.03------
122. exceptional postcondition1.94------
123. exceptional postcondition1.85------
124. variant decrease0.16------
125. precondition------2.47
126. postcondition1.90------
127. exceptional postcondition2.04------
128. exceptional postcondition2.02------
129. exceptional postcondition1.95------
130. variant decrease0.14------
131. precondition------2.69
132. postcondition1.75------
133. exceptional postcondition1.89------
134. exceptional postcondition1.84------
135. exceptional postcondition1.84------
VC for interp_for---------
split_goal_wp
  1. postcondition0.15------
2. precondition0.29------
3. variant decrease0.07------
4. precondition0.43------
5. postcondition0.16------
6. exceptional postcondition0.15------
7. exceptional postcondition0.13------
8. exceptional postcondition0.13------
9. precondition0.17------
10. variant decrease0.07------
11. precondition0.45------
12. precondition---0.22---
13. variant decrease0.14------
14. precondition---0.20---
15. postcondition10.85------
16. exceptional postcondition---0.47---
17. exceptional postcondition12.33------
18. exceptional postcondition12.03------
19. exceptional postcondition17.01------
20. exceptional postcondition17.31------
21. exceptional postcondition16.76------
VC for interp_call---------
split_goal_wp
  1. postcondition0.43------
2. postcondition0.26------
3. exceptional postcondition0.24------
4. exceptional postcondition0.29------
5. postcondition0.25------
6. exceptional postcondition0.25------
7. exceptional postcondition0.34------
8. precondition0.70------
9. variant decrease0.07------
10. precondition2.03------
11. postcondition------0.06
12. exceptional postcondition------0.05
13. exceptional postcondition0.73------
14. postcondition------0.06
15. exceptional postcondition------0.05
16. exceptional postcondition0.75------
VC for interp_sexpr0.76------
VC for interp_sexpr_aux---------
split_goal_wp
  1. postcondition0.09------
2. precondition0.13------
3. variant decrease0.07------
4. precondition0.10------
5. variant decrease0.08------
6. precondition---0.27---
7. postcondition---0.23---
VC for interp_sfrag_aux---------
split_goal_wp
  1. postcondition0.11------
2. postcondition0.05------
3. postcondition0.26------
4. postcondition0.27------
5. precondition0.17------
6. variant decrease0.05------
7. precondition0.28------
8. postcondition1.02------
9. postcondition0.11------
10. postcondition1.08------
11. postcondition1.07------
VC for interp_lexpr0.78------
VC for interp_lexpr_aux---------
split_goal_wp
  1. postcondition0.07------
2. precondition0.10------
3. variant decrease0.06------
4. precondition0.10------
5. variant decrease0.08------
6. precondition---0.21---
7. postcondition------1.94
VC for interp_lfrag_aux1.17------
VC for interp_process---------
split_goal_wp
  1. precondition2.51------
2. variant decrease0.09------
3. precondition1.71------
4. postcondition2.40------
5. postcondition0.13------
6. postcondition1.64------
7. postcondition1.66------

Theory "interpreter.Interpreter": fully verified in 0.05 s

ObligationsAlt-Ergo (1.30)
VC for populate_penv0.05
VC for interp_program---
split_goal_wp