Why3 Proof Results for Project "mp2"

Theory "mp2.N": fully verified in 1105.26 s

ObligationsAlt-Ergo (1.30)CVC3 (2.4.1)CVC4 (1.4)Eprover (1.9.1-001)Z3 (4.4.1)
VC for map_eq_shift---------------
split_goal_wp
  1. postcondition0.03------------
VC for map_eq_shift_zero---------------
split_goal_wp
  1. assertion0.04------------
2. assertion0.03------------
3. variant decrease0.04------------
4. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition2.04------------
5. assertion0.03------------
6. postcondition---------------
inline_all
  1. postcondition1.54------------
limb_max_bound0.02------------
VC for prod_compat_strict_r---0.05---------
VC for value_sub---------------
split_goal_wp
  1. variant decrease0.03------------
VC for value_sub_frame---------------
split_goal_wp
  1. variant decrease0.03------------
2. precondition0.04------------
3. postcondition0.07------------
VC for value_sub_frame_shift---------------
split_goal_wp
  1. precondition0.02------------
2. precondition0.04------------
3. assertion0.03------------
inline_all
  1. assertion0.03------------
4. variant decrease0.02------------
5. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------0.170.02
6. assertion0.03------------
7. postcondition0.02------------
VC for value_sub_tail---------------
split_goal_wp
  1. variant decrease0.03------------
2. precondition0.04------------
3. postcondition0.07------------
VC for value_sub_concat---------------
split_goal_wp
  1. assertion0.02------------
2. variant decrease0.03------------
3. precondition0.03------------
4. postcondition---0.12---------
VC for value_sub_head---------------
split_goal_wp
  1. precondition0.03------------
2. postcondition0.06------------
VC for value_sub_update---------------
split_goal_wp
  1. assertion0.03------------
2. assertion0.04------------
3. precondition0.03------------
4. precondition0.03------------
5. precondition0.02------------
6. precondition0.02------------
7. postcondition---0.06---------
VC for value_zero---------------
split_goal_wp
  1. variant decrease0.04------------
2. precondition0.04------------
3. postcondition------------0.02
VC for value_sub_update_no_change---------------
split_goal_wp
  1. precondition0.03------------
2. postcondition0.03------------
VC for value_sub_shift_no_change---------------
split_goal_wp
  1. precondition0.03------------
2. postcondition0.02------------
VC for value_sub_lower_bound---------------
split_goal_wp
  1. precondition0.03------------
2. variant decrease0.03------------
3. postcondition------0.06------
VC for value_sub_upper_bound---------------
split_goal_wp
  1. precondition0.03------------
2. assertion---0.21---------
3. variant decrease0.04------------
4. precondition0.03------------
5. postcondition0.08------------
VC for value_sub_lower_bound_tight---------------
split_goal_wp
  1. assertion0.04------------
2. postcondition0.03------------
VC for value_sub_upper_bound_tight---------------
split_goal_wp
  1. precondition0.04------------
2. postcondition0.40------------
VC for copy---------------
split_goal_wp
  1. integer overflow------------0.04
2. integer overflow------------0.04
3. precondition0.04------------
4. precondition0.03------------
5. loop invariant init------------0.03
6. loop invariant init------------0.03
7. loop invariant init------------0.01
8. loop invariant init------------0.01
9. loop invariant init------------0.02
10. loop invariant init------------0.02
11. loop invariant init------------0.02
12. loop invariant init------------0.02
13. precondition---------------
split_goal_wp
  1. VC for copy------------0.05
2. VC for copy------------0.05
14. precondition---------------
split_goal_wp
  1. VC for copy------------0.03
2. VC for copy------------0.03
15. precondition0.03------------
16. precondition0.04------------
17. integer overflow------------0.06
18. loop variant decrease------------0.04
19. loop invariant preservation------------0.03
20. loop invariant preservation0.12------------
21. loop invariant preservation------------0.03
22. loop invariant preservation------------0.03
23. loop invariant preservation------------0.03
24. loop invariant preservation------------0.03
25. loop invariant preservation0.050.060.08------
26. loop invariant preservation0.03------------
27. postcondition------------0.05
VC for compare_same_size---------------
split_goal_wp
  1. loop invariant init0.03---------0.02
2. loop invariant init0.04---------0.01
3. integer overflow0.03---------0.03
4. assertion0.09------------
5. precondition0.05------------
6. integer overflow0.04---------0.02
7. integer overflow0.04---------0.04
8. assertion0.04------------
9. precondition0.03------------
10. precondition0.03------------
11. precondition0.06---------0.05
12. precondition0.05---------0.02
13. assertion0.06------------
14. precondition0.04---------0.03
15. precondition0.05---------0.02
16. precondition0.07---------0.02
17. assertion---0.10---------
18. assertion---------------
split_goal_wp
  1. VC for compare_same_size---0.12---------
2. VC for compare_same_size0.18------------
19. integer overflow0.10---------0.03
20. postcondition------------0.04
21. assertion0.05---------0.03
22. precondition0.05---------0.03
23. assertion---0.12---------
24. assertion---------------
split_goal_wp
  1. VC for compare_same_size---0.16---------
2. VC for compare_same_size0.33---------0.03
25. integer overflow0.10------------
26. integer overflow0.11---------0.04
27. postcondition------------0.03
28. loop variant decrease0.04---------0.03
29. loop invariant preservation0.03---------0.03
30. loop invariant preservation0.04------------
31. precondition0.03------------
32. integer overflow0.03---------0.04
33. postcondition------------0.04
VC for is_zero---------------
split_goal_wp
  1. integer overflow0.04---------0.02
2. loop invariant init0.03---------0.03
3. loop invariant init0.03---------0.03
4. integer overflow0.03---------0.02
5. integer overflow0.03---------0.03
6. integer overflow0.04---------0.03
7. assertion0.02------------
8. precondition0.04---------0.03
9. precondition0.03---------0.02
10. precondition0.03---------0.03
11. integer overflow0.05---------0.02
12. postcondition0.05---------0.02
13. postcondition0.14------------
14. assertion0.04---------0.02
15. loop variant decrease0.04---------0.02
16. loop invariant preservation0.03---------0.03
17. loop invariant preservation0.06------------
18. integer overflow0.03---------0.03
19. postcondition0.03---------0.02
20. postcondition0.02------------
VC for zero---------------
split_goal_wp
  1. integer overflow0.03------------
2. integer overflow0.03------------
3. loop invariant init0.03------------
4. loop invariant init0.06------------
5. precondition0.04------------
6. precondition0.04------------
7. integer overflow0.05------------
8. integer overflow0.04------------
9. loop variant decrease0.03------------
10. loop invariant preservation0.04------------
11. loop invariant preservation0.21------------
12. postcondition0.03------------
VC for add_limb---------------
split_goal_wp
  1. integer overflow0.04---------0.02
2. integer overflow0.04---------0.03
3. loop invariant init0.03---------0.03
4. loop invariant init0.03---------0.02
5. loop invariant init0.03------------
6. precondition0.03---------0.03
7. precondition0.03---------0.02
8. precondition0.05------------
9. assertion---------------
inline_all
  1. assertion---------------
split_goal_wp
  1. assertion2.14------------
2. assertion---0.10---------
10. integer overflow0.07---------0.02
11. integer overflow0.06---------0.03
12. precondition0.05---------0.03
13. precondition0.07---------0.03
14. assertion---------------
split_goal_wp
  1. VC for add_limb---1.05---5.58---
2. VC for add_limb0.10------------
3. VC for add_limb0.06------------
4. VC for add_limb0.09------------
5. VC for add_limb0.07------------
6. VC for add_limb0.07------------
7. VC for add_limb0.16------------
8. VC for add_limb------0.06------
15. loop variant decrease0.08---------0.03
16. loop invariant preservation0.08---------0.06
17. loop invariant preservation0.09---------0.03
18. loop invariant preservation---0.06---------
19. postcondition0.04------------
20. postcondition0.05---------0.03
21. loop invariant init0.03---------0.03
22. loop invariant init0.04---------0.03
23. loop invariant init0.12------------
24. precondition0.03---------0.04
25. precondition0.04------------
26. assertion---------------
split_goal_wp
  1. assertion0.07------------
2. assertion---------------
inline_all
  1. assertion---------0.05---
27. integer overflow0.06---------0.03
28. integer overflow0.04---------0.03
29. precondition0.04---------0.03
30. precondition0.08---------0.04
31. loop variant decrease0.04---------0.03
32. loop invariant preservation0.05---------0.02
33. loop invariant preservation0.05---------0.04
34. loop invariant preservation0.07------------
35. postcondition0.04------------
36. postcondition0.04---------0.02
VC for add_limbs---------------
split_goal_wp
  1. integer overflow0.03---------0.03
2. integer overflow0.04---------0.04
3. loop invariant init0.03---------0.02
4. loop invariant init0.11------------
5. loop invariant init0.04---------0.02
6. precondition0.04---------0.03
7. precondition0.05---------0.03
8. precondition0.05---------0.02
9. precondition0.05------------
10. assertion---------------
split_goal_wp
  1. assertion---------4.84---
11. integer overflow0.04---------0.02
12. integer overflow0.07---------0.03
13. precondition0.08---------0.03
14. precondition0.09---------0.04
15. precondition0.05---------0.04
16. assertion---------------
split_goal_wp
  1. VC for add_limbs2.04------------
2. VC for add_limbs0.20------------
3. VC for add_limbs0.11------------
4. VC for add_limbs0.11------------
5. VC for add_limbs0.10------------
6. VC for add_limbs0.11------------
7. VC for add_limbs0.10------------
8. VC for add_limbs0.27------------
9. VC for add_limbs0.11------------
10. VC for add_limbs0.27------------
11. VC for add_limbs------0.10------
17. loop variant decrease0.10---------0.03
18. loop invariant preservation0.10---------0.06
19. loop invariant preservation0.16---------0.01
20. loop invariant preservation0.12---------0.04
21. postcondition0.03---------0.03
22. postcondition0.03------------
VC for add---------------
split_goal_wp
  1. integer overflow------------0.03
2. integer overflow------------0.04
3. loop invariant init------------0.02
4. loop invariant init0.03------------
5. loop invariant init------------0.03
6. precondition0.04------------
7. precondition0.04------------
8. precondition------------0.02
9. precondition0.04------------
10. assertion---------------
split_goal_wp
  1. assertion---------4.35---
11. integer overflow------------0.03
12. integer overflow------------0.02
13. precondition------------0.03
14. precondition------------0.03
15. precondition------------0.03
16. assertion---------------
split_goal_wp
  1. VC for add1.36------------
2. VC for add0.24------------
3. VC for add0.12------------
4. VC for add0.12------------
5. VC for add0.11------------
6. VC for add0.11------------
7. VC for add0.12------------
8. VC for add0.29------------
9. VC for add0.10------------
10. VC for add0.29------------
11. VC for add------0.10------
17. loop variant decrease------------0.03
18. loop invariant preservation------------0.06
19. loop invariant preservation------------0.01
20. loop invariant preservation------------0.04
21. loop invariant init------------0.03
22. loop invariant init0.13------------
23. loop invariant init------------0.04
24. integer overflow------------0.03
25. assertion------------0.03
26. loop invariant init------------0.02
27. loop invariant init------------0.00
28. loop invariant init0.04------------
29. assertion0.04------------
30. precondition0.07------------
31. precondition0.08------------
32. integer overflow------------0.02
33. integer overflow------------0.06
34. precondition0.05------------
35. precondition0.05------------
36. assertion---------------
split_goal_wp
  1. VC for add0.05------------
2. VC for add0.08------------
3. VC for add0.11------------
4. VC for add0.07------------
5. VC for add---------0.74---
6. VC for add0.06------------
37. loop variant decrease------------0.03
38. loop invariant preservation0.07------------
39. loop invariant preservation------------0.02
40. loop invariant preservation0.07------------
41. postcondition0.04------------
42. postcondition------------0.02
43. precondition0.06------------
44. precondition------------0.02
45. precondition0.05------------
46. assertion---------------
split_goal_wp
  1. assertion0.15------------
47. integer overflow------------0.02
48. integer overflow------------0.10
49. precondition------------0.03
50. precondition------------0.02
51. assertion---------------
split_goal_wp
  1. VC for add---------5.77---
2. VC for add0.13------------
3. VC for add0.15------------
4. VC for add0.07------------
5. VC for add------0.07------
6. VC for add0.04------------
7. VC for add0.16------------
8. VC for add------0.06------
52. loop variant decrease------------0.03
53. loop invariant preservation------------0.04
54. loop invariant preservation------------0.01
55. loop invariant preservation------------0.03
56. assertion------------0.03
57. loop invariant init------------0.02
58. loop invariant init------------0.01
59. loop invariant init0.04------------
60. assertion0.05------------
61. precondition------------0.03
62. precondition0.07------------
63. integer overflow------------0.03
64. integer overflow------------0.03
65. precondition0.06------------
66. precondition0.07------------
67. assertion---------------
split_goal_wp
  1. VC for add0.09------------
2. VC for add0.08------------
3. VC for add0.10------------
4. VC for add0.10------------
5. VC for add---------0.76---
6. VC for add0.07------------
68. loop variant decrease------------0.03
69. loop invariant preservation0.07------------
70. loop invariant preservation------------0.03
71. loop invariant preservation0.07------------
72. postcondition0.05------------
73. postcondition------------0.02
VC for add_in_place---------------
split_goal_wp
  1. integer overflow0.02------------
2. integer overflow0.03------------
3. loop invariant init0.03------------
4. loop invariant init0.07------------
5. loop invariant init0.02------------
6. loop invariant init0.04------------
7. loop invariant init0.02------------
8. precondition0.04------------
9. assertion0.03------------
10. precondition0.04------------
11. precondition0.02------------
12. precondition------0.09------
13. assertion---------4.25---
14. integer overflow0.03------------
15. integer overflow0.06------------
16. precondition0.03------------
17. precondition0.04------------
18. precondition0.04------------
19. assertion---------------
split_goal_wp
  1. VC for add_in_place0.40------------
2. VC for add_in_place---------------
introduce_premises
  1. VC for add_in_place---------0.62---
3. VC for add_in_place0.22------------
4. VC for add_in_place0.15------------
5. VC for add_in_place---------------
introduce_premises
  1. VC for add_in_place---------0.02---
6. VC for add_in_place------0.07------
7. VC for add_in_place0.08------------
8. VC for add_in_place0.21------------
9. VC for add_in_place0.16------------
10. VC for add_in_place0.30------------
11. VC for add_in_place------0.05------
20. loop variant decrease0.15------------
21. loop invariant preservation------0.07------
22. loop invariant preservation0.22------------
23. loop invariant preservation0.16------------
24. loop invariant preservation0.21------------
25. loop invariant preservation0.27------------
26. loop invariant init0.02------------
27. loop invariant init0.02------------
28. loop invariant init0.03------------
29. loop invariant init0.03------------
30. loop invariant init0.04------------
31. assertion0.04------------
32. assertion---------------
split_goal_wp
  1. assertion0.04------------
2. assertion0.04------------
3. VC for add_in_place0.04------------
4. VC for add_in_place0.03------------
33. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition0.03------------
34. precondition------0.03------
35. precondition0.04------------
36. assertion---------------
split_goal_wp
  1. VC for add_in_place0.04------------
2. VC for add_in_place0.04------------
3. VC for add_in_place0.04------------
4. VC for add_in_place0.03------------
5. VC for add_in_place0.05------------
37. postcondition0.02------------
38. postcondition0.04------------
39. postcondition0.06------------
40. precondition0.05------------
41. assertion0.03------------
42. precondition0.04------------
43. precondition0.03------------
44. precondition0.08------------
45. precondition0.04------------
46. assertion---------------
split_goal_wp
  1. assertion---------3.49---
47. integer overflow0.04------------
48. integer overflow0.04------------
49. assertion0.04------------
50. precondition0.04------------
51. precondition0.04------------
52. assertion---------------
split_goal_wp
  1. VC for add_in_place0.30------------
2. VC for add_in_place---------------
introduce_premises
  1. VC for add_in_place---------0.64---
3. VC for add_in_place0.16------------
4. VC for add_in_place0.10------------
5. VC for add_in_place0.09------------
6. VC for add_in_place0.08------------
7. VC for add_in_place0.08------------
8. VC for add_in_place0.08------------
9. VC for add_in_place------0.06------
53. loop variant decrease------0.06------
54. loop invariant preservation------0.07------
55. loop invariant preservation------0.06------
56. loop invariant preservation------0.05------
57. loop invariant preservation---------0.51---
58. loop invariant preservation------0.20------
59. assertion0.04------------
60. postcondition0.04------------
61. postcondition0.03------------
62. postcondition0.03------------
VC for sub_limb---------------
split_goal_wp
  1. integer overflow------------0.03
2. integer overflow------------0.03
3. loop invariant init------------0.02
4. loop invariant init------------0.02
5. loop invariant init0.06------------
6. precondition------------0.02
7. precondition------------0.02
8. precondition0.06------------
9. assertion---------------
split_goal_wp
  1. assertion0.47------4.00---
2. assertion0.02------------
10. integer overflow------------0.02
11. integer overflow------------0.05
12. precondition------------0.03
13. precondition------------0.02
14. assertion---------------
split_goal_wp
  1. VC for sub_limb---------3.77---
2. VC for sub_limb0.10------------
3. VC for sub_limb0.07------------
4. VC for sub_limb0.07------------
5. VC for sub_limb0.06------------
6. VC for sub_limb0.06------------
7. VC for sub_limb0.17------------
8. VC for sub_limb------0.06------
15. loop variant decrease------------0.03
16. loop invariant preservation------------0.05
17. loop invariant preservation------------0.04
18. loop invariant preservation---0.08---------
19. postcondition0.03------------
20. postcondition------------0.02
21. loop invariant init------------0.02
22. loop invariant init------------0.04
23. loop invariant init0.11------------
24. precondition------------0.04
25. precondition0.06------------
26. assertion---------------
split_goal_wp
  1. assertion0.09------3.61---
2. assertion---------------
inline_all
  1. assertion0.040.07---------
27. integer overflow------------0.03
28. integer overflow------------0.03
29. precondition------------0.02
30. precondition------------0.03
31. loop variant decrease------------0.04
32. loop invariant preservation------------0.03
33. loop invariant preservation------------0.05
34. loop invariant preservation0.07------------
35. postcondition0.03------------
36. postcondition------------0.02
VC for sub_limbs---------------
split_goal_wp
  1. integer overflow------------0.03
2. integer overflow------------0.03
3. loop invariant init------------0.04
4. loop invariant init0.09------------
5. loop invariant init------------0.02
6. precondition------------0.04
7. precondition------------0.03
8. precondition------------0.03
9. precondition0.08------------
10. assertion---------------
split_goal_wp
  1. assertion---------3.95---
