Obligations | Alt-Ergo (2.0.0) | CVC4 (1.5) | Eprover (1.9) | ||
reachable_succ | --- | --- | 0.02 | ||
reachable_trans | --- | --- | --- | ||
induction_pr | |||||
reachable_trans.1 | 0.01 | --- | --- | ||
reachable_trans.2 | 0.01 | --- | --- | ||
wreach_var | --- | --- | --- | ||
induction_pr | |||||
wreach_var.1 | 0.01 | --- | --- | ||
wreach_var.2 | 0.01 | --- | --- | ||
wreach_reachable | --- | --- | --- | ||
split_goal_wp | |||||
wreach_reachable.1 | --- | --- | --- | ||
induction_pr | |||||
wreach_reachable.1.1 | 0.01 | --- | --- | ||
wreach_reachable.1.2 | 0.01 | --- | --- | ||
wreach_reachable.2 | --- | --- | --- | ||
induction_pr | |||||
wreach_reachable.2.1 | 0.01 | --- | --- | ||
wreach_reachable.2.2 | 0.01 | --- | --- | ||
5. VC for random_search | --- | --- | --- | ||
split_goal_wp | |||||
1. postcondition | 0.01 | --- | --- | ||
2. postcondition | 0.01 | --- | --- | ||
3. precondition | 0.01 | --- | --- | ||
4. postcondition | 0.01 | --- | --- | ||
5. postcondition | 0.05 | --- | --- | ||
6. precondition | --- | 0.10 | --- | ||
7. assertion | --- | --- | --- | ||
split_goal_wp | |||||
1. assertion | --- | --- | 1.30 | ||
2. VC for random_search | 0.01 | 0.17 | --- | ||
3. VC for random_search | --- | 0.20 | --- | ||
8. postcondition | 0.01 | --- | --- | ||
9. postcondition | 0.02 | --- | --- | ||
6. VC for random_search_main | --- | --- | --- | ||
split_goal_wp | |||||
1. precondition | 0.01 | --- | 2.41 | ||
2. postcondition | --- | --- | 0.03 |