Why3 Proof Results for Project "flash_nodata_certif"

Theory "flash_nodata_certif.Flash_nodata_initialisation": fully verified in 0.27 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)
initialisation4.93Timeout (30s)0.040.030.160.020.02

Theory "flash_nodata_certif.Flash_nodata_property": fully verified in 0.87 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.430.050.070.030.260.030.00

Theory "flash_nodata_certif.Flash_nodata_hint_1": fully verified in 5.07 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_1Timeout (30s)5.00Timeout (30s)Timeout (30s)Timeout (30s)2.100.07

Theory "flash_nodata_certif.Flash_nodata_hint_2": fully verified in 9.82 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_2Timeout (5s)9.76Timeout (30s)Timeout (5s)Timeout (5s)2.200.06

Theory "flash_nodata_certif.Flash_nodata_hint_3": fully verified in 2.36 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_3Timeout (30s)1.880.27Timeout (5s)Timeout (5s)0.170.04

Theory "flash_nodata_certif.Flash_nodata_hint_4": fully verified in 2.31 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_4Timeout (5s)1.780.31Timeout (5s)Timeout (5s)0.170.05

Theory "flash_nodata_certif.Flash_nodata_hint_5": fully verified in 2.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)
hint_5Timeout (5s)1.830.27Timeout (5s)Timeout (5s)0.210.07

Theory "flash_nodata_certif.Flash_nodata_hint_6": fully verified in 2.49 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_6Timeout (5s)1.970.26Timeout (5s)Timeout (5s)0.220.04

Theory "flash_nodata_certif.Flash_nodata_hint_7": fully verified in 2.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_7Timeout (5s)1.680.27Timeout (5s)Timeout (5s)0.250.04

Theory "flash_nodata_certif.Flash_nodata_hint_8": fully verified in 2.35 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_8Timeout (5s)1.800.32Timeout (5s)Timeout (5s)0.180.05

Theory "flash_nodata_certif.Flash_nodata_hint_9": fully verified in 2.13 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_9Timeout (5s)1.560.29Timeout (5s)Timeout (5s)0.230.05

Theory "flash_nodata_certif.Flash_nodata_hint_10": fully verified in 2.03 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_10Timeout (5s)1.560.22Timeout (5s)Timeout (5s)0.210.04

Theory "flash_nodata_certif.Flash_nodata_hint_11": fully verified in 2.30 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_11Timeout (5s)1.760.29Timeout (5s)Timeout (5s)0.190.06

Theory "flash_nodata_certif.Flash_nodata_hint_12": fully verified in 2.15 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_12Timeout (5s)1.670.25Timeout (5s)Timeout (5s)0.190.04

Theory "flash_nodata_certif.Flash_nodata_hint_13": fully verified in 2.23 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_13Timeout (5s)1.700.28Timeout (5s)Timeout (5s)0.200.05

Theory "flash_nodata_certif.Flash_nodata_hint_14": fully verified in 7.19 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_14Timeout (5s)3.893.23Timeout (5s)Timeout (5s)5.020.07

Theory "flash_nodata_certif.Flash_nodata_hint_15": fully verified in 9.18 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_15Timeout (5s)2.726.39Timeout (5s)Timeout (5s)5.020.07

Theory "flash_nodata_certif.Flash_nodata_hint_16": fully verified in 2.41 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_16Timeout (5s)1.850.29Timeout (5s)Timeout (5s)0.220.05

Theory "flash_nodata_certif.Flash_nodata_hint_17": fully verified in 2.42 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_17Timeout (5s)1.820.29Timeout (5s)Timeout (5s)0.250.06

Theory "flash_nodata_certif.Flash_nodata_hint_18": fully verified in 2.05 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_18Timeout (5s)1.530.28Timeout (5s)Timeout (5s)0.200.04

Theory "flash_nodata_certif.Flash_nodata_hint_19": fully verified in 2.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)
hint_19Timeout (5s)1.790.30Timeout (5s)Timeout (5s)0.250.04

Theory "flash_nodata_certif.Flash_nodata_hint_20": fully verified in 2.45 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_20Timeout (5s)1.950.25Timeout (5s)Timeout (5s)0.190.06