11. integer overflow------------0.03
12. integer overflow------------0.03
13. precondition------------0.04
14. precondition------------0.03
15. precondition------------0.03
16. assertion---------------
split_goal_wp
  1. VC for sub_limbs1.52------------
2. VC for sub_limbs0.17------------
3. VC for sub_limbs0.10------------
4. VC for sub_limbs0.10------------
5. VC for sub_limbs0.10------------
6. VC for sub_limbs0.10------------
7. VC for sub_limbs0.11------------
8. VC for sub_limbs0.10------------
9. VC for sub_limbs0.30------------
10. VC for sub_limbs---3.72---------
11. VC for sub_limbs------0.06------
17. loop variant decrease------------0.04
18. loop invariant preservation------------0.06
19. loop invariant preservation------------0.01
20. loop invariant preservation------------0.04
21. postcondition------------0.02
22. postcondition0.03------------
VC for sub---------------
split_goal_wp
  1. integer overflow------------0.03
2. integer overflow------------0.03
3. integer overflow------------0.02
4. loop invariant init------------0.02
5. loop invariant init0.04------------
6. loop invariant init------------0.04
7. precondition------------0.03
8. precondition------------0.03
9. precondition------------0.03
10. precondition0.09------------
11. assertion---4.21---3.84---
12. integer overflow------------0.03
13. precondition------------0.02
14. precondition------------0.02
15. precondition------------0.02
16. assertion---------------
split_goal_wp
  1. VC for sub1.52------------
2. VC for sub0.22------------
3. VC for sub0.17------------
4. VC for sub0.08------------
5. VC for sub0.11------------
6. VC for sub0.10------------
7. VC for sub0.21------------
8. VC for sub0.31------------
9. VC for sub---------0.08---
10. VC for sub------0.07------
17. loop variant decrease------------0.03
18. loop invariant preservation------------0.03
19. loop invariant preservation------------0.01
20. loop invariant preservation------------0.04
21. loop invariant init------------0.02
22. loop invariant init0.02------------
23. loop invariant init------------0.02
24. integer overflow0.04------------
25. assertion0.03------------
26. loop invariant init0.04------------
27. loop invariant init0.06------------
28. loop invariant init0.05------------
29. assertion0.04------------
30. precondition0.04------------
31. precondition0.04------------
32. integer overflow0.06------------
33. integer overflow0.05------------
34. precondition------------0.02
35. precondition------------0.02
36. assertion---------------
split_goal_wp
  1. VC for sub0.06------------
2. VC for sub0.11------------
3. VC for sub---------6.52---
4. VC for sub0.06------------
5. VC for sub---------2.43---
6. VC for sub0.09------------
37. loop variant decrease0.07------------
38. loop invariant preservation0.07------------
39. loop invariant preservation0.04------------
40. loop invariant preservation------------0.01
41. postcondition0.03------------
42. postcondition0.05------------
43. precondition------------0.02
44. precondition------------0.02
45. precondition0.07------------
46. assertion---------------
split_goal_wp
  1. assertion0.22------------
47. integer overflow------------0.08
48. precondition0.04------------
49. precondition0.05------------
50. assertion---------------
split_goal_wp
  1. VC for sub---------1.90---
2. VC for sub0.09------------
3. VC for sub0.06------------
4. VC for sub0.05------------
5. VC for sub0.06------------
6. VC for sub0.04------------
7. VC for sub0.10------------
8. VC for sub------0.06------
51. loop variant decrease------------0.04
52. loop invariant preservation0.06------------
53. loop invariant preservation0.05------------
54. loop invariant preservation------------0.06
55. assertion0.07------------
56. loop invariant init0.05------------
57. loop invariant init0.03------------
58. loop invariant init0.03------------
59. assertion0.04------------
60. precondition0.06------------
61. precondition0.06------------
62. integer overflow0.06------------
63. integer overflow0.06------------
64. precondition0.05------------
65. precondition0.06------------
66. assertion---------------
split_goal_wp
  1. VC for sub0.07------------
2. VC for sub0.07------------
3. VC for sub0.15------------
4. VC for sub0.10------------
5. VC for sub---------2.23---
6. VC for sub0.07------------
67. loop variant decrease0.05------------
68. loop invariant preservation0.06------------
69. loop invariant preservation0.05------------
70. loop invariant preservation0.06------------
71. postcondition0.03------------
72. postcondition0.04---------0.02
VC for sub_in_place---------------
split_goal_wp
  1. integer overflow0.02------------
2. integer overflow0.03------------
3. integer overflow0.02------------
4. loop invariant init0.02------------
5. loop invariant init0.07------------
6. loop invariant init0.02------------
7. loop invariant init0.04------------
8. loop invariant init0.02------------
9. precondition0.05------------
10. assertion0.04------------
11. precondition0.04------------
12. precondition0.03------------
13. precondition0.04------------
14. assertion---------3.66---
15. integer overflow0.03------------
16. precondition0.03------------
17. precondition0.04------------
18. precondition0.08------------
19. assertion---------------
split_goal_wp
  1. VC for sub_in_place---------3.46---
2. VC for sub_in_place0.20------------
3. VC for sub_in_place0.13------------
4. VC for sub_in_place0.15------------
5. VC for sub_in_place0.13------------
6. VC for sub_in_place0.12------------
7. VC for sub_in_place0.15------------
8. VC for sub_in_place0.38------------
9. VC for sub_in_place0.44------------
10. VC for sub_in_place------0.07------
20. loop variant decrease0.13------------
21. loop invariant preservation0.14------------
22. loop invariant preservation0.14------------
23. loop invariant preservation0.14------------
24. loop invariant preservation0.20------------
25. loop invariant preservation0.26------------
26. loop invariant init0.02------------
27. loop invariant init0.02------------
28. loop invariant init0.02------------
29. loop invariant init0.03------------
30. loop invariant init0.05------------
31. assertion0.03------------
32. assertion---------------
split_goal_wp
  1. assertion0.04------------
2. assertion0.03------------
3. VC for sub_in_place0.05------------
4. VC for sub_in_place0.04------------
33. precondition0.04------------
34. precondition0.03------------
35. precondition0.03------------
36. assertion---------------
split_goal_wp
  1. VC for sub_in_place0.05------------
2. VC for sub_in_place0.04------------
3. VC for sub_in_place0.05------------
4. VC for sub_in_place0.04------------
5. VC for sub_in_place0.04------------
37. postcondition0.04------------
38. postcondition0.04------------
39. postcondition0.06------------
40. precondition0.04------------
41. assertion0.05------------
42. precondition0.03------------
43. precondition0.03------------
44. precondition0.03------------
45. precondition0.06------------
46. assertion0.28------------
47. integer overflow0.04------------
48. assertion0.04------------
49. precondition0.04------------
50. precondition0.04------------
51. assertion---------------
split_goal_wp
  1. VC for sub_in_place---1.46---------
2. VC for sub_in_place0.12------------
3. VC for sub_in_place0.06------------
4. VC for sub_in_place0.06------------
5. VC for sub_in_place0.06------------
6. VC for sub_in_place0.06------------
7. VC for sub_in_place0.24------------
8. VC for sub_in_place------0.06------
52. loop variant decrease------0.12------
53. loop invariant preservation------0.07------
54. loop invariant preservation------0.06------
55. loop invariant preservation------0.06------
56. loop invariant preservation---------0.51---
57. loop invariant preservation------0.23------
58. assertion0.04------------
59. postcondition0.03------------
60. postcondition0.04------------
61. postcondition0.04------------
VC for mul_limb---------------
split_goal_wp
  1. integer overflow------------0.03
2. integer overflow------------0.04
3. loop invariant init------------0.02
4. loop invariant init0.13------------
5. precondition0.05------------
6. precondition------------0.03
7. precondition------------0.01
8. precondition------------0.04
9. precondition---------------
split_goal_wp
  1. VC for mul_limb0.04------------
2. VC for mul_limb---------0.45---
10. assertion0.04------------
11. assertion---------------
split_goal_wp
  1. VC for mul_limb------------0.04
2. VC for mul_limb------------0.03
3. VC for mul_limb------------0.04
4. VC for mul_limb------------0.05
5. VC for mul_limb------------0.01
6. VC for mul_limb------------0.02
7. VC for mul_limb------------0.03
8. VC for mul_limb------------0.03
9. VC for mul_limb------------0.04
10. VC for mul_limb------------0.03
12. integer overflow------------0.05
13. integer overflow------------0.03
14. integer overflow------------0.04
15. precondition------------0.03
16. precondition------------0.03
17. assertion---------------
split_goal_wp
  1. VC for mul_limb---------------
inline_all
  1. VC for mul_limb---------------
2. VC for mul_limb0.26------------
3. VC for mul_limb0.19------------
4. VC for mul_limb0.20------------
5. VC for mul_limb0.20------------
6. VC for mul_limb0.20------------
7. VC for mul_limb0.18------------
8. VC for mul_limb0.20------------
9. VC for mul_limb0.19------------
10. VC for mul_limb0.19------------
11. VC for mul_limb0.36------------
12. VC for mul_limb------0.06------
18. loop variant decrease------------0.03
19. loop invariant preservation------------0.06
20. loop invariant preservation------------0.00
21. postcondition0.02------------
VC for addmul_limb---------------
split_goal_wp
  1. integer overflow------------0.02
2. integer overflow------------0.03
3. loop invariant init------------0.02
4. loop invariant init0.08------------
5. loop invariant init------------0.01
6. loop invariant init------------0.01
7. precondition0.04------------
8. precondition---------------
split_goal_wp
  1. VC for addmul_limb------------0.03
2. VC for addmul_limb------------0.03
9. assertion------------0.02
10. precondition------------0.03
11. precondition------------0.02
12. precondition------------0.03
13. precondition---------------
split_goal_wp
  1. VC for addmul_limb------------0.03
2. VC for addmul_limb------------0.04
14. assertion---------------
split_goal_wp
  1. assertion---0.09---------
2. assertion---------0.66---
3. VC for addmul_limb------------0.03
15. assertion---------------
split_goal_wp
  1. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------0.07---
16. assertion---------------
split_goal_wp
  1. VC for addmul_limb------------0.05
2. VC for addmul_limb------------0.05
3. VC for addmul_limb------------0.05
4. VC for addmul_limb------------0.06
5. VC for addmul_limb------------0.01
6. VC for addmul_limb------------0.02
7. VC for addmul_limb------------0.03
8. VC for addmul_limb------------0.03
17. assertion------------0.03
18. assertion------------0.09
19. assertion------------0.03
20. integer overflow------------0.09
21. integer overflow------------0.03
22. integer overflow------------0.04
23. assertion---------------
split_goal_wp
  1. VC for addmul_limb---------------
inline_all
  1. VC for addmul_limb---0.08---------
2. VC for addmul_limb---------0.08---
3. VC for addmul_limb---------0.02---
4. VC for addmul_limb---0.07---------
5. VC for addmul_limb------------0.01
6. VC for addmul_limb------------0.01
7. VC for addmul_limb---------0.03---
8. VC for addmul_limb------------0.01
9. VC for addmul_limb---------0.04---
10. VC for addmul_limb---------------
inline_all
  1. VC for addmul_limb---0.12---------
11. VC for addmul_limb------------0.01
12. VC for addmul_limb------------0.02
13. VC for addmul_limb------------0.01
14. VC for addmul_limb------------0.01
15. VC for addmul_limb---1.22---------
16. VC for addmul_limb------0.08------
24. loop variant decrease------------0.03
25. loop invariant preservation------------0.04
26. loop invariant preservation------------0.00
27. loop invariant preservation---------4.67---
28. loop invariant preservation------0.19------
29. postcondition0.03------------
30. postcondition------------0.02
VC for mul_limbs---------------
split_goal_wp
  1. precondition0.03------------
2. integer overflow------------0.02
3. integer overflow------------0.04
4. integer overflow------------0.03
5. precondition0.04------------
6. integer overflow0.02------------
7. loop invariant init------------0.02
8. loop invariant init0.09------------
9. loop invariant init0.02------------
10. loop invariant init------------0.02
11. loop invariant init0.02------------
12. loop invariant init------------0.04
13. precondition------------0.03
14. assertion---------------
split_goal_wp
  1. assertion------0.06------
15. precondition0.03------------
16. precondition------------0.03
17. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for mul_limbs------------0.02
2. VC for mul_limbs------------0.03
3. VC for mul_limbs------------0.12
4. VC for mul_limbs------------0.14
18. assertion---------------
split_goal_wp
  1. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion0.04------------
19. assertion---------------
split_goal_wp
  1. VC for mul_limbs0.04------------
2. VC for mul_limbs0.06------------
3. VC for mul_limbs0.05------------
4. VC for mul_limbs0.11------------
5. VC for mul_limbs0.08------------
20. precondition------------0.03
21. precondition------------0.04
22. precondition------------0.04
23. precondition---------------
split_goal_wp
  1. VC for mul_limbs------------0.03
2. VC for mul_limbs------------0.03
24. integer overflow------------0.03
25. assertion---------------
split_goal_wp
  1. VC for mul_limbs---------0.42---
2. VC for mul_limbs---------4.23---
26. precondition------------0.03
27. precondition------------0.03
28. precondition------------0.03
29. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------0.96---
30. assertion---------------
split_goal_wp
  1. VC for mul_limbs---------------
introduce_premises
  1. VC for mul_limbs---------------
inline_goal
  1. VC for mul_limbs1.98------------
2. VC for mul_limbs0.16------------
3. VC for mul_limbs0.28------------
4. VC for mul_limbs4.02------------
5. VC for mul_limbs---1.34---------
6. VC for mul_limbs---1.28---------
7. VC for mul_limbs---------0.02---
8. VC for mul_limbs---1.08---------
9. VC for mul_limbs------0.04---0.01
10. VC for mul_limbs---------0.03---
11. VC for mul_limbs------0.04---0.01
12. VC for mul_limbs---------0.03---
13. VC for mul_limbs------0.04---0.01
14. VC for mul_limbs------0.080.020.02
15. VC for mul_limbs---------0.03---
16. VC for mul_limbs------0.100.040.01
17. VC for mul_limbs------0.04---0.01
18. VC for mul_limbs------0.04---0.01
19. VC for mul_limbs---------0.03---
20. VC for mul_limbs------0.070.030.04
21. VC for mul_limbs------0.04---0.02
22. VC for mul_limbs---------------
introduce_premises
  1. VC for mul_limbs---------0.08---
23. VC for mul_limbs------0.110.03---
31. precondition------------0.05
32. loop variant decrease------------0.03
33. loop invariant preservation------------0.03
34. loop invariant preservation------------0.03
35. loop invariant preservation------0.13------
36. loop invariant preservation------------0.03
37. loop invariant preservation------------0.04
38. loop invariant preservation------------0.04
39. precondition------------0.04
40. precondition------------0.03
41. assertion---------------
split_goal_wp
  1. VC for mul_limbs------------0.03
2. VC for mul_limbs------------0.03
42. assertion---------------
split_goal_wp
  1. VC for mul_limbs------------0.03
2. VC for mul_limbs------------0.02
43. precondition------------0.02
44. precondition------------0.01
45. assertion---------------
split_goal_wp
  1. VC for mul_limbs------------0.02
2. VC for mul_limbs0.04------------
3. VC for mul_limbs0.06------------
4. VC for mul_limbs---0.08---------
5. VC for mul_limbs------------0.01
6. VC for mul_limbs---0.07---------
7. VC for mul_limbs------------0.02
46. postcondition0.10------------
VC for addmul_limbs---------------
split_goal_wp
  1. integer overflow------------0.02
2. integer overflow------------0.03
3. integer overflow------------0.02
4. precondition------------0.06
5. integer overflow0.03------------
6. variant decrease------------0.01
7. precondition------------0.02
8. assertion------------0.01
9. postcondition0.19------------
10. loop invariant init0.03------------
11. loop invariant init0.12------------
12. loop invariant init0.04------------
13. loop invariant init0.02------------
14. loop invariant init0.02------------
15. loop invariant init0.02------------
16. precondition0.05------------
17. assertion---------------
split_goal_wp
  1. assertion---0.09---------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------0.08---
18. precondition0.06------------
19. precondition0.05------------
20. precondition0.06------------
21. assertion0.04------------
22. assertion---------------
split_goal_wp
  1. VC for addmul_limbs0.04------------
2. VC for addmul_limbs0.05------------
3. VC for addmul_limbs0.08------------
4. VC for addmul_limbs0.10------------
5. VC for addmul_limbs0.08------------
23. precondition0.14------------
24. assertion---2.08---------
25. precondition0.05------------
26. precondition0.05------------
27. precondition0.06------------
28. precondition0.08------------
29. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------------
split_goal_wp
  1. assertion0.32------------
30. integer overflow0.08------------
31. assertion---------------
split_goal_wp
  1. VC for addmul_limbs---------------
introduce_premises
  1. VC for addmul_limbs---------------
inline_goal
  1. VC for addmul_limbs0.16------------
2. VC for addmul_limbs---------------
introduce_premises
  1. VC for addmul_limbs---------------
inline_goal
  1. VC for addmul_limbs---------0.09---
32. precondition0.09------------
33. precondition0.12------------
34. precondition0.13------------
35. precondition0.27------------
36. assertion0.58------------
37. assertion---------------
split_goal_wp
  1. VC for addmul_limbs0.58------------
2. VC for addmul_limbs------0.45------
3. VC for addmul_limbs---------3.77---
4. VC for addmul_limbs---------0.07---
5. VC for addmul_limbs---2.34---------
6. VC for addmul_limbs------0.110.12---
7. VC for addmul_limbs---3.11---------
8. VC for addmul_limbs---------------
introduce_premises
  1. VC for addmul_limbs---------0.03---
9. VC for addmul_limbs---------0.03---
10. VC for addmul_limbs---------0.03---
11. VC for addmul_limbs------0.04---0.01
12. VC for addmul_limbs---------0.03---
13. VC for addmul_limbs------------0.05
14. VC for addmul_limbs------------0.02
15. VC for addmul_limbs---------0.04---
16. VC for addmul_limbs---0.16---------
17. VC for addmul_limbs---------------
inline_all
  1. VC for addmul_limbs---0.12---------
18. VC for addmul_limbs---------0.02---
19. VC for addmul_limbs------------0.01
20. VC for addmul_limbs------0.04---0.01
21. VC for addmul_limbs------------0.01
22. VC for addmul_limbs---------0.03---
23. VC for addmul_limbs---------0.18---
24. VC for addmul_limbs------------0.04
25. VC for addmul_limbs------------0.02
26. VC for addmul_limbs------------0.02
27. VC for addmul_limbs---------------
introduce_premises
  1. VC for addmul_limbs---------0.10---
