Why3 Proof Results for Project "dag2"

Theory "dag2.TestAcyclicGraph": fully verified in 0.14 s

ObligationsAlt-Ergo (2.1.0)CVC4 (1.5)Eprover (1.9)Spass (3.5)Z3 (4.6.2)
paths_in---------------
induction_pr
  paths_in.10.010.030.010.030.03
paths_in.20.010.040.030.04Timeout (15s)
2. VC for add_grays0.000.020.010.030.01
3. VC for add_blacks0.000.020.010.030.01
4. VC for dfs---------------
split_goal_wp
  1. postcondition0.010.050.020.040.12
2. postcondition0.010.050.030.040.02
3. postcondition0.010.040.010.030.02
4. exceptional postcondition0.091.42Timeout (15s)Timeout (15s)0.20
5. assertion0.040.070.06Timeout (15s)0.04
6. precondition0.010.050.030.040.03
7. precondition0.030.091.37Timeout (15s)0.03
8. precondition0.110.080.66Timeout (15s)Timeout (15s)
9. preconditionTimeout (15s)0.080.06Timeout (15s)Timeout (15s)
10. postcondition0.110.080.74Timeout (15s)Timeout (15s)
11. postcondition0.040.08Timeout (15s)Timeout (15s)0.04
12. postcondition0.010.040.010.030.03
13. exceptional postcondition0.010.040.010.030.01
14. precondition0.010.050.030.040.03
15. preconditionTimeout (15s)14.90---------
introduce_premises
  1. precondition---------------
inline_goal
  1. precondition---------------
introduce_premises
  1. precondition---------------
inline_goal
  1. preconditionTimeout (15s)14.680.15Timeout (15s)Timeout (15s)
16. precondition0.060.501.66Timeout (15s)Timeout (15s)
17. precondition0.020.070.05Timeout (15s)0.03
18. assertion0.130.20Timeout (15s)Timeout (15s)0.06
19. precondition0.010.050.040.050.03
20. precondition0.100.152.12Timeout (15s)0.04
21. precondition0.790.22Timeout (15s)Timeout (15s)Timeout (15s)
22. preconditionTimeout (15s)1.28Timeout (15s)Timeout (15s)Timeout (15s)
23. postcondition0.330.108.17Timeout (15s)Timeout (15s)
24. postcondition0.080.09Timeout (15s)Timeout (15s)0.04
25. postcondition0.010.040.010.030.03
26. exceptional postcondition0.010.040.010.030.02
27. exceptional postcondition0.010.040.010.030.02
5. VC for is_acyclic---------------
split_goal_wp
  1. precondition0.010.030.010.030.02
2. precondition0.010.040.030.040.03
3. precondition0.020.040.0510.330.17
4. preconditionTimeout (15s)0.080.037.210.03
5. assertion0.010.050.330.070.03
6. assertion0.3214.72Timeout (15s)Timeout (15s)Timeout (15s)
7. postcondition0.010.050.010.030.03
8. postcondition0.010.040.010.030.02