Why3 Proof Results for Project "rs1"

Theory "rs1.RandomSearch": fully verified in 2.12 s

ObligationsAlt-Ergo (2.0.0)CVC4 (1.5)Eprover (1.9)
path_decomp_with_last_occTimeout (15s)------
induction_pr
  path_decomp_with_last_occ.10.01------
path_decomp_with_last_occ.2Timeout (15s)14.780.77
whitepath_decomp_with_last_occ2.12------
whitepath_enhanceTimeout (15s)15.10Timeout (15s)
introduce_premises
  whitepath_enhance.1---------
inline_goal
  whitepath_enhance.1.11.62------
4. VC for random_search---------
split_goal_wp
  1. postcondition0.01------
2. postcondition0.01------
3. precondition0.01------
4. precondition0.01------
5. postcondition0.01------
6. postcondition0.07------
7. precondition0.09------
8. precondition0.01------
9. assertion2.61------
10. postcondition0.01------
11. postcondition2.51------
5. VC for random_search_main---------
split_goal_wp
  1. precondition0.01------
2. precondition0.01------
3. postconditionTimeout (15s)15.110.17