28. VC for addmul_limbs---------------
inline_all
  1. VC for addmul_limbs---0.10---------
29. VC for addmul_limbs------0.080.17---
38. precondition------0.13------
39. loop variant decrease0.54------------
40. loop invariant preservation0.48------------
41. loop invariant preservation0.46------------
42. loop invariant preservation0.42------------
43. loop invariant preservation0.50------------
44. loop invariant preservation0.46------------
45. loop invariant preservation------0.46------
46. postcondition0.04------------
VC for mul---------------
split_goal_wp
  1. precondition0.03------------
2. precondition0.04------------
3. precondition0.03------------
4. precondition0.03------------
5. precondition0.02------------
6. precondition0.03------------
7. precondition0.09------------
8. assertion---------------
split_goal_wp
  1. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------2.32---
9. integer overflow0.04------------
10. integer overflow0.04------------
11. precondition0.04------------
12. integer overflow0.04------------
13. loop invariant init0.04------------
14. loop invariant init0.03------------
15. loop invariant init0.04------------
16. loop invariant init0.04------------
17. loop invariant init0.03------------
18. precondition0.03------------
19. assertion0.07------------
20. precondition0.04------------
21. precondition0.04------------
22. precondition0.09------------
23. assertion---------------
split_goal_wp
  1. assertion0.04------------
24. assertion---------------
split_goal_wp
  1. VC for mul0.13------------
2. VC for mul0.14------------
3. VC for mul0.14------------
4. VC for mul0.12------------
5. VC for mul0.36------------
25. precondition0.16------------
26. precondition0.09------------
27. precondition0.50------------
28. integer overflow0.14------------
29. assertion---------3.26---
30. precondition0.14------------
31. precondition0.15------------
32. precondition0.19------------
33. assertion---------4.82---
34. assertion---------------
split_goal_wp
  1. VC for mul---------------
introduce_premises
  1. VC for mul---------------
inline_goal
  1. VC for mul------------2.05
2. VC for mul0.22------------
3. VC for mul0.32------------
4. VC for mul---0.48---------
5. VC for mul---1.07---------
6. VC for mul---4.92---------
7. VC for mul---------------
introduce_premises
  1. VC for mul---------0.04---
8. VC for mul------------0.01
9. VC for mul---------0.03---
10. VC for mul------------0.01
11. VC for mul------------0.01
12. VC for mul---------0.04---
13. VC for mul------------0.02
14. VC for mul------------0.01
15. VC for mul------------0.01
16. VC for mul---------------
inline_all
  1. VC for mul---------1.20---
17. VC for mul------0.080.05---
35. precondition------------0.07
36. loop variant decrease0.36------------
37. loop invariant preservation0.34------------
38. loop invariant preservation0.33------------
39. loop invariant preservation0.34------------
40. loop invariant preservation0.41------------
41. loop invariant preservation0.65------------
42. integer overflow0.10------------
43. precondition0.04------------
44. postcondition0.05------------
45. postcondition0.06------------
VC for pow2_64---------------
split_goal_wp
  1. assertion0.04------------
2. assertion0.03------------
3. assertion0.04------------
4. assertion0.03------------
5. assertion0.03------------
6. assertion0.04------------
7. postcondition0.03------------
VC for mod_mult0.03------------
VC for lsld_ext---------------
split_goal_wp
  1. integer overflow------------0.02
2. precondition0.02------------
3. assertion---------------
split_goal_wp
  1. VC for lsld_ext------------0.04
2. VC for lsld_ext------------0.05
4. assertion---------------
split_goal_wp
  1. VC for lsld_ext0.02------------
2. VC for lsld_ext0.03------------
3. VC for lsld_ext0.04------------
4. VC for lsld_ext0.05------------
5. assertion---------------
split_goal_wp
  1. VC for lsld_ext------0.04------
2. VC for lsld_ext---------0.27---
3. VC for lsld_ext------0.05------
4. VC for lsld_ext------0.06------
6. assertion---------------
split_goal_wp
  1. assertion------------0.02
7. precondition0.05------------
8. precondition0.05------------
9. assertion---------------
split_goal_wp
  1. VC for lsld_ext0.090.060.050.020.02
2. VC for lsld_ext0.09------------
3. VC for lsld_ext0.07------------
4. VC for lsld_ext0.09------------
5. VC for lsld_ext---------------
inline_all
  1. VC for lsld_ext---------0.03---
6. VC for lsld_ext---------0.03---
7. VC for lsld_ext0.08------------
10. assertion---------------
split_goal_wp
  1. VC for lsld_ext---0.11---------
2. VC for lsld_ext---0.08---------
3. VC for lsld_ext------------0.01
4. VC for lsld_ext------------0.01
5. VC for lsld_ext---0.07---------
6. VC for lsld_ext---0.07---------
7. VC for lsld_ext---0.08---------
8. VC for lsld_ext---0.09---------
9. VC for lsld_ext------------0.01
10. VC for lsld_ext------------0.01
11. VC for lsld_ext---0.06---------
11. assertion---------------
split_goal_wp
  1. VC for lsld_ext------------0.01
2. VC for lsld_ext------------0.06
3. VC for lsld_ext------------0.05
4. VC for lsld_ext------0.08------
5. VC for lsld_ext---0.09---------
6. VC for lsld_ext------------0.02
7. VC for lsld_ext------------0.01
8. VC for lsld_ext------------0.02
12. postcondition0.12------------
13. postcondition0.53------------
14. postcondition0.07------------
15. postcondition0.290.070.050.03---
VC for clz_ext---------------
split_goal_wp
  1. precondition------------0.02
2. assertion---------------
split_goal_wp
  1. VC for clz_ext------------0.04
2. VC for clz_ext0.04------------
3. VC for clz_ext0.03------------
4. VC for clz_ext------------0.03
5. VC for clz_ext---1.49---------
6. VC for clz_ext---0.30---------
7. VC for clz_ext------------0.04
8. VC for clz_ext0.03------------
9. VC for clz_ext---0.08---------
10. VC for clz_ext0.05------------
11. VC for clz_ext0.02------------
12. VC for clz_ext---0.10---------
13. VC for clz_ext0.02------------
3. postcondition------------0.03
4. postcondition------------0.02
5. postcondition------------0.03
6. postcondition------------0.01
VC for lshift---------------
split_goal_wp
  1. integer overflow0.03------------
2. integer overflow0.04------------
3. integer overflow0.04------------
4. integer overflow0.05------------
5. integer overflow0.04------------
6. precondition0.02------------
7. precondition0.03------------
8. precondition0.04------------
9. precondition0.07---------0.03
10. loop invariant init0.030.060.065.470.03
11. loop invariant init---------------
inline_all
  1. loop invariant init---0.07---------
12. loop invariant init0.04------------
13. loop invariant init0.04------------
14. loop invariant init------------0.02
15. loop invariant init0.03---------0.03
16. loop invariant init------------0.02
17. loop invariant init0.04---------0.03
18. loop invariant init------0.07------
19. precondition0.05------------
20. precondition0.10------------
21. precondition0.04------------
22. assertion---------------
split_goal_wp
  1. assertion------------0.04
23. integer overflow------------0.06
24. precondition------------0.03
25. precondition------------0.03
26. integer overflow------0.26---0.06
27. precondition------0.070.66---
28. precondition------------0.08
29. integer overflow------------0.04
30. precondition------------0.03
31. precondition------------0.03
32. assertion---------------
split_goal_wp
  1. VC for lshift---------0.07---
2. VC for lshift------0.13------
3. VC for lshift------0.15------
4. VC for lshift------0.04------
5. VC for lshift------------0.03
6. VC for lshift------------0.04
7. VC for lshift---------0.05---
8. VC for lshift---0.08---0.16---
9. VC for lshift---0.09---0.04---
10. VC for lshift------------0.01
11. VC for lshift------------0.02
12. VC for lshift------------0.01
13. VC for lshift------------0.03
14. VC for lshift---0.11---------
15. VC for lshift---0.10---------
16. VC for lshift------------0.01
17. VC for lshift---------0.55---
18. VC for lshift------------0.02
19. VC for lshift---------------
inline_all
  1. VC for lshift---0.11---------
20. VC for lshift---------0.14---
33. loop variant decrease------------0.03
34. loop invariant preservation------------0.04
35. loop invariant preservation---------------
inline_all
  1. loop invariant preservation---0.12---------
36. loop invariant preservation------0.21------
37. loop invariant preservation------0.06------
38. loop invariant preservation------------0.04
39. loop invariant preservation------------0.02
40. loop invariant preservation------------0.03
41. loop invariant preservation------------0.04
42. loop invariant preservation------------0.04
43. assertion0.09------------
44. precondition------------0.03
45. precondition------------0.02
46. precondition---------------
split_goal_wp
  1. VC for lshift------------0.05
2. VC for lshift------------0.05
47. precondition------------0.03
48. postcondition---0.97---------
VC for rshift---------------
split_goal_wp
  1. integer overflow------------0.04
2. integer overflow------------0.02
3. integer overflow------------0.02
4. integer overflow------------0.02
5. integer overflow------------0.02
6. precondition------------0.05
7. precondition0.04------------
8. precondition------0.12------
9. precondition------------0.03
10. loop invariant init------------0.03
11. loop invariant init---------------
inline_all
  1. loop invariant init---0.05---------
12. loop invariant init------------0.02
13. loop invariant init------------0.03
14. loop invariant init------------0.01
15. loop invariant init------------0.01
16. loop invariant init------------0.01
17. loop invariant init------------0.01
18. loop invariant init------------0.02
19. precondition------------0.04
20. precondition------------0.03
21. precondition------------0.04
22. assertion------------0.02
23. integer overflow------------0.04
24. precondition------0.05------
25. precondition------0.050.040.01
26. integer overflow------0.18---0.04
27. precondition------0.10------
28. assertion---------------
split_goal_wp
  1. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------1.12---
29. precondition------0.09------
30. integer overflow------------0.03
31. precondition------0.06---0.02
32. precondition------------0.02
33. assertion---------------
split_goal_wp
  1. VC for rshift---------0.06---
2. VC for rshift---------0.50---
3. VC for rshift---------0.020.03
4. VC for rshift---2.98---------
5. VC for rshift---------0.03---
6. VC for rshift---------0.190.01
7. VC for rshift------------0.01
8. VC for rshift---------0.03---
9. VC for rshift---------0.03---
10. VC for rshift---------0.10---
11. VC for rshift---------0.180.01
12. VC for rshift---------0.03---
13. VC for rshift---0.08---------
14. VC for rshift------------0.01
15. VC for rshift---------------
introduce_premises
  1. VC for rshift---------0.10---
16. VC for rshift---3.92---------
introduce_premises
  1. VC for rshift---------0.08---
17. VC for rshift---------0.03---
34. loop variant decrease------0.09---0.07
35. loop invariant preservation------0.08---0.06
36. loop invariant preservation------0.080.020.01
37. loop invariant preservation------0.15------
38. loop invariant preservation------0.09------
39. loop invariant preservation------0.140.440.05
40. loop invariant preservation------0.140.030.05
41. loop invariant preservation------0.130.460.03
42. loop invariant preservation------0.130.030.04
43. loop invariant preservation------0.080.020.05
44. assertion---------------
split_goal_wp
  1. assertion---------0.10---
45. precondition------0.042.600.02
46. assertion------0.06------
47. precondition------0.06---0.03
48. precondition------0.100.120.03
49. precondition------0.10------
50. assertion------0.29------
51. precondition------0.044.580.01
52. assertion---------------
split_goal_wp
  1. VC for rshift---------------
introduce_premises
  1. VC for rshift---------------
inline_goal
  1. VC for rshift---------0.06---
2. VC for rshift------0.314.06---
53. assertion---------------
split_goal_wp
  1. VC for rshift---------------
introduce_premises
  1. VC for rshift---------------
inline_goal
  1. VC for rshift---------4.72---
2. VC for rshift---------------
introduce_premises
  1. VC for rshift---------------
inline_goal
  1. VC for rshift---------0.08---
54. postcondition---------0.03---
VC for fact_div---------------
split_goal_wp
  1. assertion---------------
split_goal_wp
  1. VC for fact_div0.04------------
2. VC for fact_div0.03------------
3. VC for fact_div0.04------------
4. VC for fact_div0.03------------
5. VC for fact_div0.05------------
6. VC for fact_div0.05------------
7. VC for fact_div0.05------------
8. VC for fact_div0.05------------
9. VC for fact_div0.03------------
10. VC for fact_div0.04------------
11. VC for fact_div---0.06---------
2. postcondition---------0.17---
VC for invert_limb---------------
split_goal_wp
  1. integer overflow------------0.03
2. integer overflow------------0.03
3. integer overflow------------0.03
4. precondition------------0.03
5. precondition0.06------------
6. assertion---------------
split_goal_wp
  1. VC for invert_limb------------0.01
2. VC for invert_limb------------0.01
3. VC for invert_limb------------0.01
4. VC for invert_limb------------0.01
5. VC for invert_limb0.030.05---------
6. VC for invert_limb------------0.01
7. VC for invert_limb0.02------------
8. VC for invert_limb0.030.06---------
7. postcondition------------0.03
VC for div2by1_inv---------------
split_goal_wp
  1. integer overflow0.020.050.060.040.03
2. integer overflow0.020.060.050.040.03
3. assertion---1.33---------
4. precondition0.030.070.050.020.03
5. precondition0.030.050.040.020.03
6. assertion------0.03------
7. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.03
2. VC for div2by1_inv------------0.04
3. VC for div2by1_inv------------0.02
4. VC for div2by1_inv0.03------------
5. VC for div2by1_inv------------0.07
6. VC for div2by1_inv------------0.01
7. VC for div2by1_inv------------0.06
8. VC for div2by1_inv------------0.01
9. VC for div2by1_inv------------0.03
10. VC for div2by1_inv------------0.02
11. VC for div2by1_inv------------0.02
12. VC for div2by1_inv------------0.02
13. VC for div2by1_inv------------0.01
14. VC for div2by1_inv------------0.01
15. VC for div2by1_inv------------0.02
16. VC for div2by1_inv------------0.01
17. VC for div2by1_inv------------0.01
18. VC for div2by1_inv0.14------------
19. VC for div2by1_inv------------0.03
20. VC for div2by1_inv------------0.03
21. VC for div2by1_inv------------0.04
22. VC for div2by1_inv------------0.01
23. VC for div2by1_inv------------0.04
24. VC for div2by1_inv------------0.04
25. VC for div2by1_inv------------0.02
26. VC for div2by1_inv------------0.04
27. VC for div2by1_inv------------0.03
28. VC for div2by1_inv------0.09------
8. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------0.08------
2. VC for div2by1_inv------------0.03
3. VC for div2by1_inv------------0.01
9. assertion------------0.01
10. assertion---------------
split_goal_wp
  1. assertion------0.21------
11. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.01
2. VC for div2by1_inv------------0.02
3. VC for div2by1_inv------0.49------
4. VC for div2by1_inv------------0.01
5. VC for div2by1_inv------------0.01
6. VC for div2by1_inv------------0.04
7. VC for div2by1_inv0.06------------
8. VC for div2by1_inv------------0.01
9. VC for div2by1_inv------------0.01
10. VC for div2by1_inv------------0.01
11. VC for div2by1_inv------------0.01
12. VC for div2by1_inv------------0.02
13. VC for div2by1_inv------------0.02
14. VC for div2by1_inv------0.06------
12. assertion---0.09---------
13. precondition------------0.05
14. precondition------------0.06
15. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.01
2. VC for div2by1_inv------------0.04
3. VC for div2by1_inv------------0.02
4. VC for div2by1_inv------------0.08
5. VC for div2by1_inv------------0.07
6. VC for div2by1_inv---0.10---------
7. VC for div2by1_inv------------0.02
8. VC for div2by1_inv------------0.05
9. VC for div2by1_inv------------0.02
10. VC for div2by1_inv------------0.02
11. VC for div2by1_inv------------0.01
12. VC for div2by1_inv------------0.04
13. VC for div2by1_inv------------0.06
14. VC for div2by1_inv---------------
introduce_premises
  1. VC for div2by1_inv---------47.84---
15. VC for div2by1_inv------------0.01
16. VC for div2by1_inv------------0.03
17. VC for div2by1_inv------------0.01
18. VC for div2by1_inv------------0.02
19. VC for div2by1_inv------------0.02
20. VC for div2by1_inv------------0.04
21. VC for div2by1_inv------0.11------
22. VC for div2by1_inv------------0.02
23. VC for div2by1_inv------------0.02
24. VC for div2by1_inv------------0.03
25. VC for div2by1_inv------------0.08
26. VC for div2by1_inv------------0.03
27. VC for div2by1_inv---------------
introduce_premises
  1. VC for div2by1_inv---------45.97---
28. VC for div2by1_inv---------0.20---
29. VC for div2by1_inv------------0.03
30. VC for div2by1_inv------------0.01
31. VC for div2by1_inv------------0.03
32. VC for div2by1_inv------------0.01
33. VC for div2by1_inv------------0.02
34. VC for div2by1_inv------------0.02
35. VC for div2by1_inv------------0.01
36. VC for div2by1_inv------------0.01
37. VC for div2by1_inv------------0.07
38. VC for div2by1_inv1.21------3.69---
39. VC for div2by1_inv------------0.09
40. VC for div2by1_inv------------0.06
41. VC for div2by1_inv------------0.02
42. VC for div2by1_inv1.24------------
43. VC for div2by1_inv------------0.01
44. VC for div2by1_inv------------0.01
45. VC for div2by1_inv------------0.01
46. VC for div2by1_inv------------0.01
47. VC for div2by1_inv------------0.04
48. VC for div2by1_inv------------0.04
49. VC for div2by1_inv------------0.04
16. assertion---------------
split_goal_wp
  1. assertion------0.15------
17. assertion---------------
split_goal_wp
  1. assertion------------0.03
2. VC for div2by1_inv------0.10------
3. VC for div2by1_inv------------0.01
4. VC for div2by1_inv------------0.05
5. VC for div2by1_inv------------0.03
6. VC for div2by1_inv------------0.00
7. VC for div2by1_inv------------0.01
8. VC for div2by1_inv------------0.01
9. VC for div2by1_inv------0.32------
18. assertion------0.13------
19. assertion------------0.05
20. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.03
2. VC for div2by1_inv------0.20------
3. VC for div2by1_inv------0.85------
4. VC for div2by1_inv------0.11------
21. assertion------------0.04
22. assertion---0.23---------
23. assertion---------------
split_goal_wp
  1. assertion------------0.03