Theory "flash_nodata_certif.Flash_nodata_hint_21": fully verified in 2.20 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_21Timeout (5s)1.750.24Timeout (5s)Timeout (5s)0.170.04

Theory "flash_nodata_certif.Flash_nodata_hint_22": fully verified in 6.15 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_22Timeout (5s)3.152.94Timeout (5s)Timeout (5s)5.020.06

Theory "flash_nodata_certif.Flash_nodata_hint_23": fully verified in 7.09 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_23Timeout (5s)2.934.11Timeout (5s)Timeout (5s)5.020.05

Theory "flash_nodata_certif.Flash_nodata_hint_24": fully verified in 4.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_24Timeout (5s)2.442.38Timeout (5s)Timeout (5s)5.020.06

Theory "flash_nodata_certif.Flash_nodata_hint_25": fully verified in 4.75 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_25Timeout (5s)2.092.60Timeout (5s)Timeout (5s)5.010.06

Theory "flash_nodata_certif.Flash_nodata_hint_26": fully verified in 2.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_26Timeout (5s)1.810.25Timeout (5s)Timeout (5s)0.140.05

Theory "flash_nodata_certif.Flash_nodata_hint_27": fully verified in 4.56 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_27Timeout (5s)2.192.32Timeout (5s)Timeout (5s)5.010.05

Theory "flash_nodata_certif.Flash_nodata_hint_28": fully verified in 1.54 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_28Timeout (5s)1.130.22Timeout (5s)Timeout (5s)0.170.02

Theory "flash_nodata_certif.Flash_nodata_hint_29": fully verified in 6.84 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_29Timeout (5s)2.072.47Timeout (5s)Timeout (5s)2.240.06

Theory "flash_nodata_certif.Flash_nodata_hint_30": fully verified in 6.68 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_30Timeout (5s)6.62Timeout (30s)Timeout (5s)Timeout (5s)5.040.06

Theory "flash_nodata_certif.Flash_nodata_hint_31": fully verified in 5.12 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_31Timeout (5s)3.072.00Timeout (5s)Timeout (5s)5.030.05

Theory "flash_nodata_certif.Flash_nodata_hint_32": fully verified in 6.50 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_32Timeout (5s)2.191.83Timeout (5s)Timeout (5s)2.430.05

Theory "flash_nodata_certif.Flash_nodata_hint_33": fully verified in 3.48 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_33Timeout (5s)3.42Timeout (5s)Timeout (5s)Timeout (5s)5.010.06

Theory "flash_nodata_certif.Flash_nodata_hint_34": fully verified in 4.58 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_34Timeout (5s)2.232.30Timeout (5s)Timeout (5s)5.000.05

Theory "flash_nodata_certif.Flash_nodata_hint_35": fully verified in 7.53 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_35Timeout (5s)3.324.15Timeout (5s)Timeout (5s)5.000.06

Theory "flash_nodata_certif.Flash_nodata_hint_36": fully verified in 4.66 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_36Timeout (5s)2.032.58Timeout (5s)Timeout (5s)5.000.05

Theory "flash_nodata_certif.Flash_nodata_hint_37": fully verified in 7.50 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_37Timeout (5s)2.894.56Timeout (5s)Timeout (5s)5.010.05

Theory "flash_nodata_certif.Flash_nodata_hint_38": fully verified in 2.21 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_38Timeout (5s)1.630.27Timeout (5s)Timeout (5s)0.260.05

Theory "flash_nodata_certif.Flash_nodata_hint_39": fully verified in 2.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_39Timeout (5s)1.630.30Timeout (5s)Timeout (5s)0.260.05

Theory "flash_nodata_certif.Flash_nodata_hint_40": fully verified in 2.27 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_40Timeout (5s)1.710.26Timeout (5s)Timeout (5s)0.250.05

Theory "flash_nodata_certif.Flash_nodata_hint_41": fully verified in 2.17 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_41Timeout (5s)1.600.31Timeout (5s)Timeout (5s)0.200.06

Theory "flash_nodata_certif.Flash_nodata_preservation": fully verified in 1.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)
preservationTimeout (5s)0.260.210.59Timeout (5s)0.200.02