Why3 Proof Results for Project "ricart_abdulla_int_certif"

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_initialisation": fully verified in 4.51 s

ObligationsAlt-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)
initialisation0.18Timeout (30s)0.05Timeout (5s)Timeout (5s)4.450.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_property": fully verified in 0.38 s

ObligationsAlt-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)
property0.03Timeout (5s)0.040.020.260.020.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_1": fully verified in 0.24 s

ObligationsAlt-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.213.210.05Timeout (30s)Timeout (5s)30.030.03

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_2": fully verified in 0.28 s

ObligationsAlt-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_20.060.100.09Timeout (5s)Timeout (5s)0.020.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_3": fully verified in 0.26 s

ObligationsAlt-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_30.060.070.10Timeout (5s)Timeout (5s)0.020.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_4": fully verified in 0.28 s

ObligationsAlt-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_40.040.100.10Timeout (5s)Timeout (5s)0.030.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_5": fully verified in 0.25 s

ObligationsAlt-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_50.040.090.07Timeout (5s)Timeout (5s)0.030.02

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_6": fully verified in 0.25 s

ObligationsAlt-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_60.050.060.11Timeout (5s)Timeout (5s)0.020.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_7": fully verified in 0.40 s

ObligationsAlt-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_70.050.060.090.15Timeout (5s)0.030.02

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_8": fully verified in 5.92 s

ObligationsAlt-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_80.060.050.100.903.771.030.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_9": fully verified in 1.01 s

ObligationsAlt-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_90.060.060.100.78Timeout (5s)4.990.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_10": fully verified in 0.95 s

ObligationsAlt-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_100.050.050.110.11Timeout (5s)0.620.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_11": fully verified in 4.86 s

ObligationsAlt-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_110.050.050.130.133.760.730.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_12": fully verified in 3.40 s

ObligationsAlt-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_120.100.050.143.06Timeout (5s)0.040.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_13": fully verified in 2.96 s

ObligationsAlt-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_130.070.340.131.36Timeout (5s)1.390.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_14": fully verified in 0.77 s

ObligationsAlt-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_140.061.430.110.55Timeout (5s)0.040.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_15": fully verified in 1.88 s

ObligationsAlt-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_150.130.110.12Timeout (5s)Timeout (5s)1.500.02

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_hint_16": fully verified in 0.28 s

ObligationsAlt-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_160.13Timeout (5s)0.14Timeout (5s)Timeout (5s)5.000.01

Theory "ricart_abdulla_int_certif.Ricart_abdulla_int_preservation": fully verified in 0.38 s

ObligationsAlt-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)
preservation0.040.020.010.030.260.020.00