2. VC for div2by1_inv------0.13------
3. VC for div2by1_inv------------0.05
4. VC for div2by1_inv------------0.03
5. VC for div2by1_inv------------0.12
6. VC for div2by1_inv------------0.03
7. VC for div2by1_inv------------0.01
8. VC for div2by1_inv------0.11------
9. VC for div2by1_inv------0.16------
10. VC for div2by1_inv------0.06------
24. assertion---------------
split_goal_wp
  1. assertion------------0.03
2. assertion------------0.03
3. VC for div2by1_inv------------0.10
4. VC for div2by1_inv------0.07------
5. VC for div2by1_inv------------0.03
25. assertion------1.92------
26. assertion---------------
split_goal_wp
  1. assertion------------0.04
2. assertion------------0.02
3. VC for div2by1_inv------------0.01
4. VC for div2by1_inv------------0.01
5. VC for div2by1_inv------------0.04
6. VC for div2by1_inv------------0.01
7. VC for div2by1_inv------------0.06
8. VC for div2by1_inv------------0.04
9. VC for div2by1_inv------0.07------
27. assertion---------------
split_goal_wp
  1. assertion------------0.01
2. VC for div2by1_inv------------0.04
3. VC for div2by1_inv------------0.03
4. VC for div2by1_inv------------0.06
5. VC for div2by1_inv------------0.02
6. VC for div2by1_inv------------0.02
7. VC for div2by1_inv------------0.01
8. VC for div2by1_inv------------0.03
9. VC for div2by1_inv------------0.05
10. VC for div2by1_inv------------0.08
11. VC for div2by1_inv------------0.03
12. VC for div2by1_inv------0.08------
13. VC for div2by1_inv------------0.11
14. VC for div2by1_inv------------0.09
15. VC for div2by1_inv------0.59------
16. VC for div2by1_inv------0.20------
17. VC for div2by1_inv------------0.01
18. VC for div2by1_inv---------0.03---
19. VC for div2by1_inv------------0.03
28. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.01
2. VC for div2by1_inv------------0.01
29. assertion---------------
split_goal_wp
  1. assertion------------0.01
2. VC for div2by1_inv------0.30------
3. VC for div2by1_inv---0.11---------
4. VC for div2by1_inv------------0.01
5. VC for div2by1_inv------0.07------
30. assertion------------0.03
31. assertion------------0.03
32. assertion------0.24------
33. integer overflow------0.18---0.09
34. integer overflow------------0.03
35. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.04
2. VC for div2by1_inv------------0.03
36. assertion---0.13---------
37. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.03
2. VC for div2by1_inv------------0.04
38. assertion------------0.01
39. postcondition------------0.01
40. postcondition------------0.03
41. assertion------------0.09
42. assertion---0.14---------
43. postcondition------------0.00
44. postcondition------------0.05
45. assertion------------0.03
46. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.05
2. VC for div2by1_inv------------0.03
47. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.03
2. VC for div2by1_inv---0.120.070.03---
48. assertion------------0.01
49. assertion---------------
split_goal_wp
  1. VC for div2by1_inv------------0.01
2. VC for div2by1_inv------------0.03
3. VC for div2by1_inv------------0.02
4. VC for div2by1_inv------------0.01
5. VC for div2by1_inv------------0.01
6. VC for div2by1_inv------------0.04
7. VC for div2by1_inv------------0.02
8. VC for div2by1_inv------------0.01
9. VC for div2by1_inv------------0.03
10. VC for div2by1_inv------------0.04
11. VC for div2by1_inv---0.15---------
12. VC for div2by1_inv------------0.04
50. integer overflow------------0.04
51. integer overflow------------0.05
52. assertion------------0.12
53. assertion---------------
split_goal_wp
  1. assertion---0.14---------
54. assertion------0.06------
55. assertion---------------
split_goal_wp
  1. assertion------------0.01
56. postcondition------------0.01
57. postcondition------------0.04
58. assertion---------------
split_goal_wp
  1. VC for div2by1_inv---------0.020.03
2. VC for div2by1_inv------------0.03
59. assertion---0.11---------
60. postcondition------------0.01
61. postcondition------------0.04
VC for divmod_1---------------
split_goal_wp
  1. integer overflow------------0.03
2. integer overflow------------0.03
3. integer overflow------------0.03
4. integer overflow------------0.03
5. integer overflow------------0.03
6. integer overflow------------0.03
7. precondition0.03------------
8. precondition0.04------------
9. precondition------------0.03
10. precondition------------0.02
11. precondition------------0.02
12. precondition0.04------------
13. assertion---------------
split_goal_wp
  1. assertion0.08------------
14. assertion0.06------------
15. precondition------------0.04
16. loop invariant init------------0.03
17. loop invariant init------------0.04
18. loop invariant init------------0.03
19. loop invariant init------------0.02
20. loop invariant init------------0.04
21. loop invariant init------------0.04
22. loop invariant init------------0.02
23. loop invariant init0.03---------0.04
24. loop invariant init0.06------------
25. loop invariant init0.04------------
26. loop invariant init------------0.42
27. assertion------------0.02
28. precondition------0.12------
29. precondition------------0.02
30. precondition------------0.03
31. precondition------------0.07
32. assertion---------------
split_goal_wp
  1. VC for divmod_1------------0.05
2. VC for divmod_1------0.20------
3. VC for divmod_1------------0.03
4. VC for divmod_1------------0.00
5. VC for divmod_1------------0.04
6. VC for divmod_1------0.19------
7. VC for divmod_1------------0.04
8. VC for divmod_1------------0.02
9. VC for divmod_1------0.07------
10. VC for divmod_1------------0.02
11. VC for divmod_1------------0.05
12. VC for divmod_1---0.21---------
13. VC for divmod_1------------0.03
14. VC for divmod_1------------0.03
15. VC for divmod_1------------0.01
16. VC for divmod_1------------0.04
17. VC for divmod_1------------0.02
18. VC for divmod_1------------0.06
19. VC for divmod_1------------0.02
20. VC for divmod_1------------0.03
33. assertion---------------
split_goal_wp
  1. VC for divmod_1------------0.02
2. VC for divmod_1------------0.05
3. VC for divmod_1------------0.03
34. integer overflow------------0.05
35. precondition------------0.02
36. precondition---------------
split_goal_wp
  1. precondition------0.08------
37. precondition------------0.02
38. precondition------------0.05
39. precondition------------0.07
40. assertion---------------
split_goal_wp
  1. VC for divmod_1------0.08------
2. VC for divmod_1---------0.03---
3. VC for divmod_1---------0.02---
4. VC for divmod_1------------0.05
5. VC for divmod_1------------0.01
6. VC for divmod_1---------0.04---
7. VC for divmod_1------------0.03
8. VC for divmod_1------------0.03
41. precondition------------0.06
42. assertion---------------
split_goal_wp
  1. VC for divmod_1------------0.03
2. VC for divmod_1------0.200.10---
3. VC for divmod_1------------0.05
4. VC for divmod_1------------0.03
5. VC for divmod_1------------0.05
6. VC for divmod_1------------0.04
7. VC for divmod_1------------0.02
8. VC for divmod_1---0.12---------
9. VC for divmod_1------------0.02
10. VC for divmod_1------------0.02
11. VC for divmod_1---0.15---------
12. VC for divmod_1------------0.03
13. VC for divmod_1------------0.03
43. precondition------------0.03
44. precondition------------0.03
45. precondition------0.12------
46. precondition------------0.07
47. precondition------------0.08
48. integer overflow------0.37------
49. precondition------------0.03
50. precondition------------0.03
51. assertion---------------
split_goal_wp
  1. VC for divmod_1---------0.38---
2. VC for divmod_1---0.89---------
3. VC for divmod_1---0.22---0.03---
4. VC for divmod_1---0.15---------
5. VC for divmod_1---0.13---------
6. VC for divmod_1---0.12---------
7. VC for divmod_1------------0.01
8. VC for divmod_1---------0.38---
9. VC for divmod_1------0.10------
10. VC for divmod_1------------0.01
11. VC for divmod_1------0.11------
12. VC for divmod_1------0.04------
13. VC for divmod_1---0.14------0.02
14. VC for divmod_1---0.14---------
15. VC for divmod_1---0.12---------
52. loop variant decrease------------0.04
53. loop invariant preservation------0.11------
54. loop invariant preservation------0.24------
55. loop invariant preservation------0.15------
56. loop invariant preservation------------0.03
57. loop invariant preservation------------0.04
58. loop invariant preservation------------0.03
59. loop invariant preservation------------0.03
60. loop invariant preservation------------0.04
61. loop invariant preservation------------0.01
62. loop invariant preservation------------0.06
63. loop invariant preservation------------0.03
64. precondition------------0.03
65. precondition------------0.03
66. precondition------------0.03
67. assertion---------------
split_goal_wp
  1. VC for divmod_1---------0.03---
2. VC for divmod_1---0.69---------
3. VC for divmod_1---------0.11---
4. VC for divmod_1------------0.01
5. VC for divmod_1------------0.01
6. VC for divmod_1---0.10---------
68. precondition------------0.05
69. precondition------------0.02
70. precondition---0.08------0.03
71. postcondition---0.60---------
72. postcondition---0.07---------
73. precondition0.05------------
74. loop invariant init0.04------------
75. loop invariant init0.04------------
76. loop invariant init0.05------------
77. loop invariant init0.04------------
78. loop invariant init0.04------------
79. loop invariant init0.03------------
80. loop invariant init0.03------------
81. loop invariant init0.05------------
82. loop invariant init0.05------------
83. assertion0.06------------
84. precondition0.06------------
85. precondition0.05------------
86. precondition0.03------------
87. precondition0.03------------
88. precondition------0.07------
89. precondition------0.09------
90. precondition------0.10------
91. precondition------0.10------
92. precondition------0.13------
93. integer overflow------0.20------
94. precondition------0.08------
95. precondition------0.08------
96. assertion---------------
split_goal_wp
  1. VC for divmod_1---------0.35---
2. VC for divmod_1---------0.02---
3. VC for divmod_1---------------
introduce_premises
  1. VC for divmod_1---------0.05---
4. VC for divmod_1------0.09------
5. VC for divmod_1---------0.40---
6. VC for divmod_1------0.04------
7. VC for divmod_1------0.08------
8. VC for divmod_1------0.04------
9. VC for divmod_1---------6.18---
10. VC for divmod_1------0.10------
97. loop variant decrease------0.10------
98. loop invariant preservation------0.08------
99. loop invariant preservation------0.13------
100. loop invariant preservation------0.08------
101. loop invariant preservation------0.15------
102. loop invariant preservation------0.14------
103. loop invariant preservation------0.14------
104. loop invariant preservation------0.18------
105. loop invariant preservation------0.08------
106. loop invariant preservation------0.08------
107. postcondition0.05------------
108. postcondition0.04---0.06------
VC for div3by2_inv---------------
split_goal_wp
  1. integer overflow0.03------------
2. integer overflow0.04------------
3. precondition0.03------------
4. precondition0.05------------
5. assertion0.04------------
6. assertion---------------
split_goal_wp
  1. VC for div3by2_inv0.03---0.05---0.04
2. VC for div3by2_inv------0.11---0.04
3. VC for div3by2_inv0.03---0.04---0.02
4. VC for div3by2_inv0.03---0.05---0.01
5. VC for div3by2_inv---------------
inline_all
  1. VC for div3by2_inv---0.08---------
6. VC for div3by2_inv0.04------------
7. VC for div3by2_inv------0.10------
8. VC for div3by2_inv0.05---0.02---0.01
9. VC for div3by2_inv0.06---0.07---0.03
10. VC for div3by2_inv0.05---0.07---0.02
11. VC for div3by2_inv------0.09---0.03
12. VC for div3by2_inv0.07---0.05---0.02
7. assertion------0.53------
8. precondition0.04------------
9. precondition---0.090.060.020.04
10. precondition---0.090.060.020.02
11. assertion---0.090.07------
12. precondition---0.090.060.020.04
13. precondition---0.090.090.020.05
14. assertion---0.090.07------
15. precondition------0.03------
16. assertion------3.41------
17. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------0.14------
2. VC for div3by2_inv------0.090.04---
3. VC for div3by2_inv---0.10---------
4. VC for div3by2_inv------------0.01
5. VC for div3by2_inv---0.080.080.01---
6. VC for div3by2_inv------0.150.36---
7. VC for div3by2_inv---0.100.080.02---
8. VC for div3by2_inv------0.04---0.01
9. VC for div3by2_inv------0.08---0.01
10. VC for div3by2_inv------0.04---0.02
11. VC for div3by2_inv------0.04---0.01
12. VC for div3by2_inv------0.04---0.01
13. VC for div3by2_inv------0.07------
14. VC for div3by2_inv------0.06------
15. VC for div3by2_inv------0.05---0.02
16. VC for div3by2_inv---------0.11---
17. VC for div3by2_inv------------0.01
18. VC for div3by2_inv------0.08------
18. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------0.09------
2. VC for div3by2_inv---0.11---------
3. VC for div3by2_inv------0.29---0.09
4. VC for div3by2_inv------0.04---0.01
5. VC for div3by2_inv------0.04---0.01
6. VC for div3by2_inv------0.16---0.08
7. VC for div3by2_inv------0.04---0.01
8. VC for div3by2_inv------0.08---0.01
9. VC for div3by2_inv------0.26---0.07
10. VC for div3by2_inv------0.28------
11. VC for div3by2_inv------0.08------
12. VC for div3by2_inv------------0.01
13. VC for div3by2_inv------0.06---0.07
14. VC for div3by2_inv------0.09---0.02
15. VC for div3by2_inv------0.04---0.01
16. VC for div3by2_inv---0.12---------
17. VC for div3by2_inv------0.05---0.01
18. VC for div3by2_inv------0.04---0.02
19. VC for div3by2_inv------0.06---0.02
20. VC for div3by2_inv------0.04---0.02
21. VC for div3by2_inv------0.04---0.02
22. VC for div3by2_inv---0.15---0.03---
23. VC for div3by2_inv------0.08---0.04
24. VC for div3by2_inv------0.41---0.13
25. VC for div3by2_inv------------0.08
26. VC for div3by2_inv------0.21---0.08
27. VC for div3by2_inv------0.21---0.07
28. VC for div3by2_inv---0.13---------
29. VC for div3by2_inv------0.09---0.03
30. VC for div3by2_inv------0.22---0.10
31. VC for div3by2_inv------0.10---0.05
32. VC for div3by2_inv---0.21---------
33. VC for div3by2_inv---0.110.05---0.05
34. VC for div3by2_inv------0.09---0.01
35. VC for div3by2_inv------0.04---0.01
36. VC for div3by2_inv------0.08---0.02
37. VC for div3by2_inv------0.24---0.11
38. VC for div3by2_inv------0.24---0.10
39. VC for div3by2_inv---------0.09---
40. VC for div3by2_inv------0.090.10---
41. VC for div3by2_inv------0.09---0.01
42. VC for div3by2_inv------0.09---0.05
43. VC for div3by2_inv------0.09---0.03
44. VC for div3by2_inv------0.04---0.01
45. VC for div3by2_inv------0.21------
46. VC for div3by2_inv------0.23---0.09
47. VC for div3by2_inv------0.21---0.06
48. VC for div3by2_inv------0.21---0.08
49. VC for div3by2_inv---------0.08---
50. VC for div3by2_inv---------0.62---
51. VC for div3by2_inv---------------
introduce_premises
  1. VC for div3by2_inv---------------
inline_goal
  1. VC for div3by2_inv---------0.02---
52. VC for div3by2_inv---------0.05---
53. VC for div3by2_inv---0.140.13---0.03
54. VC for div3by2_inv---------54.35---
55. VC for div3by2_inv---------4.76---
56. VC for div3by2_inv------------0.01
57. VC for div3by2_inv------0.40------
58. VC for div3by2_inv---------2.84---
59. VC for div3by2_inv------0.10------
60. VC for div3by2_inv------0.350.240.04
61. VC for div3by2_inv---------0.10---
62. VC for div3by2_inv---------2.74---
63. VC for div3by2_inv---------------
introduce_premises
  1. VC for div3by2_inv---------3.76---
64. VC for div3by2_inv------0.09---0.04
65. VC for div3by2_inv---------2.62---
66. VC for div3by2_inv------0.08---0.01
67. VC for div3by2_inv------0.10---0.02
68. VC for div3by2_inv------0.10---0.01
69. VC for div3by2_inv------0.33---0.10
70. VC for div3by2_inv------0.10---0.04
71. VC for div3by2_inv------0.04---0.01
72. VC for div3by2_inv------0.05---0.02
73. VC for div3by2_inv------0.04---0.01
74. VC for div3by2_inv------0.04---0.01
75. VC for div3by2_inv------------0.06
76. VC for div3by2_inv------0.40---0.12
77. VC for div3by2_inv---0.15---------
78. VC for div3by2_inv------------0.01
79. VC for div3by2_inv------------0.02
80. VC for div3by2_inv------0.04---0.01
81. VC for div3by2_inv------0.05---0.00
82. VC for div3by2_inv------0.04---0.01
83. VC for div3by2_inv------0.05---0.01
84. VC for div3by2_inv------0.05---0.02
85. VC for div3by2_inv------0.05---0.01
86. VC for div3by2_inv------0.04------
87. VC for div3by2_inv---------------
introduce_premises
  1. VC for div3by2_inv---------11.29---
88. VC for div3by2_inv------0.18---0.02
89. VC for div3by2_inv---0.120.040.100.01
90. VC for div3by2_inv---0.200.12---0.05
91. VC for div3by2_inv------------0.01
92. VC for div3by2_inv------------0.03
93. VC for div3by2_inv---------2.38---
94. VC for div3by2_inv------0.09------
95. VC for div3by2_inv---------------
inline_all
  1. VC for div3by2_inv---0.14---------
