Why3 Proof Results for Project "rs1"

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

Obligations		Alt-Ergo (2.1.0)	CVC4 (1.5)	Eprover (1.9)
path_lst_occ		---	---	---
induction_pr
	path_lst_occ.1	0.01	---	---
	path_lst_occ.2	---	---	0.03
path_inv		0.01	---	---
whitepath_suffix		0.02	---	---
whitepath_inv		---	2.66	---
whitepath_split_lst_occ		---	0.30	---
6. VC for random_search		---	---	---
split_goal_wp
	1. postcondition	0.01	---	---
	2. postcondition	0.01	---	---
	3. precondition	0.01	---	---
	4. precondition	0.01	---	---
	5. postcondition	0.01	---	---
	6. postcondition	0.07	---	---
	7. precondition	0.09	---	---
	8. precondition	0.01	---	---
	9. assertion	0.06	---	---
	10. postcondition	0.01	---	---
	11. postcondition	0.10	---	---
7. VC for random_search_main		---	---	---
split_goal_wp
	1. precondition	0.01	---	---
	2. precondition	0.01	---	---
	3. postcondition	---	---	0.17