Why3 Proof Results for Project "rs2"

Theory "rs2.RandomSearch": fully verified in 0.19 s

ObligationsAlt-Ergo (1.01)Alt-Ergo (2.0.0)CVC4 (1.4)CVC4 (1.5)Eprover (1.8-001)Eprover (1.9)Simplify (1.5.7 alt)Z3 (4.4.0)
whitepath_id---0.02------------------
whitepath_sub---0.02------------------
whitepath_cons---0.03------------------
4. VC for random_search------------------------
split_goal_wp
  1. postcondition---0.02------------------
2. variant decrease---0.02------------------
3. precondition---0.02------------------
4. precondition---0.02------------------
5. postcondition---0.04------------------
6. variant decrease---0.03------------------
7. precondition---0.10------------------
8. precondition---0.03------------------
9. assertionTimeout (1s) (obsolete)---Timeout (1s) (obsolete)1.94 (obsolete)Timeout (1s) (obsolete)---Timeout (5s) (obsolete)Timeout (1s) (obsolete)
split_goal_wp
  1. assertionTimeout (1s) (obsolete)---Timeout (1s) (obsolete)4.96 (obsolete)---1.28---Timeout (1s) (obsolete)
2. VC for random_search---------0.16------------
3. VC for random_search---------0.08------------
10. postcondition---0.10------------------
5. VC for random_search_mainTimeout (5s) (obsolete)------------0.12------