96. VC for div3by2_inv------0.07---0.02
97. VC for div3by2_inv------------0.07
98. VC for div3by2_inv------------0.03
99. VC for div3by2_inv------------0.01
100. VC for div3by2_inv------------0.01
101. VC for div3by2_inv------------0.01
102. VC for div3by2_inv------------0.01
103. VC for div3by2_inv------------0.02
104. VC for div3by2_inv------------0.01
105. VC for div3by2_inv------------0.01
106. VC for div3by2_inv------------0.00
107. VC for div3by2_inv------------0.02
108. VC for div3by2_inv------------0.01
109. VC for div3by2_inv------------0.01
110. VC for div3by2_inv------------0.02
111. VC for div3by2_inv------------0.01
112. VC for div3by2_inv------------0.01
113. VC for div3by2_inv------0.08------
114. VC for div3by2_inv------0.08------
115. VC for div3by2_inv------------0.01
116. VC for div3by2_inv------------0.01
117. VC for div3by2_inv------------0.02
118. VC for div3by2_inv---0.150.10------
119. VC for div3by2_inv------------0.01
120. VC for div3by2_inv------------0.01
121. VC for div3by2_inv------------0.01
122. VC for div3by2_inv------------0.00
123. VC for div3by2_inv------------0.02
124. VC for div3by2_inv------------0.04
125. VC for div3by2_inv------------0.08
126. VC for div3by2_inv---0.28---------
127. VC for div3by2_inv------------0.04
128. VC for div3by2_inv------------0.01
129. VC for div3by2_inv------------0.04
130. VC for div3by2_inv------------0.12
131. VC for div3by2_inv------------0.03
132. VC for div3by2_inv------------0.04
133. VC for div3by2_inv------------0.01
134. VC for div3by2_inv------------0.13
135. VC for div3by2_inv------0.12------
136. VC for div3by2_inv------------0.03
137. VC for div3by2_inv------------0.02
138. VC for div3by2_inv------------0.01
139. VC for div3by2_inv------------0.01
140. VC for div3by2_inv------------0.01
141. VC for div3by2_inv------0.09------
142. VC for div3by2_inv------------0.01
143. VC for div3by2_inv------------0.00
144. VC for div3by2_inv------------0.04
145. VC for div3by2_inv------0.07------
146. VC for div3by2_inv---0.19---------
147. VC for div3by2_inv---------0.04---
148. VC for div3by2_inv------------0.03
149. VC for div3by2_inv---------------
inline_all
  1. VC for div3by2_inv---0.78---------
150. VC for div3by2_inv------0.14---0.02
151. VC for div3by2_inv------------0.08
152. VC for div3by2_inv------------0.01
153. VC for div3by2_inv------------0.01
154. VC for div3by2_inv---------0.13---
155. VC for div3by2_inv------0.34------
156. VC for div3by2_inv------------0.13
157. VC for div3by2_inv------0.06---0.03
158. VC for div3by2_inv------------0.02
159. VC for div3by2_inv------------0.00
160. VC for div3by2_inv---------0.03---
161. VC for div3by2_inv------------0.13
162. VC for div3by2_inv------------0.01
163. VC for div3by2_inv------0.16------
164. VC for div3by2_inv------------0.02
165. VC for div3by2_inv------------0.09
166. VC for div3by2_inv------------0.12
167. VC for div3by2_inv------------0.02
168. VC for div3by2_inv------------0.02
169. VC for div3by2_inv------------0.02
170. VC for div3by2_inv------------0.01
171. VC for div3by2_inv------0.10------
172. VC for div3by2_inv------------0.04
173. VC for div3by2_inv------------0.03
174. VC for div3by2_inv------0.08---0.04
175. VC for div3by2_inv------0.080.03---
19. assertion------0.44------
20. assertion---------------
split_goal_wp
  1. assertion------------0.06
2. VC for div3by2_inv------------0.04
3. VC for div3by2_inv------------0.02
4. VC for div3by2_inv------0.08------
5. VC for div3by2_inv------------0.08
6. VC for div3by2_inv------------0.03
7. VC for div3by2_inv------------0.01
8. VC for div3by2_inv------------0.01
9. VC for div3by2_inv------------0.01
10. VC for div3by2_inv------0.98------
21. assertion---------------
split_goal_wp
  1. assertion------0.20---0.07
2. VC for div3by2_inv------------0.03
3. VC for div3by2_inv------------0.02
4. VC for div3by2_inv------------0.03
5. VC for div3by2_inv------0.12---0.05
6. VC for div3by2_inv------0.03---0.01
7. VC for div3by2_inv------0.08---0.05
8. VC for div3by2_inv------0.34---0.11
9. VC for div3by2_inv------0.09---0.02
10. VC for div3by2_inv------0.03---0.02
11. VC for div3by2_inv------0.09---0.03
12. VC for div3by2_inv------0.04---0.01
13. VC for div3by2_inv------0.09---0.02
14. VC for div3by2_inv------0.11---0.05
22. assertion------0.28------
23. assertion---------------
split_goal_wp
  1. assertion------0.720.59---
2. VC for div3by2_inv---------0.09---
24. assertion---------------
split_goal_wp
  1. assertion------------0.01
2. VC for div3by2_inv------------0.04
3. VC for div3by2_inv---------0.04---
4. VC for div3by2_inv------------0.01
5. VC for div3by2_inv------------0.01
6. VC for div3by2_inv------------0.08
7. VC for div3by2_inv------------0.03
25. assertion------4.12------
26. precondition---0.120.080.020.07
27. precondition---0.120.080.020.03
28. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------0.11------
2. VC for div3by2_inv---------0.03---
3. VC for div3by2_inv------------0.01
4. VC for div3by2_inv------2.98------
29. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------------0.04
2. VC for div3by2_inv------------0.04
3. VC for div3by2_inv------0.58------
4. VC for div3by2_inv------------0.05
5. VC for div3by2_inv------------0.02
6. VC for div3by2_inv------------0.13
7. VC for div3by2_inv------------0.03
8. VC for div3by2_inv------------0.05
9. VC for div3by2_inv------------0.15
10. VC for div3by2_inv------------0.02
11. VC for div3by2_inv------------0.11
12. VC for div3by2_inv------------0.05
13. VC for div3by2_inv---------0.74---
14. VC for div3by2_inv------------0.06
15. VC for div3by2_inv------------0.05
16. VC for div3by2_inv------------0.16
17. VC for div3by2_inv------------0.04
18. VC for div3by2_inv------------0.03
19. VC for div3by2_inv------------0.12
20. VC for div3by2_inv------------0.03
21. VC for div3by2_inv------0.55------
22. VC for div3by2_inv------------0.01
23. VC for div3by2_inv------0.11------
30. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------0.05------
2. VC for div3by2_inv------0.10------
3. VC for div3by2_inv------0.15------
4. VC for div3by2_inv---------0.03---
5. VC for div3by2_inv------0.04------
6. VC for div3by2_inv------0.06------
7. VC for div3by2_inv---------0.03---
31. assertion---------------
split_goal_wp
  1. assertion------0.16------
32. precondition---0.120.180.020.08
33. precondition---0.120.190.020.03
34. assertion------3.44------
35. assertion---------------
split_goal_wp
  1. assertion------0.14---0.13
2. assertion------0.12------
36. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------0.16------
2. VC for div3by2_inv------0.74------
3. VC for div3by2_inv------0.12------
4. VC for div3by2_inv------0.04------
5. VC for div3by2_inv------0.11------
6. VC for div3by2_inv------0.57------
7. VC for div3by2_inv------0.04------
8. VC for div3by2_inv------0.12------
9. VC for div3by2_inv------0.11------
10. VC for div3by2_inv------0.11------
11. VC for div3by2_inv------0.04------
12. VC for div3by2_inv------0.10------
13. VC for div3by2_inv---0.20---------
37. assertion---------------
split_goal_wp
  1. assertion---0.182.32------
2. assertion------2.54------
38. assertion---------------
split_goal_wp
  1. VC for div3by2_inv---------1.14---
2. VC for div3by2_inv------------0.02
3. VC for div3by2_inv------------0.12
39. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------------0.10
2. VC for div3by2_inv------------0.10
40. postcondition------0.15---0.01
41. postcondition------0.18------
42. assertion------0.51------
43. postcondition---0.150.110.02---
44. postcondition------0.12------
45. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------0.08------
2. VC for div3by2_inv------0.10------
3. VC for div3by2_inv------0.10------
4. VC for div3by2_inv------0.09------
5. VC for div3by2_inv---0.14---2.10---
6. VC for div3by2_inv------0.090.03---
46. assertion------0.09------
47. precondition---0.130.100.020.08
48. precondition---0.120.110.020.03
49. assertion------0.29------
50. assertion---------------
split_goal_wp
  1. assertion------0.10------
2. assertion---0.140.11------
51. assertion---------------
split_goal_wp
  1. VC for div3by2_inv------0.12------
2. VC for div3by2_inv------0.44------
3. VC for div3by2_inv------0.12------
4. VC for div3by2_inv------0.04------
5. VC for div3by2_inv------0.12------
6. VC for div3by2_inv------0.30------
7. VC for div3by2_inv------0.04------
8. VC for div3by2_inv------0.14------
9. VC for div3by2_inv------0.12------
10. VC for div3by2_inv------0.14------
11. VC for div3by2_inv------0.04------
12. VC for div3by2_inv------0.12------
13. VC for div3by2_inv---1.40---------
52. assertion---------------
split_goal_wp
  1. assertion------4.03------
2. assertion------1.97------
53. assertion---------------
split_goal_wp
  1. VC for div3by2_inv---------0.97---
2. VC for div3by2_inv------------0.02
3. VC for div3by2_inv------------0.12
54. assertion------3.96------
55. postcondition------0.10---0.11
56. postcondition------0.10------
57. assertion------0.33------
58. postcondition---0.100.080.030.04
59. postcondition------0.08------
VC for bounds_imply_rec3by20.03------------
VC for reciprocal_word_3by2---------------
split_goal_wp
  1. integer overflow0.03------------
2. precondition0.03------------
3. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by20.03------------
2. VC for reciprocal_word_3by20.20------------
3. VC for reciprocal_word_3by20.15------------
4. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by20.03------------
2. VC for reciprocal_word_3by20.29------------
3. VC for reciprocal_word_3by20.03------------
4. VC for reciprocal_word_3by2------0.08------
5. VC for reciprocal_word_3by20.03---0.060.27---
6. VC for reciprocal_word_3by20.04---0.050.03---
7. VC for reciprocal_word_3by20.06---0.050.03---
5. assertion------0.16------
6. assertion---------------
split_goal_wp
  1. assertion------0.93------
7. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------------0.06
2. VC for reciprocal_word_3by2------------0.04
3. VC for reciprocal_word_3by2------------0.02
8. assertion0.05------------
9. integer overflow---0.910.07---0.03
10. integer overflow0.02------------
11. assertion---0.07---------
12. integer overflow---0.96---------
13. assertion0.042.670.06---0.04
14. assertion------0.40------
15. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2---0.09---------
2. VC for reciprocal_word_3by20.04---0.05---0.01
16. assertion0.150.07---------
17. assertion0.18------------
18. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------------0.04
2. VC for reciprocal_word_3by20.23------------
3. VC for reciprocal_word_3by20.27---------0.04
4. VC for reciprocal_word_3by20.29------------
5. VC for reciprocal_word_3by20.29---------0.06
6. VC for reciprocal_word_3by20.28------------
19. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by20.24---0.06---0.03
2. VC for reciprocal_word_3by2------------0.02
3. VC for reciprocal_word_3by20.58---0.19---0.04
20. assertion---------------
split_goal_wp
  1. assertion------0.10------
2. assertion------0.12------
21. integer overflow------0.12---0.05
22. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2---0.08---0.03---
2. VC for reciprocal_word_3by2------0.05------
3. VC for reciprocal_word_3by2------0.08------
4. VC for reciprocal_word_3by2------0.07------
5. VC for reciprocal_word_3by2------0.05------
6. VC for reciprocal_word_3by2------0.04------
7. VC for reciprocal_word_3by2------0.03------
8. VC for reciprocal_word_3by2---------0.03---
23. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------------0.03
2. VC for reciprocal_word_3by2------0.19---0.00
24. integer overflow---1.04---------
25. precondition---0.08---------
26. postcondition---0.060.060.020.01
27. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------0.13------
2. VC for reciprocal_word_3by2------0.14------
28. integer overflow------0.12---0.04
29. precondition---0.10---------
30. postcondition---0.080.060.020.00
31. precondition------0.65------
32. postcondition---0.060.050.020.01
33. integer overflow------0.10---0.03
34. assertion---0.100.09---0.03
35. assertion------0.22------
36. assertion---0.12---------
37. assertion0.07------------
38. assertion---------------
split_goal_wp
  1. assertion------0.09------
39. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------0.08---0.04
2. VC for reciprocal_word_3by2------0.10------
3. VC for reciprocal_word_3by2------0.05---0.03
4. VC for reciprocal_word_3by2------0.16------
5. VC for reciprocal_word_3by2------0.06------
6. VC for reciprocal_word_3by2------0.07------
40. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------0.06---0.03
2. VC for reciprocal_word_3by2------------0.04
3. VC for reciprocal_word_3by2------0.11---0.04
41. assertion------0.09------
42. integer overflow------------0.04
43. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by20.20------------
2. VC for reciprocal_word_3by2------0.05------
3. VC for reciprocal_word_3by2------0.09------
4. VC for reciprocal_word_3by2------0.08------
5. VC for reciprocal_word_3by2------0.06------
6. VC for reciprocal_word_3by2------0.03------
7. VC for reciprocal_word_3by2------0.03------
8. VC for reciprocal_word_3by2---------0.03---
44. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------------0.03
2. VC for reciprocal_word_3by2------0.25---0.01
45. integer overflow---1.02---------
46. precondition---------------
split_goal_wp
  1. VC for reciprocal_word_3by2---0.09---------
2. VC for reciprocal_word_3by2---0.09---------
47. postcondition---0.080.070.020.02
48. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------0.12------
2. VC for reciprocal_word_3by2------0.17------
49. integer overflow------0.12---0.04
50. precondition---0.08---------
51. postcondition---0.080.060.020.02
52. precondition---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------0.15------
2. VC for reciprocal_word_3by2------0.44------
53. postcondition---0.070.050.010.02
54. assertion---2.380.08------
55. assertion---1.630.07------
56. assertion---------------
split_goal_wp
  1. assertion------0.07------
57. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------0.11---0.05
2. VC for reciprocal_word_3by20.07---0.12------
3. VC for reciprocal_word_3by20.06---0.06---0.04
4. VC for reciprocal_word_3by20.10---0.10------
5. VC for reciprocal_word_3by20.06---0.05------
6. VC for reciprocal_word_3by20.05---0.08------
58. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by20.04------------
2. VC for reciprocal_word_3by20.05------------
3. VC for reciprocal_word_3by24.24---------0.04
59. assertion------0.13------
60. integer overflow------------0.04
61. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2---------0.03---
2. VC for reciprocal_word_3by2------0.06------
3. VC for reciprocal_word_3by2------0.10------
4. VC for reciprocal_word_3by2------0.08------
5. VC for reciprocal_word_3by2------0.06------
6. VC for reciprocal_word_3by2------0.04------
7. VC for reciprocal_word_3by2------0.03------
8. VC for reciprocal_word_3by2---------0.03---
62. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------0.11------
2. VC for reciprocal_word_3by2------0.26------
63. integer overflow---1.02---------
64. precondition---------------
split_goal_wp
  1. VC for reciprocal_word_3by2---0.10---------
2. VC for reciprocal_word_3by2---0.10---------
65. postcondition---0.060.060.020.02
66. assertion---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------0.06------
2. VC for reciprocal_word_3by2------0.16---0.01
67. integer overflow------0.09---0.04
68. precondition---------------
split_goal_wp
  1. VC for reciprocal_word_3by2---0.07---------
2. VC for reciprocal_word_3by2---0.07---------
69. postcondition---0.080.070.020.01
70. precondition---------------
split_goal_wp
  1. VC for reciprocal_word_3by2------------0.04
2. VC for reciprocal_word_3by2------0.36------
71. postcondition---0.060.050.010.01
VC for sub3---------------
split_goal_wp
  1. integer overflow0.03------------
2. precondition0.03------------
3. precondition0.02------------
4. integer overflow0.03------------
5. postcondition0.02------------
VC for submul_limb---------------
split_goal_wp
  1. integer overflow0.02------------
2. integer overflow0.02------------
3. loop invariant init---------------
split_goal_wp
  1. VC for submul_limb0.03------------
2. VC for submul_limb0.02------------
4. loop invariant init0.09------------
5. loop invariant init---------------
split_goal_wp
  
6. loop invariant init---------------
split_goal_wp
  
7. precondition---------------
split_goal_wp
  1. VC for submul_limb0.03------------
2. VC for submul_limb0.03------------
8. precondition---------------
split_goal_wp
  1. VC for submul_limb0.02------------
2. VC for submul_limb0.04------------
9. assertion0.06------------
10. precondition0.04------------
11. precondition------------0.04
12. precondition---------------
split_goal_wp
  1. VC for submul_limb------------0.02
2. VC for submul_limb------------0.01
13. precondition---------------
split_goal_wp
  1. VC for submul_limb------------0.05
2. VC for submul_limb------------0.05
14. assertion---------------
split_goal_wp
  1. assertion------------0.04
2. assertion---------0.70---
3. VC for submul_limb------------0.02
15. assertion---------0.09---
16. assertion---------------
split_goal_wp
  1. VC for submul_limb------------0.06
2. VC for submul_limb------------0.04
3. VC for submul_limb------------0.04
4. VC for submul_limb------------0.04
5. VC for submul_limb------------0.02
6. VC for submul_limb------------0.02
7. VC for submul_limb------------0.03
8. VC for submul_limb------------0.04
17. assertion---------------
split_goal_wp
  1. VC for submul_limb0.02------------
2. VC for submul_limb------------0.04
3. VC for submul_limb------------0.04
18. assertion---------------
split_goal_wp
  1. assertion------------0.03
2. VC for submul_limb------------0.04
19. assertion---------------
split_goal_wp
  1. assertion------------0.01
2. VC for submul_limb------------0.17
20. integer overflow------------0.11
21. integer overflow------------0.04
22. integer overflow------------0.05
23. assertion---------------
split_goal_wp
  1. VC for submul_limb---0.92---------
2. VC for submul_limb---------------
inline_all
  1. VC for submul_limb---0.11---------
3. VC for submul_limb---------0.02---
4. VC for submul_limb---------0.09---
5. VC for submul_limb------------0.02
6. VC for submul_limb------------0.01
7. VC for submul_limb---------0.03---
8. VC for submul_limb------------0.01
9. VC for submul_limb---------0.10---
10. VC for submul_limb---------------
introduce_premises
  1. VC for submul_limb---------------
inline_goal
  1. VC for submul_limb---------0.06---
11. VC for submul_limb------0.05---0.01
12. VC for submul_limb------------0.01
13. VC for submul_limb------------0.05
14. VC for submul_limb---------0.03---
15. VC for submul_limb---1.66---------
16. VC for submul_limb---------0.10---
24. loop variant decrease---------------
split_goal_wp
  1. VC for submul_limb------------0.03
2. VC for submul_limb------------0.04
25. loop invariant preservation---------------
split_goal_wp
  1. VC for submul_limb------------0.04
