Why3 Proof Results for Project "bakery_certif"
Theory "bakery_certif.Bakery_initialisation": fully verified in 1.39 s
| Obligations | Alt-Ergo (0.99 nb1noE) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) | iProver (1.0) |
initialisation | 0.01 | 0.02 | 0.03 | 0.01 | 0.03 | 0.00 | 0.03 | 1.26 |
Theory "bakery_certif.Bakery_property": fully verified in 0.08 s
| Obligations | Alt-Ergo (0.99 nb1noE) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) | iProver (1.0) |
property | 0.00 | 0.00 | 0.01 | 0.01 | 0.03 | 0.00 | 0.00 | 0.03 |
Theory "bakery_certif.Bakery_hint_1": fully verified in 0.29 s
| Obligations | Alt-Ergo (0.99 nb1noE) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) | iProver (1.0) |
hint_1 | 0.04 | 0.04 | 0.04 | Timeout (5s) | 0.16 | 5.01 | 0.01 | Timeout (5s) |
Theory "bakery_certif.Bakery_hint_2": fully verified in 1.88 s
| Obligations | Alt-Ergo (0.99 nb1noE) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) | iProver (1.0) |
hint_2 | 0.05 | 0.07 | 0.07 | 1.50 | 0.18 | 5.00 | 0.01 | Timeout (5s) |
Theory "bakery_certif.Bakery_preservation": fully verified in 0.07 s
| Obligations | Alt-Ergo (0.99 nb1noE) | CVC3 (2.4.1) | CVC4 (1.4) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) | iProver (1.0) |
preservation | 0.00 | 0.00 | 0.00 | 0.01 | 0.03 | 0.00 | 0.00 | 0.03 |