Why3 Proof Results for Project "rs3"

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

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