2. VC for submul_limb------------0.05
26. loop invariant preservation------------0.02
27. loop invariant preservation---------4.60---
28. loop invariant preservation------0.15------
29. postcondition0.02------------
30. postcondition0.03------------
VC for div_sb_qr---------------
split_goal_wp
  1. integer overflow0.02---------0.02
2. integer overflow0.02---------0.03
3. integer overflow0.04---------0.02
4. integer overflow0.04---------0.03
5. integer overflow0.02---------0.02
6. integer overflow0.03---------0.02
7. integer overflow0.02---------0.02
8. integer overflow0.05---------0.02
9. precondition0.03------------
10. integer overflow0.06---------0.03
11. precondition0.03------------
12. integer overflow0.10---------0.04
13. precondition------------0.03
14. assertion---------------
split_goal_wp
  1. VC for div_sb_qr0.03------------
2. VC for div_sb_qr0.04------------
15. integer overflow0.08---------0.03
16. precondition0.03------------
17. precondition---------------
split_goal_wp
  1. precondition0.03---------0.03
18. integer overflow0.02---------0.03
19. integer overflow0.03---------0.03
20. precondition0.05------------
21. precondition0.08------------
22. precondition0.06------------
23. assertion---------------
split_goal_wp
  1. assertion---------0.02---
2. assertion------0.08------
24. precondition0.03------------
25. precondition0.06------------
26. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_sb_qr------0.07------
2. VC for div_sb_qr------0.12------
3. VC for div_sb_qr------0.07------
4. VC for div_sb_qr------0.13------
27. precondition0.04------------
28. assertion---------------
inline_all
  1. assertion---1.08---------
29. assertion---------------
split_goal_wp
  1. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------0.16---
2. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------0.02---
30. precondition------0.12------
31. precondition0.04------------
32. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------0.68---
33. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------------0.02
2. VC for div_sb_qr------------0.02
3. VC for div_sb_qr0.04------------
4. VC for div_sb_qr0.04------------
5. VC for div_sb_qr0.03------------
6. VC for div_sb_qr0.04------------
7. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------1.32---
8. VC for div_sb_qr0.03------------
9. VC for div_sb_qr0.03------------
10. VC for div_sb_qr0.26------------
34. precondition------0.14------
35. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.09------
2. VC for div_sb_qr0.03------------
3. VC for div_sb_qr------0.51------
4. VC for div_sb_qr0.09------------
36. precondition------0.09------
37. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.84---
2. VC for div_sb_qr---0.120.11---0.02
3. VC for div_sb_qr------0.51------
4. VC for div_sb_qr0.43------------
5. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr0.30------------
6. VC for div_sb_qr------------0.02
7. VC for div_sb_qr---0.96---------
8. VC for div_sb_qr0.22------------
9. VC for div_sb_qr1.07---------0.06
10. VC for div_sb_qr------0.11---0.04
11. VC for div_sb_qr---0.110.12---0.01
12. VC for div_sb_qr---0.160.12---0.04
38. postcondition---------------
introduce_premises
  1. postcondition---------------
inline_goal
  1. postcondition---------0.11---
39. postcondition0.15------------
40. assertion---------------
split_goal_wp
  1. VC for div_sb_qr0.04------------
2. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr0.460.21---0.50---
41. assertion---------------
split_goal_wp
  1. VC for div_sb_qr0.06------------
2. VC for div_sb_qr0.04------------
3. VC for div_sb_qr------------0.06
4. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.09---
42. precondition------0.16------
43. precondition------------0.08
44. precondition------0.08------
45. precondition------------0.02
46. precondition------------0.03
47. assertion---------------
split_goal_wp
  1. VC for div_sb_qr0.06------------
2. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.13---------
3. VC for div_sb_qr---1.30---------
4. VC for div_sb_qr------------0.06
5. VC for div_sb_qr---0.97---------
6. VC for div_sb_qr------------0.03
7. VC for div_sb_qr------------0.05
8. VC for div_sb_qr---------0.76---
9. VC for div_sb_qr---1.26---------
10. VC for div_sb_qr---1.48---------
11. VC for div_sb_qr---1.32---------
12. VC for div_sb_qr------------0.01
13. VC for div_sb_qr---1.25---------
14. VC for div_sb_qr------------0.09
48. precondition------0.09------
49. precondition------0.09------
50. precondition------0.16------
51. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------------0.11
2. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------1.58---
3. VC for div_sb_qr---------0.03---
4. VC for div_sb_qr------------0.02
5. VC for div_sb_qr0.100.12---0.03---
6. VC for div_sb_qr------------0.04
52. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.11---------
2. VC for div_sb_qr------------0.06
3. VC for div_sb_qr0.08------------
4. VC for div_sb_qr0.06------------
5. VC for div_sb_qr---------0.70---
6. VC for div_sb_qr------0.54------
7. VC for div_sb_qr0.10------------
8. VC for div_sb_qr0.12------------
9. VC for div_sb_qr0.18------------
53. postcondition---0.10---------
54. postcondition------------0.01
55. postcondition------------0.03
56. loop invariant init------0.10---0.04
57. loop invariant init0.04---0.11------
58. loop invariant init0.03---0.38------
59. loop invariant init0.12---------0.04
60. loop invariant init0.09---0.15---0.03
61. loop invariant init0.15---------0.07
62. loop invariant init------0.13------
63. loop invariant init------------0.03
64. loop invariant init0.05------------
65. loop invariant init0.03------------
66. integer overflow------------0.08
67. precondition------------0.11
68. precondition------------0.11
69. precondition---------------
split_goal_wp
  1. VC for div_sb_qr0.20---------0.09
2. VC for div_sb_qr------0.15------
70. integer overflow------0.18---0.06
71. precondition------0.11------
72. precondition------0.16------
73. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.32------
2. VC for div_sb_qr------------0.02
3. VC for div_sb_qr------------0.13
4. VC for div_sb_qr------------0.14
5. VC for div_sb_qr0.32------------
6. VC for div_sb_qr---1.76---------
7. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.12---
74. precondition------0.18------
75. precondition------0.19------
76. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.14---------
2. VC for div_sb_qr---1.16---------
3. VC for div_sb_qr---1.28---------
4. VC for div_sb_qr---1.14---------
5. VC for div_sb_qr---0.100.12------
77. precondition------0.13------
78. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------------0.07
2. VC for div_sb_qr------0.26------
3. VC for div_sb_qr------------0.02
4. VC for div_sb_qr------------0.10
5. VC for div_sb_qr------------0.06
6. VC for div_sb_qr---0.12---------
7. VC for div_sb_qr---1.26---------
8. VC for div_sb_qr---0.14---------
9. VC for div_sb_qr------0.26------
10. VC for div_sb_qr---0.16---------
11. VC for div_sb_qr------0.13------
79. assertion------0.25---0.05
80. postcondition------0.12------
81. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition------3.23------
82. precondition------0.13------
83. precondition------0.25------
84. assertion---------------
split_goal_wp
  1. assertion------1.69------
2. VC for div_sb_qr------------0.19
3. VC for div_sb_qr------------0.16
4. VC for div_sb_qr------------0.16
5. VC for div_sb_qr------------0.04
85. precondition------1.05------
86. postcondition---------------
introduce_premises
  1. postcondition---------------
inline_goal
  1. postcondition---------0.09---
87. precondition------0.15------
88. precondition------0.13------
89. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---------0.16---
2. VC for div_sb_qr------------0.07
3. VC for div_sb_qr------------0.04
4. VC for div_sb_qr------------0.03
5. VC for div_sb_qr------------0.04
6. VC for div_sb_qr------------0.05
7. VC for div_sb_qr------0.18------
8. VC for div_sb_qr------------0.03
9. VC for div_sb_qr------------0.20
10. VC for div_sb_qr------------0.01
11. VC for div_sb_qr------------0.06
90. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.12---------
2. VC for div_sb_qr------------0.05
3. VC for div_sb_qr------0.28------
4. VC for div_sb_qr------0.43------
5. VC for div_sb_qr------------0.06
6. VC for div_sb_qr------------0.06
7. VC for div_sb_qr---0.15---------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
8. VC for div_sb_qr------------0.04
9. VC for div_sb_qr------------0.02
10. VC for div_sb_qr---0.17---------
11. VC for div_sb_qr------------0.02
12. VC for div_sb_qr------------0.06
13. VC for div_sb_qr------------0.04
14. VC for div_sb_qr---0.14---------
15. VC for div_sb_qr------------0.08
16. VC for div_sb_qr------------0.06
17. VC for div_sb_qr------------0.02
18. VC for div_sb_qr------------0.02
19. VC for div_sb_qr------------0.04
20. VC for div_sb_qr------------0.03
21. VC for div_sb_qr------------0.04
22. VC for div_sb_qr------------0.04
23. VC for div_sb_qr------------0.02
24. VC for div_sb_qr---2.70---------
25. VC for div_sb_qr------------0.03
26. VC for div_sb_qr------------0.02
27. VC for div_sb_qr------------0.09
28. VC for div_sb_qr------------0.06
29. VC for div_sb_qr------------0.05
30. VC for div_sb_qr------------0.04
31. VC for div_sb_qr------------0.06
32. VC for div_sb_qr---0.17---------
33. VC for div_sb_qr---0.22---------
34. VC for div_sb_qr------------0.06
91. precondition------0.37------
92. precondition------0.31------
93. precondition------------0.22
94. precondition------0.19------
95. precondition------0.14------
96. precondition---------------
split_goal_wp
  1. VC for div_sb_qr------0.35---0.18
2. VC for div_sb_qr------0.37---0.20
97. precondition------0.28------
98. precondition------0.26------
99. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.26---------
2. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.21---------
3. VC for div_sb_qr------------0.06
4. VC for div_sb_qr------0.35------
5. VC for div_sb_qr------0.42---0.12
6. VC for div_sb_qr------0.51------
7. VC for div_sb_qr------1.98------
8. VC for div_sb_qr------0.36------
9. VC for div_sb_qr---0.12---------
10. VC for div_sb_qr---------0.04---
11. VC for div_sb_qr---------0.02---
12. VC for div_sb_qr------0.28------
13. VC for div_sb_qr---0.16---------
14. VC for div_sb_qr---0.22---------
introduce_premises
  1. VC for div_sb_qr---------0.04---
100. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.340.280.06
2. VC for div_sb_qr------0.43---0.06
3. VC for div_sb_qr------0.22------
4. VC for div_sb_qr------0.09------
5. VC for div_sb_qr------0.34------
6. VC for div_sb_qr------0.18---0.02
7. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.02---
8. VC for div_sb_qr------2.44------
9. VC for div_sb_qr---------0.06---
10. VC for div_sb_qr------0.180.05---
11. VC for div_sb_qr------0.05---0.02
12. VC for div_sb_qr------0.29---0.07
13. VC for div_sb_qr------0.22---0.04
14. VC for div_sb_qr------------0.02
15. VC for div_sb_qr---------0.07---
16. VC for div_sb_qr------0.310.040.01
17. VC for div_sb_qr---0.24---------
18. VC for div_sb_qr---0.24---------
19. VC for div_sb_qr---------5.08---
20. VC for div_sb_qr------0.19------
21. VC for div_sb_qr------0.32---0.06
22. VC for div_sb_qr------0.22------
23. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.37---
24. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.02---
25. VC for div_sb_qr------0.39---0.07
26. VC for div_sb_qr---0.25---------
27. VC for div_sb_qr------0.21---0.04
28. VC for div_sb_qr---0.26---------
29. VC for div_sb_qr---0.18---------
30. VC for div_sb_qr---0.17---------
31. VC for div_sb_qr------1.95------
32. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------1.05---
33. VC for div_sb_qr------0.40------
34. VC for div_sb_qr------1.98------
35. VC for div_sb_qr------2.08------
36. VC for div_sb_qr------0.40------
37. VC for div_sb_qr---6.58---------
38. VC for div_sb_qr------0.44------
39. VC for div_sb_qr---0.23---------
40. VC for div_sb_qr---0.15---------
41. VC for div_sb_qr------0.06---0.02
42. VC for div_sb_qr------0.06---0.01
43. VC for div_sb_qr------0.060.070.02
44. VC for div_sb_qr---0.30---------
45. VC for div_sb_qr------0.26------
46. VC for div_sb_qr------0.06---0.01
47. VC for div_sb_qr---0.18---------
48. VC for div_sb_qr------0.230.070.05
49. VC for div_sb_qr------0.24------
101. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------------0.12
2. VC for div_sb_qr------0.55------
3. VC for div_sb_qr------------0.03
4. VC for div_sb_qr---------0.06---
5. VC for div_sb_qr---0.16---------
6. VC for div_sb_qr------0.21------
7. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.04---
8. VC for div_sb_qr------------0.04
9. VC for div_sb_qr------------0.09
10. VC for div_sb_qr------------0.09
11. VC for div_sb_qr------------0.10
12. VC for div_sb_qr------0.34------
13. VC for div_sb_qr------------0.02
14. VC for div_sb_qr---0.21---------
15. VC for div_sb_qr------------0.00
16. VC for div_sb_qr------------0.06
17. VC for div_sb_qr------------0.07
18. VC for div_sb_qr------------0.07
19. VC for div_sb_qr------------0.08
20. VC for div_sb_qr------------0.02
21. VC for div_sb_qr------------0.05
102. precondition------0.30------
103. precondition------0.31------
104. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.99---------
2. VC for div_sb_qr------------0.02
3. VC for div_sb_qr------------0.28
4. VC for div_sb_qr------------0.09
5. VC for div_sb_qr------------0.03
6. VC for div_sb_qr------------0.02
7. VC for div_sb_qr------------0.03
8. VC for div_sb_qr------------0.11
9. VC for div_sb_qr------------0.18
10. VC for div_sb_qr---0.21---------
11. VC for div_sb_qr------------0.02
12. VC for div_sb_qr------------0.01
13. VC for div_sb_qr------------0.27
14. VC for div_sb_qr------------0.07
15. VC for div_sb_qr------------0.02
16. VC for div_sb_qr------------0.12
17. VC for div_sb_qr------------0.02
18. VC for div_sb_qr---1.12---------
19. VC for div_sb_qr------------0.05
105. loop variant decrease------0.27------
106. loop invariant preservation------0.24------
107. loop invariant preservation------0.48------
108. loop invariant preservation------2.54------
109. loop invariant preservation------0.44------
110. loop invariant preservation------0.42------
111. loop invariant preservation------0.42------
112. loop invariant preservation------0.53------
113. loop invariant preservation---0.170.300.020.01
114. loop invariant preservation------------0.01
115. loop invariant preservation------------0.01
116. assertion---------------
split_goal_wp
  1. VC for div_sb_qr0.28------------
2. VC for div_sb_qr------------0.09
3. VC for div_sb_qr------------0.06
4. VC for div_sb_qr------0.29------
5. VC for div_sb_qr------0.54------
117. precondition---------------
split_goal_wp
  1. VC for div_sb_qr0.18---0.20------
2. VC for div_sb_qr------0.17------
118. precondition------0.15---1.67
119. precondition------0.11------
120. precondition------0.12------
121. precondition------0.11------
122. assertion---------------
split_goal_wp
  1. VC for div_sb_qr0.30---------0.03
2. VC for div_sb_qr0.511.41---------
3. VC for div_sb_qr0.541.02---------
4. VC for div_sb_qr0.52---------0.03
5. VC for div_sb_qr0.32---0.22------
6. VC for div_sb_qr0.41---0.15------
7. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr0.40------0.08---
8. VC for div_sb_qr0.340.88---------
9. VC for div_sb_qr0.28---------0.01
10. VC for div_sb_qr------0.09------
123. postcondition0.24---------0.01
124. precondition0.25------------
125. precondition0.24---------0.02
126. precondition------------2.72
127. precondition------0.11------
128. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition------2.82------
129. integer overflow------0.86---0.10
130. precondition------0.95------
131. precondition---------------
split_goal_wp
  1. precondition------0.22------
2. precondition------0.20------
132. assertion---------------
split_goal_wp
  1. assertion------2.53------
2. VC for div_sb_qr------------0.19
3. VC for div_sb_qr------------0.14
4. VC for div_sb_qr------------0.12
5. VC for div_sb_qr------0.17---0.06
133. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition------0.180.070.02
134. postcondition---------------
introduce_premises
  1. postcondition---------------
inline_goal
  1. postcondition---------0.07---
135. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.170.080.20
2. VC for div_sb_qr------0.16------
136. precondition------0.40------
137. precondition------0.16------
138. precondition------0.32------
139. precondition------0.21------
140. precondition------0.31------
141. precondition------0.32------
142. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---------0.31---
2. VC for div_sb_qr---------0.04---
3. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.07---
143. precondition------0.16------
144. assertion---------------
split_goal_wp
  1. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------0.93---
2. assertion---------------
introduce_premises
  1. assertion---------------
inline_goal
  1. assertion---------1.08---
145. precondition------0.30------
146. precondition------0.29------
147. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.20---------
2. VC for div_sb_qr---1.34---------
3. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.17---------
4. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.21---------
5. VC for div_sb_qr------------0.09
6. VC for div_sb_qr---0.16---------
148. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.34------
2. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
3. VC for div_sb_qr---0.170.31------
149. assertion------0.51---0.21
150. assertion------0.30------
151. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.19------
2. VC for div_sb_qr---0.27---------
3. VC for div_sb_qr---0.20---------
4. VC for div_sb_qr---0.200.05---0.03
5. VC for div_sb_qr---0.230.06---0.01
6. VC for div_sb_qr---0.18---------
7. VC for div_sb_qr---0.16---------
8. VC for div_sb_qr---0.190.32------
152. precondition------0.33------
153. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------1.09---
2. VC for div_sb_qr------0.350.06---
3. VC for div_sb_qr------0.22------
4. VC for div_sb_qr---------0.05---
5. VC for div_sb_qr---------0.05---
154. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.28------
2. VC for div_sb_qr------------0.27
3. VC for div_sb_qr------------0.29
4. VC for div_sb_qr------0.23------
5. VC for div_sb_qr------------0.05
6. VC for div_sb_qr------------0.02
7. VC for div_sb_qr------0.30------
8. VC for div_sb_qr------1.62------
9. VC for div_sb_qr------1.64------
10. VC for div_sb_qr------0.51------
11. VC for div_sb_qr---0.180.22------
12. VC for div_sb_qr------0.26------
13. VC for div_sb_qr------0.27------
14. VC for div_sb_qr------2.96------
15. VC for div_sb_qr------------0.03
16. VC for div_sb_qr------------0.03
17. VC for div_sb_qr------0.06------
18. VC for div_sb_qr------------0.02
19. VC for div_sb_qr------------0.02
20. VC for div_sb_qr------------0.01
21. VC for div_sb_qr------0.28------
22. VC for div_sb_qr------------0.08
23. VC for div_sb_qr------------0.03
24. VC for div_sb_qr------------0.03
25. VC for div_sb_qr---0.27---------
26. VC for div_sb_qr---0.24---------
27. VC for div_sb_qr------0.25------
28. VC for div_sb_qr------0.30---0.02
29. VC for div_sb_qr------0.29------
155. postcondition---0.260.32------
156. assertion------0.30---0.08
157. precondition------0.30------
158. precondition------0.20------
159. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.43------
2. VC for div_sb_qr------------0.14
3. VC for div_sb_qr------------0.03
4. VC for div_sb_qr------------0.02
5. VC for div_sb_qr---1.36---------
6. VC for div_sb_qr------------0.11
7. VC for div_sb_qr------------0.05
8. VC for div_sb_qr------------0.23
9. VC for div_sb_qr------------0.06
10. VC for div_sb_qr------------0.04
11. VC for div_sb_qr------1.860.024.79
12. VC for div_sb_qr------------0.16
13. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.18---------
14. VC for div_sb_qr------0.25---0.07
15. VC for div_sb_qr------------0.06
16. VC for div_sb_qr---1.03---------
17. VC for div_sb_qr------------0.05
18. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.20------1.18
19. VC for div_sb_qr---0.18---------
160. postcondition------------0.01
161. precondition------0.19------
162. precondition------0.33------
163. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.22---------
2. VC for div_sb_qr---1.34---------
3. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.18---------
4. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.19---------
5. VC for div_sb_qr------0.20------
164. assertion---------------
split_goal_wp
  1. assertion---0.17---------
