Why3 Proof Results for Project "ricart_abdulla_int_certif"
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_initialisation": fully verified in 4.51 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
initialisation | 0.18 | Timeout (30s) | 0.05 | Timeout (5s) | Timeout (5s) | 4.45 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_property": fully verified in 0.38 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
property | 0.03 | Timeout (5s) | 0.04 | 0.02 | 0.26 | 0.02 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_1": fully verified in 0.24 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_1 | 0.21 | 3.21 | 0.05 | Timeout (30s) | Timeout (5s) | 30.03 | 0.03 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_2": fully verified in 0.28 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_2 | 0.06 | 0.10 | 0.09 | Timeout (5s) | Timeout (5s) | 0.02 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_3": fully verified in 0.26 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_3 | 0.06 | 0.07 | 0.10 | Timeout (5s) | Timeout (5s) | 0.02 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_4": fully verified in 0.28 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_4 | 0.04 | 0.10 | 0.10 | Timeout (5s) | Timeout (5s) | 0.03 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_5": fully verified in 0.25 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_5 | 0.04 | 0.09 | 0.07 | Timeout (5s) | Timeout (5s) | 0.03 | 0.02 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_6": fully verified in 0.25 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_6 | 0.05 | 0.06 | 0.11 | Timeout (5s) | Timeout (5s) | 0.02 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_7": fully verified in 0.40 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_7 | 0.05 | 0.06 | 0.09 | 0.15 | Timeout (5s) | 0.03 | 0.02 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_8": fully verified in 5.92 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_8 | 0.06 | 0.05 | 0.10 | 0.90 | 3.77 | 1.03 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_9": fully verified in 1.01 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_9 | 0.06 | 0.06 | 0.10 | 0.78 | Timeout (5s) | 4.99 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_10": fully verified in 0.95 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_10 | 0.05 | 0.05 | 0.11 | 0.11 | Timeout (5s) | 0.62 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_11": fully verified in 4.86 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_11 | 0.05 | 0.05 | 0.13 | 0.13 | 3.76 | 0.73 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_12": fully verified in 3.40 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_12 | 0.10 | 0.05 | 0.14 | 3.06 | Timeout (5s) | 0.04 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_13": fully verified in 2.96 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_13 | 0.07 | 0.34 | 0.13 | 1.36 | Timeout (5s) | 1.39 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_14": fully verified in 0.77 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_14 | 0.06 | 1.43 | 0.11 | 0.55 | Timeout (5s) | 0.04 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_15": fully verified in 1.88 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_15 | 0.13 | 0.11 | 0.12 | Timeout (5s) | Timeout (5s) | 1.50 | 0.02 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_16": fully verified in 0.28 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
hint_16 | 0.13 | Timeout (5s) | 0.14 | Timeout (5s) | Timeout (5s) | 5.00 | 0.01 |
Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_preservation": fully verified in 0.38 s
Obligations | Alt-Ergo (0.96) | CVC3 (2.4.1) | CVC4 (1.3) | Eprover (1.8-001) | Spass (3.5) | Yices (1.0.40) | Z3 (4.3.2) |
preservation | 0.04 | 0.02 | 0.01 | 0.03 | 0.26 | 0.02 | 0.00 |