Why3 Proof Results for Project "rs2"

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

Obligations			Alt-Ergo (1.01)	Alt-Ergo (2.0.0)	CVC4 (1.5)	Eprover (1.9)
whitepath_id			---	0.02	---	---
whitepath_covar			---	0.01	---	---
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. assertion		---	---	---	---
	split_goal_wp
		1. assertion	---	---	---	1.22
		2. VC for random_search	---	---	0.16	---
		3. VC for random_search	---	---	0.08	0.39
	10. postcondition		---	0.10	---	---
5. VC for random_search_main			Timeout (5s) (obsolete)	---	---	0.12