2. assertion---0.16---------
165. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------------0.06
2. VC for div_sb_qr------0.28------
3. VC for div_sb_qr------------0.08
4. VC for div_sb_qr---0.25---------
5. VC for div_sb_qr------------0.14
6. VC for div_sb_qr------------0.19
7. VC for div_sb_qr---0.26---------
8. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.38---------
9. VC for div_sb_qr------------0.09
10. VC for div_sb_qr------------0.01
11. VC for div_sb_qr------------0.06
12. VC for div_sb_qr------------0.01
13. VC for div_sb_qr------------0.08
14. VC for div_sb_qr------------0.23
15. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.22---------
16. VC for div_sb_qr---0.28---------
17. VC for div_sb_qr------------0.05
18. VC for div_sb_qr------------0.07
19. VC for div_sb_qr------------0.02
20. VC for div_sb_qr------2.06------
21. VC for div_sb_qr------------0.18
22. VC for div_sb_qr------------0.02
23. VC for div_sb_qr---0.18---------
24. VC for div_sb_qr------------0.01
25. VC for div_sb_qr---0.18---------
26. VC for div_sb_qr---0.18---------
27. VC for div_sb_qr------------0.02
28. VC for div_sb_qr---0.26------0.01
29. VC for div_sb_qr---1.22---------
30. VC for div_sb_qr------------0.01
31. VC for div_sb_qr------------0.04
166. postcondition------------0.05
167. assertion---------------
split_goal_wp
  1. assertion------------0.24
2. assertion------------0.07
3. assertion------------0.08
4. assertion------------0.17
5. VC for div_sb_qr------------0.06
6. VC for div_sb_qr------------0.05
7. VC for div_sb_qr------------0.21
168. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition------------0.02
169. integer overflow------1.94---0.27
170. integer overflow------------0.25
171. precondition------------0.09
172. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_sb_qr------2.00------
2. VC for div_sb_qr------0.12------
3. VC for div_sb_qr------------5.62
4. VC for div_sb_qr------------6.04
173. precondition------0.43------
174. assertion---------------
split_goal_wp
  1. assertion------------0.08
2. VC for div_sb_qr------------0.08
3. VC for div_sb_qr------------0.22
4. VC for div_sb_qr------------0.20
5. VC for div_sb_qr------------0.21
6. VC for div_sb_qr------------0.21
7. VC for div_sb_qr------0.38------
175. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition------0.28------
176. postcondition---------------
introduce_premises
  1. postcondition---------------
inline_goal
  1. postcondition---------0.08---
177. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.30---------
2. VC for div_sb_qr------0.52------
3. VC for div_sb_qr------0.46------
4. VC for div_sb_qr------2.69------
5. VC for div_sb_qr------------0.02
6. VC for div_sb_qr------------0.05
7. VC for div_sb_qr------------0.10
8. VC for div_sb_qr---0.20---------
9. VC for div_sb_qr------------0.04
10. VC for div_sb_qr------------0.05
178. precondition------0.06------
179. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---------0.05---
2. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr------------0.01
3. VC for div_sb_qr---0.22---------
4. VC for div_sb_qr---------0.70---
5. VC for div_sb_qr------0.23------
6. VC for div_sb_qr------0.47------
7. VC for div_sb_qr------------0.02
8. VC for div_sb_qr------0.24------
180. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------------0.09
2. VC for div_sb_qr------------0.22
181. precondition------0.28------
182. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.29---------
inline_all
  1. VC for div_sb_qr---0.29---------
2. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.08---
3. VC for div_sb_qr------0.43------
4. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr------0.04------
5. VC for div_sb_qr------0.08------
6. VC for div_sb_qr---------0.04---
7. VC for div_sb_qr---1.82---------
8. VC for div_sb_qr------0.33------
9. VC for div_sb_qr------0.310.040.06
10. VC for div_sb_qr------2.12------
11. VC for div_sb_qr------------0.05
12. VC for div_sb_qr---1.17---------
13. VC for div_sb_qr------0.280.240.02
14. VC for div_sb_qr------0.42---0.02
15. VC for div_sb_qr------0.45---0.12
16. VC for div_sb_qr------------0.09
17. VC for div_sb_qr------0.321.510.05
18. VC for div_sb_qr---0.30---------
183. postcondition---------0.030.02
184. integer overflow------------0.24
185. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.21---------
2. VC for div_sb_qr---0.24---------
3. VC for div_sb_qr---0.31---------
4. VC for div_sb_qr------0.06------
5. VC for div_sb_qr---0.160.490.03---
186. precondition------------0.26
187. precondition------0.29------
188. precondition------0.06------
189. precondition---------------
split_goal_wp
  1. VC for div_sb_qr------0.74---0.28
2. VC for div_sb_qr------0.57------
190. precondition------0.40------
191. precondition------0.33------
192. precondition------0.54------
193. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------0.56------
2. VC for div_sb_qr------4.20------
3. VC for div_sb_qr---0.280.57------
4. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------1.08---
5. VC for div_sb_qr------0.33------
6. VC for div_sb_qr------0.61------
7. VC for div_sb_qr------0.32---0.02
8. VC for div_sb_qr------0.580.280.05
9. VC for div_sb_qr------0.52---0.04
10. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
11. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.09---
12. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.04---
13. VC for div_sb_qr------0.52------
14. VC for div_sb_qr---------12.80---
15. VC for div_sb_qr------0.32---0.10
16. VC for div_sb_qr------0.36---0.05
17. VC for div_sb_qr------------0.02
18. VC for div_sb_qr---------0.10---
19. VC for div_sb_qr------0.340.060.02
20. VC for div_sb_qr---0.20---------
introduce_premises
  1. VC for div_sb_qr---------0.04---
21. VC for div_sb_qr---------0.10---
22. VC for div_sb_qr---0.20---------
23. VC for div_sb_qr------0.05------
24. VC for div_sb_qr---------0.04---
25. VC for div_sb_qr------0.48------
26. VC for div_sb_qr------0.640.08---
27. VC for div_sb_qr---------0.13---
28. VC for div_sb_qr------0.66---0.09
29. VC for div_sb_qr------0.50------
30. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.02---
31. VC for div_sb_qr------0.32------
32. VC for div_sb_qr------0.60------
33. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.23---
34. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
35. VC for div_sb_qr------0.340.08---
36. VC for div_sb_qr------0.320.080.05
37. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.08---
38. VC for div_sb_qr---1.52---------
39. VC for div_sb_qr------0.48------
40. VC for div_sb_qr------0.32------
41. VC for div_sb_qr------0.06---0.02
42. VC for div_sb_qr------0.07---0.02
43. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
44. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
45. VC for div_sb_qr------0.36------
46. VC for div_sb_qr------3.40------
47. VC for div_sb_qr------4.50------
48. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.02---
49. VC for div_sb_qr---------0.06---
50. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr------------0.01
51. VC for div_sb_qr---------0.49---
52. VC for div_sb_qr------0.07---0.02
53. VC for div_sb_qr---0.23---------
54. VC for div_sb_qr------0.06---0.01
55. VC for div_sb_qr------0.460.090.08
56. VC for div_sb_qr------0.39------
194. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------------0.06
2. VC for div_sb_qr------0.70------
3. VC for div_sb_qr------------0.16
4. VC for div_sb_qr------------0.02
5. VC for div_sb_qr------------0.02
6. VC for div_sb_qr---1.26---------
7. VC for div_sb_qr------------0.11
8. VC for div_sb_qr------------0.05
9. VC for div_sb_qr------------0.12
10. VC for div_sb_qr------0.58------
11. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---0.36---0.04---
12. VC for div_sb_qr------------0.12
195. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---1.42---------
2. VC for div_sb_qr------------0.02
3. VC for div_sb_qr------------0.36
4. VC for div_sb_qr------------0.17
5. VC for div_sb_qr------------0.02
6. VC for div_sb_qr------------0.02
7. VC for div_sb_qr------------0.17
8. VC for div_sb_qr------------0.17
9. VC for div_sb_qr------------0.35
10. VC for div_sb_qr---0.28---------
11. VC for div_sb_qr------------0.02
12. VC for div_sb_qr------------0.11
13. VC for div_sb_qr------------0.16
14. VC for div_sb_qr------------0.06
15. VC for div_sb_qr------------0.02
16. VC for div_sb_qr------------0.13
17. VC for div_sb_qr------------0.02
18. VC for div_sb_qr---1.68---------
19. VC for div_sb_qr------------0.06
196. loop variant decrease---------------
split_goal_wp
  1. VC for div_sb_qr------0.52---0.04
2. VC for div_sb_qr------------0.18
197. loop invariant preservation------0.41------
198. loop invariant preservation------0.85------
199. loop invariant preservation------4.65------
200. loop invariant preservation------0.61------
201. loop invariant preservation------0.74---0.05
202. loop invariant preservation------0.62------
203. loop invariant preservation------0.56---0.04
204. loop invariant preservation------0.25------
205. loop invariant preservation------------0.02
206. loop invariant preservation------------0.02
207. precondition------------0.16
208. precondition------0.20------
209. precondition------0.05------
210. precondition---------------
split_goal_wp
  1. VC for div_sb_qr------0.45------
2. VC for div_sb_qr------0.44------
211. precondition------0.31------
212. precondition------0.24------
213. precondition------0.65------
214. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------1.20---
2. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.13---
3. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.40---
4. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------1.06---
5. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
6. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.58---
7. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.38---
8. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr------0.34------
9. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.14---
10. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.04---
11. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.12---
12. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.06---
13. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.02---
14. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.27---
15. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.57---
16. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr------0.08------
17. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.06---
18. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.04---
19. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.03---
20. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.04---
21. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.16---
22. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.03---
23. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.03---
24. VC for div_sb_qr------0.08------
25. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.17---
26. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr------0.13------
27. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.26---
28. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.15---
29. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.08---
30. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.68---
31. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.02---
32. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.10---
33. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.12---
34. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.34---
35. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
36. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.06---
37. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------1.60---
38. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr------0.15------
39. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.04---
40. VC for div_sb_qr------0.08------
41. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr------0.05------
42. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
43. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
44. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr------0.07------
45. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------2.01---
46. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.09---
47. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.04---
48. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.03---
49. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr------0.05------
50. VC for div_sb_qr---0.31---------
51. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr------0.04------
52. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr------0.05------
53. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
54. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
55. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.04---
215. precondition------0.34------
216. precondition------0.38------
217. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---0.22---------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.02---
2. VC for div_sb_qr---1.61---------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
3. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.34---------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.90---
4. VC for div_sb_qr---------------
inline_all
  1. VC for div_sb_qr---0.20---------
5. VC for div_sb_qr------0.24------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.04---
218. assertion---------------
split_goal_wp
  1. VC for div_sb_qr------------0.11
2. VC for div_sb_qr------0.66------
3. VC for div_sb_qr------------0.03
4. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.02---
5. VC for div_sb_qr---0.29---------
6. VC for div_sb_qr------------0.02
7. VC for div_sb_qr------------0.05
8. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr------0.130.26---
9. VC for div_sb_qr------0.41------
10. VC for div_sb_qr---1.16---------
11. VC for div_sb_qr---0.32---------
12. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.06---
13. VC for div_sb_qr------------0.30
14. VC for div_sb_qr------------0.27
15. VC for div_sb_qr------------0.26
16. VC for div_sb_qr---0.22---------
17. VC for div_sb_qr------------0.08
18. VC for div_sb_qr------------0.14
19. VC for div_sb_qr---0.35---------
20. VC for div_sb_qr------------0.03
21. VC for div_sb_qr---0.23---------
22. VC for div_sb_qr------3.13------
23. VC for div_sb_qr------------0.06
24. VC for div_sb_qr---0.20---------
25. VC for div_sb_qr------------0.02
26. VC for div_sb_qr------------0.01
27. VC for div_sb_qr------------0.02
28. VC for div_sb_qr------------0.02
29. VC for div_sb_qr------------0.03
30. VC for div_sb_qr------------0.02
31. VC for div_sb_qr------------0.02
32. VC for div_sb_qr------------0.34
33. VC for div_sb_qr------------0.01
34. VC for div_sb_qr------------0.06
35. VC for div_sb_qr---0.29---------
36. VC for div_sb_qr------------0.08
37. VC for div_sb_qr------------0.17
219. precondition------0.37------
220. precondition------0.30------
221. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---1.06---------
2. VC for div_sb_qr---0.29---------
3. VC for div_sb_qr------------0.31
4. VC for div_sb_qr------------0.16
5. VC for div_sb_qr------------0.02
6. VC for div_sb_qr---0.33---------
7. VC for div_sb_qr------------0.06
8. VC for div_sb_qr------------0.09
9. VC for div_sb_qr---0.23---------
10. VC for div_sb_qr---0.23---------
11. VC for div_sb_qr---0.31---------
12. VC for div_sb_qr------------0.02
13. VC for div_sb_qr------------0.29
14. VC for div_sb_qr------------0.02
15. VC for div_sb_qr---0.26---------
16. VC for div_sb_qr------------0.03
17. VC for div_sb_qr------------0.03
18. VC for div_sb_qr---1.46---------
19. VC for div_sb_qr------------0.03
222. loop variant decrease---------------
split_goal_wp
  1. VC for div_sb_qr------0.38---0.04
2. VC for div_sb_qr------0.38---0.18
223. loop invariant preservation------0.38------
224. loop invariant preservation------0.55------
225. loop invariant preservation------4.21------
226. loop invariant preservation------0.64---0.15
227. loop invariant preservation------0.54------
228. loop invariant preservation------0.51------
229. loop invariant preservation------0.53---0.07
230. loop invariant preservation------------0.01
231. loop invariant preservation------------0.01
232. loop invariant preservation------------0.02
233. assertion------------0.04
234. assertion------------0.04
235. precondition------0.17------
236. precondition------0.04------
237. precondition------0.15------
238. assertion---4.55---------
239. precondition------0.18------
240. assertion---------------
split_goal_wp
  1. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr0.76------------
2. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.02---
3. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.09---
4. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------0.06---
5. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr0.420.120.04------
6. VC for div_sb_qr---------------
introduce_premises
  1. VC for div_sb_qr---------------
inline_goal
  1. VC for div_sb_qr---------0.03---
241. postcondition------------0.01
242. postcondition---------------
inline_all
  1. postcondition---3.39---------
243. postcondition------0.12------
VC for divmod_2---------------
split_goal_wp
  1. integer overflow------------0.04
2. integer overflow------------0.02
3. integer overflow------------0.03
4. integer overflow------------0.03
5. integer overflow------------0.02
6. integer overflow------------0.03
7. integer overflow------------0.03
8. integer overflow------------0.04
9. precondition0.03------------
10. precondition------------0.03
11. precondition------------0.04
12. precondition0.06------------
13. precondition0.04------------
14. assertion---------------
split_goal_wp
  1. assertion---1.49---------
15. integer overflow------------0.03
16. precondition------------0.05
17. precondition------------0.02
18. precondition------------0.03
19. assertion0.63------------
20. assertion0.06------------
21. precondition------0.07------
22. precondition------0.07------
23. assertion1.42------------
split_goal_wp
  1. VC for divmod_20.04---0.17------
2. VC for divmod_20.09------------
3. VC for divmod_20.03------------
4. VC for divmod_20.04------------
5. VC for divmod_20.07------------
6. VC for divmod_20.15------------
7. VC for divmod_2------0.100.05---
24. postcondition------0.07------
25. postcondition------0.92------
26. postcondition------------0.04
27. precondition------0.08------
28. precondition------0.06------
29. postcondition0.58------------
30. postcondition------0.26------
31. postcondition------------0.03
32. loop invariant init---------------
split_goal_wp
  1. VC for divmod_2------------0.04
2. VC for divmod_2------------0.04
33. loop invariant init------0.07------
34. loop invariant init------------0.05
35. loop invariant init------------0.05
36. loop invariant init---0.12---------
37. loop invariant init------------0.03
38. precondition0.04------------
39. precondition------0.10------
40. precondition------------0.04
41. precondition------------0.04
42. precondition------------0.04
43. integer overflow------------0.07
44. precondition------0.18------
45. assertion---------------
split_goal_wp
  1. VC for divmod_2------------0.02
2. VC for divmod_2------0.11------
3. VC for divmod_2------------0.01
4. VC for divmod_2------------0.05
46. precondition------0.10------
47. precondition------0.10------
48. assertion---------------
split_goal_wp
  1. VC for divmod_2---------------
introduce_premises
  1. VC for divmod_2---------------
inline_goal
  1. VC for divmod_2---------0.07---
2. VC for divmod_2---------------
introduce_premises
  1. VC for divmod_2---------0.80---
