Why3 Proof Results for Project "matrices_ring_simp"

Theory "matrices_ring_simp.Symb": fully verified in 9.81 s

ObligationsAlt-Ergo (1.01)CVC4 (1.4)
VC for l_mdl_ok0.03---
VC for m_mdl_ok0.03---
VC for lm_mdl_ok0.04---
VC for lm_mdl_same0.08---
VC for l_compare_zero0.03---
VC for m_collapse_ok------
split_goal_wp
  1. postcondition---0.05
2. postcondition---0.06
3. precondition0.01---
4. assertion0.16---
5. postcondition0.39---
6. postcondition---0.08
7. postcondition2.87---
8. postcondition---0.06
VC for lm_collapse_ok0.09---
VC for cat_rev_ok0.09---
VC for lm_dump_ok0.16---
VC for lm_merge_ok------
split_goal_wp
  1. precondition0.02---
2. precondition0.02---
3. precondition0.02---
4. precondition0.02---
5. postcondition0.02---
6. postcondition0.28---
7. precondition0.02---
8. precondition0.02---
9. precondition0.03---
10. precondition0.03---
11. variant decrease0.03---
12. precondition0.02---
13. precondition0.03---
14. postcondition0.02---
15. postcondition---1.87
VC for cat_ok0.12---
VC for m_mul_ok0.11---
VC for m_distribute_ok0.08---
VC for lm_distribute_ok0.19---
VC for lm_opp_ok------
split_goal_wp
  1. postcondition0.02---
2. postcondition0.03---
3. variant decrease0.03---
4. precondition0.03---
5. precondition0.03---
6. precondition0.04---
7. postcondition0.03---
8. postcondition---0.13
extends_rw0.02---
VC for symb_env0.02---
VC for symb_reg0.07---
VC for symb_opp0.03---
VC for symb_add0.10---
VC for symb_sub0.04---
VC for symb_mul0.03---
VC for harness------
split_goal_wp
  1. precondition------
compute_specified
  1. precondition------
simplify_trivial_quantification_in_goal
  1. precondition------
compute_specified
  1. precondition------
introduce_premises
  1. precondition0.03---
2. precondition0.06---
3. precondition------
compute_specified
  1. precondition------
simplify_trivial_quantification_in_goal
  1. precondition------
compute_specified
  1. precondition------
introduce_premises
  1. precondition0.02---
4. precondition0.07---
5. precondition0.04---
6. precondition0.06---
7. precondition------
compute_specified
  1. precondition------
simplify_trivial_quantification_in_goal
  1. precondition------
compute_specified
  1. precondition------
introduce_premises
  1. precondition0.02---
8. precondition0.07---
9. precondition0.06---
10. precondition0.05---
11. precondition------
compute_specified
  1. precondition------
simplify_trivial_quantification_in_goal
  1. precondition------
compute_specified
  1. precondition------
introduce_premises
  1. precondition0.02---
12. precondition0.10---
13. precondition0.05---
14. precondition0.05---
15. precondition0.06---
16. precondition0.06---
17. precondition0.06---
18. precondition0.07---
19. precondition0.07---
20. precondition0.06---
21. precondition0.07---
22. precondition0.07---
23. precondition0.07---
24. precondition0.07---
25. precondition0.08---
26. precondition0.07---
27. precondition0.07---
28. precondition0.08---
29. precondition0.08---
30. precondition0.08---
31. precondition0.09---
32. precondition0.07---
33. assertion------
compute_specified
  1. assertion------
simplify_trivial_quantification_in_goal
  1. assertion------
compute_specified