Why3 Proof Results for Project "rs3"

Theory "rs3.Dfs_nbtw": fully verified in 0.02 s

ObligationsAlt-Ergo (2.0.0)CVC4 (1.5)Eprover (1.9)Z3 (4.4.0)
reachable_succTimeout (15s) (obsolete)---0.02---
reachable_trans------Timeout (15s) (obsolete)---
induction_pr
  reachable_trans.10.01---------
reachable_trans.20.01---------
d_reach_monotony_rTimeout (15s) (obsolete)15.51 (obsolete)------
induction_pr
  d_reach_monotony_r.10.01---------
d_reach_monotony_r.20.01---------
d_reach_reachable------------
split_goal_wp
  d_reach_reachable.1------------
induction_pr
  d_reach_reachable.1.10.01---------
d_reach_reachable.1.20.01---------
d_reach_reachable.2------------
induction_pr
  d_reach_reachable.2.10.01---------
d_reach_reachable.2.20.01---------
5. VC for random_search------------
split_goal_wp
  1. postcondition0.01---------
2. postcondition0.01---------
3. precondition0.01---------
4. postcondition0.01---------
5. postcondition0.05---------
6. preconditionTimeout (15s) (obsolete)0.10------
7. assertionTimeout (15s) (obsolete)Timeout (15s) (obsolete)Timeout (15s) (obsolete)Timeout (15s) (obsolete)
split_goal_wp
  1. assertionTimeout (15s) (obsolete)14.87 (obsolete)0.06---
2. VC for random_search0.010.17------
3. VC for random_searchTimeout (15s) (obsolete)0.20------
8. postcondition0.01---------
9. postcondition0.0244.70 (obsolete)Timeout (45s) (obsolete)---
6. VC for random_search_main------------
split_goal_wp
  1. precondition0.01---2.41---
2. postconditionTimeout (15s) (obsolete)---0.03---