3. VC for divmod_2------0.53------
4. VC for divmod_2---0.08---------
5. VC for divmod_2------0.56------
6. VC for divmod_2---------0.04---
7. VC for divmod_2---0.10---------
8. VC for divmod_2---------0.21---
9. VC for divmod_2------0.13------
10. VC for divmod_2------0.11---0.02
11. VC for divmod_2------0.04---0.01
12. VC for divmod_2---------0.03---
13. VC for divmod_2------0.04---0.02
14. VC for divmod_2------0.10---0.02
15. VC for divmod_2---------0.35---
16. VC for divmod_2---0.57---------
17. VC for divmod_2------0.12------
49. loop variant decrease------------0.05
50. loop invariant preservation------0.10------
51. loop invariant preservation------0.10------
52. loop invariant preservation------------0.05
53. loop invariant preservation------------0.05
54. loop invariant preservation------------0.01
55. loop invariant preservation------------0.05
56. assertion------------0.04
57. assertion---------------
split_goal_wp
  1. VC for divmod_2---0.250.150.020.04
2. VC for divmod_2---------0.11---
58. precondition------0.11---0.04
59. precondition---------------
split_goal_wp
  1. VC for divmod_2------0.15---0.05
2. VC for divmod_2------0.12------
60. assertion---------------
split_goal_wp
  1. VC for divmod_20.19------------
2. VC for divmod_20.18------------
3. VC for divmod_2---------------
introduce_premises
  1. VC for divmod_2---------------
inline_goal
  1. VC for divmod_2------0.20------
61. postcondition0.14------------
62. postcondition------------0.03
63. postcondition------------0.20
VC for div_qr---------------
split_goal_wp
  1. integer overflow------------0.04
2. integer overflow------------0.03
3. integer overflow------------0.04
4. integer overflow------------0.03
5. precondition------------0.01
6. assertion---0.09---------
7. precondition------------0.02
8. precondition------------0.03
9. precondition------------0.04
10. precondition------------0.03
11. precondition------------0.05
12. precondition------------0.03
13. postcondition0.31------------
14. postcondition------0.45------
15. integer overflow------------0.03
16. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.03
2. VC for div_qr------------0.03
17. precondition0.05------0.10---
18. precondition------------0.04
19. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.03
2. VC for div_qr------------0.03
3. VC for div_qr------------0.03
4. VC for div_qr------------0.03
20. precondition------------0.01
21. precondition------------0.03
22. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.04
2. VC for div_qr------------0.03
23. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition0.07------------
24. integer overflow------------0.03
25. precondition------------0.03
26. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.04
2. VC for div_qr------------0.04
3. VC for div_qr------------0.18
4. VC for div_qr------------0.21
27. precondition------------0.02
28. precondition------------0.04
29. precondition0.09------------
30. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.04
2. VC for div_qr------------0.04
3. VC for div_qr------------0.29
4. VC for div_qr------------0.17
31. precondition------------0.02
32. assertion---------------
split_goal_wp
  1. VC for div_qr0.45------------
2. VC for div_qr0.80------------
3. VC for div_qr0.48------------
4. VC for div_qr0.05------------
5. VC for div_qr0.04------------
6. VC for div_qr------0.230.020.26
7. VC for div_qr0.14------------
8. VC for div_qr------0.230.020.35
9. VC for div_qr0.07---0.080.020.02
10. VC for div_qr---0.40---------
11. VC for div_qr0.08---0.060.120.01
12. VC for div_qr0.13------0.06---
13. VC for div_qr0.07---0.07---0.01
14. VC for div_qr---------0.07---
15. VC for div_qr2.78---0.08---0.02
16. VC for div_qr------------0.02
17. VC for div_qr0.15------------
18. VC for div_qr0.05------------
33. postcondition------------0.04
34. postcondition------1.06------
35. precondition------------0.04
36. precondition------------0.04
37. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.03
2. VC for div_qr------------0.03
3. VC for div_qr------------0.03
4. VC for div_qr------------0.03
38. precondition------------0.02
39. precondition------------0.03
40. assertion---------------
split_goal_wp
  1. assertion0.13------------
41. precondition------------0.04
42. precondition------------0.03
43. precondition------------0.03
44. assertion---------------
split_goal_wp
  1. VC for div_qr0.11------------
2. VC for div_qr0.04------------
3. VC for div_qr0.04------------
4. VC for div_qr0.11------------
5. VC for div_qr0.06------------
6. VC for div_qr1.50---------0.19
7. VC for div_qr0.06------------
8. VC for div_qr0.06------------
9. VC for div_qr0.42------------
10. VC for div_qr3.99------------
11. VC for div_qr0.06------------
12. VC for div_qr0.08------------
13. VC for div_qr0.09------------
14. VC for div_qr0.10------------
15. VC for div_qr0.07------------
16. VC for div_qr0.05------------
17. VC for div_qr0.06------------
18. VC for div_qr0.10------------
19. VC for div_qr0.06------------
20. VC for div_qr0.12------------
21. VC for div_qr0.06------------
22. VC for div_qr0.06------------
23. VC for div_qr0.09------------
24. VC for div_qr0.05------------
45. postcondition------------0.02
46. postcondition------------0.02
47. precondition------------0.03
48. precondition------------0.07
49. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition------------0.04
50. precondition------------0.02
51. precondition------------0.03
52. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.03
2. VC for div_qr------------0.03
53. precondition------------0.03
54. assertion---------------
split_goal_wp
  1. VC for div_qr---------0.80---
2. VC for div_qr0.09------------
3. VC for div_qr0.10------------
55. postcondition---------------
inline_all
  1. postcondition------------0.01
56. integer overflow------------0.07
57. precondition------------0.03
58. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.05
2. VC for div_qr------------0.04
3. VC for div_qr------------0.62
4. VC for div_qr------------0.55
59. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.06
2. VC for div_qr------------0.04
3. VC for div_qr------------0.79
4. VC for div_qr------------0.58
60. precondition------------0.44
61. precondition0.060.79---------
62. precondition------------0.02
63. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.02
2. VC for div_qr------------0.01
3. VC for div_qr------------0.82
4. VC for div_qr------------0.78
64. precondition------------0.03
65. precondition------------0.05
66. precondition------------0.03
67. assertion---------------
split_goal_wp
  1. VC for div_qr---------------
introduce_premises
  1. VC for div_qr---------------
inline_goal
  1. VC for div_qr2.29------------
2. VC for div_qr------0.090.03---
3. VC for div_qr------------0.01
4. VC for div_qr------------0.03
5. VC for div_qr---------1.28---
6. VC for div_qr------------0.01
7. VC for div_qr---------0.02---
8. VC for div_qr------------0.78
9. VC for div_qr------------0.09
10. VC for div_qr---0.30---------
11. VC for div_qr---------0.04---
12. VC for div_qr------------0.01
13. VC for div_qr---------0.24---
14. VC for div_qr------------0.05
15. VC for div_qr------0.100.05---
16. VC for div_qr0.11------0.04---
17. VC for div_qr---------0.56---
18. VC for div_qr------------0.07
19. VC for div_qr---------0.04---
20. VC for div_qr------------0.01
21. VC for div_qr---------0.04---
22. VC for div_qr---------0.33---
23. VC for div_qr---------0.02---
24. VC for div_qr------------0.01
25. VC for div_qr------------0.01
26. VC for div_qr------------0.09
27. VC for div_qr------------0.09
28. VC for div_qr------------0.03
68. assertion---------------
split_goal_wp
  1. VC for div_qr0.09------------
2. VC for div_qr------------0.03
3. VC for div_qr0.11------------
4. VC for div_qr0.12------------
5. VC for div_qr0.18------------
6. VC for div_qr---------0.03---
69. postcondition------------0.01
70. assertion---------------
split_goal_wp
  1. VC for div_qr---0.09---------
2. VC for div_qr------------0.02
3. VC for div_qr---------0.03---
4. VC for div_qr------------0.82
5. VC for div_qr------------0.06
6. VC for div_qr------------0.03
7. VC for div_qr------------0.99
8. VC for div_qr------------0.79
9. VC for div_qr---1.02---------
10. VC for div_qr------------0.00
11. VC for div_qr---------0.20---
12. VC for div_qr---0.13---------
13. VC for div_qr---------0.07---
14. VC for div_qr---------------
introduce_premises
  1. VC for div_qr---------------
inline_goal
  1. VC for div_qr---------4.89---
15. VC for div_qr------------0.03
16. VC for div_qr---0.63---------
17. VC for div_qr------------0.01
18. VC for div_qr---------1.40---
19. VC for div_qr------------0.01
20. VC for div_qr---0.10---------
71. postcondition------------0.01
72. postcondition---0.18---------
73. integer overflow------------0.03
74. precondition------0.07------
75. integer overflow0.04------------
76. precondition0.03------------
77. integer overflow0.04------------
78. precondition0.05------------
79. precondition0.05------------
80. precondition------------0.02
81. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.03
2. VC for div_qr------------0.04
3. VC for div_qr------------0.02
4. VC for div_qr------------0.03
82. precondition------------0.04
83. precondition------------0.03
84. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.05
2. VC for div_qr------------0.05
85. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition0.04------------
86. assertion---------------
split_goal_wp
  1. VC for div_qr0.09------------
2. VC for div_qr0.23------------
3. VC for div_qr0.06------------
4. VC for div_qr0.04------------
5. VC for div_qr0.41------------
6. VC for div_qr0.06------------
7. VC for div_qr0.07------------
8. VC for div_qr0.05------------
9. VC for div_qr0.10------------
10. VC for div_qr0.04------------
11. VC for div_qr---1.86---------
12. VC for div_qr0.66------------
13. VC for div_qr0.06------------
14. VC for div_qr1.12------------
15. VC for div_qr0.04------------
16. VC for div_qr0.06------------
17. VC for div_qr---------0.64---
18. VC for div_qr0.03------------
19. VC for div_qr---------------
split_goal_wp
  1. VC for div_qr0.08------------
2. VC for div_qr0.05------------
87. integer overflow0.06------------
88. precondition0.06------------
89. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.04
2. VC for div_qr------------0.04
3. VC for div_qr------------0.21
4. VC for div_qr1.82---0.20------
90. precondition------------0.03
91. precondition0.07------------
92. precondition0.08------------
93. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.03
2. VC for div_qr------------0.03
3. VC for div_qr------------0.13
4. VC for div_qr------------0.12
94. precondition------------0.03
95. assertion---------------
split_goal_wp
  1. VC for div_qr------0.090.02---
2. VC for div_qr---------------
split_goal_wp
  1. VC for div_qr1.461.56---------
2. VC for div_qr0.46------------
3. VC for div_qr---------------
split_goal_wp
  1. VC for div_qr0.31------------
2. VC for div_qr0.08------------
4. VC for div_qr---------0.10---
5. VC for div_qr------0.270.020.22
6. VC for div_qr------0.350.020.19
7. VC for div_qr------------0.05
8. VC for div_qr0.05------------
9. VC for div_qr------0.080.160.01
10. VC for div_qr0.07------------
11. VC for div_qr0.07------------
12. VC for div_qr---0.20---------
13. VC for div_qr------0.12------
14. VC for div_qr0.04------------
96. precondition0.04------------
97. precondition0.05------------
98. integer overflow0.07------------
99. precondition0.15------------
100. precondition0.06------------
101. postcondition---1.78---------
102. postcondition0.06------------
103. postcondition0.06------------
104. postcondition------0.12------
105. precondition------------0.03
106. precondition------------0.05
107. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.04
2. VC for div_qr------------0.04
3. VC for div_qr------------0.02
4. VC for div_qr------------0.03
108. precondition------------0.03
109. precondition------------0.04
110. assertion---------------
split_goal_wp
  1. assertion0.07------------
2. assertion0.15------------
111. precondition------------0.05
112. precondition------------0.04
113. precondition------------0.03
114. assertion---------------
split_goal_wp
  1. VC for div_qr0.15------------
2. VC for div_qr0.04------------
3. VC for div_qr0.07------------
4. VC for div_qr0.16------------
5. VC for div_qr---------0.03---
6. VC for div_qr---0.13---------
7. VC for div_qr0.08------------
8. VC for div_qr0.05------------
9. VC for div_qr0.42---0.080.32---
10. VC for div_qr0.14------------
11. VC for div_qr0.05------------
12. VC for div_qr0.08------------
13. VC for div_qr------0.29------
14. VC for div_qr---0.28---------
15. VC for div_qr0.05------------
16. VC for div_qr0.10------------
17. VC for div_qr---0.08---------
18. VC for div_qr0.06------------
19. VC for div_qr0.07------------
20. VC for div_qr0.06------------
21. VC for div_qr0.06------------
22. VC for div_qr---0.12---------
23. VC for div_qr0.07------------
24. VC for div_qr0.18------------
25. VC for div_qr0.08------------
26. VC for div_qr0.06------------
27. VC for div_qr0.13------------
28. VC for div_qr0.09------------
115. postcondition------------0.02
116. postcondition------------0.01
117. precondition------------0.02
118. precondition------------0.04
119. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.03
2. VC for div_qr------------0.04
3. VC for div_qr------------0.03
4. VC for div_qr------------0.03
120. precondition------------0.02
121. precondition------------0.03
122. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.05
2. VC for div_qr------------0.04
123. precondition------------0.04
124. assertion---------------
split_goal_wp
  1. VC for div_qr---------0.96---
2. VC for div_qr0.10------------
3. VC for div_qr0.08------------
125. assertion0.08------------
126. assertion---------------
split_goal_wp
  1. VC for div_qr0.14------------
2. VC for div_qr0.10------------
3. VC for div_qr0.17------------
4. VC for div_qr0.06------------
5. VC for div_qr0.12------------
6. VC for div_qr0.06------------
7. VC for div_qr---0.08---------
8. VC for div_qr0.08------------
9. VC for div_qr0.14------------
10. VC for div_qr0.06------------
11. VC for div_qr0.08------------
12. VC for div_qr0.05------------
13. VC for div_qr------0.31------
14. VC for div_qr---------0.28---
15. VC for div_qr0.08------------
16. VC for div_qr------0.09------
17. VC for div_qr---0.10---------
18. VC for div_qr0.10------------
19. VC for div_qr0.35------------
20. VC for div_qr0.07------------
21. VC for div_qr------0.18------
22. VC for div_qr------0.13------
23. VC for div_qr---0.20---------
24. VC for div_qr---------------
eliminate_let
  1. VC for div_qr------0.180.190.08
127. postcondition---------------
split_goal_wp
  1. postcondition0.07------0.04---
2. postcondition---------3.77---
128. assertion---------------
split_goal_wp
  1. VC for div_qr---0.17---------
2. VC for div_qr0.07------------
3. VC for div_qr0.16------------
4. VC for div_qr0.08------------
5. VC for div_qr------0.21---0.44
6. VC for div_qr------------0.46
7. VC for div_qr0.12------------
8. VC for div_qr---------0.56---
9. VC for div_qr0.07------------
10. VC for div_qr0.28------------
11. VC for div_qr---0.42---------
12. VC for div_qr------0.22------
13. VC for div_qr0.11------------
14. VC for div_qr---1.56---------
15. VC for div_qr---------1.36---
16. VC for div_qr0.08------------
17. VC for div_qr0.09------------
18. VC for div_qr---------0.76---
19. VC for div_qr0.06------------
20. VC for div_qr---------------
split_goal_wp
  1. VC for div_qr0.33---0.07---0.02
2. VC for div_qr0.20---0.08---0.02
129. integer overflow0.08------------
130. precondition0.07------------
131. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.03
2. VC for div_qr------------0.04
3. VC for div_qr------------0.77
4. VC for div_qr------0.21------
132. precondition------------0.07
133. precondition0.11------------
134. precondition------------0.04
135. precondition------------0.03
136. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
split_goal_wp
  1. VC for div_qr------------0.04
2. VC for div_qr------------0.04
3. VC for div_qr------------0.88
4. VC for div_qr------------0.66
137. precondition------------0.05
138. precondition------------0.04
139. precondition------------0.03
140. assertion---------------
split_goal_wp
  1. VC for div_qr0.08------------
2. VC for div_qr------0.07------
3. VC for div_qr---------0.04---
4. VC for div_qr------0.09------
5. VC for div_qr---------1.45---
6. VC for div_qr------------0.01
7. VC for div_qr---------0.12---
8. VC for div_qr------0.40------
9. VC for div_qr------------0.08
10. VC for div_qr---0.27---------
11. VC for div_qr------0.08------
12. VC for div_qr------------0.02
13. VC for div_qr---------0.35---
14. VC for div_qr------------0.08
15. VC for div_qr------0.140.05---
16. VC for div_qr0.13------0.02---
17. VC for div_qr---------0.48---
18. VC for div_qr---------0.800.06
19. VC for div_qr---------0.04---
20. VC for div_qr---0.20------0.01
21. VC for div_qr---------0.05---
22. VC for div_qr---------0.320.01
23. VC for div_qr---------0.03---
24. VC for div_qr------------0.01
25. VC for div_qr------------0.01
26. VC for div_qr------------0.09
27. VC for div_qr------------0.08
28. VC for div_qr------------0.03
141. assertion---------------
split_goal_wp
  1. VC for div_qr0.08------0.04---
2. VC for div_qr0.16------0.69---
3. VC for div_qr0.070.10---------
4. VC for div_qr0.13------0.02---
5. VC for div_qr0.08---0.08------
6. VC for div_qr0.08---0.090.040.02
142. postcondition------------0.01
143. assertion---------------
split_goal_wp
  1. VC for div_qr---------0.03---
2. VC for div_qr---------0.03---
3. VC for div_qr------------0.04
4. VC for div_qr------0.160.020.03
5. VC for div_qr---------0.09---
6. VC for div_qr------0.37------
7. VC for div_qr------0.37------
8. VC for div_qr------------0.03
9. VC for div_qr---1.72---------
10. VC for div_qr------0.100.170.01
11. VC for div_qr---0.13---------
12. VC for div_qr---0.12---------
13. VC for div_qr---0.50---------
14. VC for div_qr------0.080.03---
15. VC for div_qr---0.16---1.47---
16. VC for div_qr------0.044.900.01
17. VC for div_qr---0.11---------
144. precondition------0.03------
145. precondition------0.08------
146. integer overflow------0.10------
147. precondition------0.12------
148. precondition------0.07------
149. postcondition---2.77---------
150. postcondition---------0.06---
151. postcondition---0.11---0.03---
152. postcondition---0.43---------
VC for tdiv_qr---------------
split_goal_wp
  1. integer overflow0.03---------0.03
2. precondition0.04---------0.04
3. integer overflow0.04---------0.03
4. precondition0.05------------
5. precondition0.04---------0.03
6. precondition0.04------------
7. precondition0.03---------0.04
8. precondition0.03---------0.03
9. precondition0.04---------0.02
10. precondition0.05---------0.04
11. precondition0.04---------0.02
12. precondition0.06---------0.16
13. precondition0.05---------0.04
14. precondition0.03---------0.04
15. precondition0.03------------
16. precondition0.05------------
17. postcondition0.03------------
18. postcondition0.04------------