Why3 Proof Results for Project "flash_nodata_certif"
Theory "flash_nodata_certif.Flash_nodata_initialisation": fully verified in 0.27 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 | 4.93 | Timeout (30s) | 0.04 | 0.03 | 0.16 | 0.02 | 0.02 |
Theory "flash_nodata_certif.Flash_nodata_property": fully verified in 0.87 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.43 | 0.05 | 0.07 | 0.03 | 0.26 | 0.03 | 0.00 |
Theory "flash_nodata_certif.Flash_nodata_hint_1": fully verified in 5.07 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 | Timeout (30s) | 5.00 | Timeout (30s) | Timeout (30s) | Timeout (30s) | 2.10 | 0.07 |
Theory "flash_nodata_certif.Flash_nodata_hint_2": fully verified in 9.82 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 | Timeout (5s) | 9.76 | Timeout (30s) | Timeout (5s) | Timeout (5s) | 2.20 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_3": fully verified in 2.36 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 | Timeout (30s) | 1.88 | 0.27 | Timeout (5s) | Timeout (5s) | 0.17 | 0.04 |
Theory "flash_nodata_certif.Flash_nodata_hint_4": fully verified in 2.31 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 | Timeout (5s) | 1.78 | 0.31 | Timeout (5s) | Timeout (5s) | 0.17 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_5": fully verified in 2.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) |
hint_5 | Timeout (5s) | 1.83 | 0.27 | Timeout (5s) | Timeout (5s) | 0.21 | 0.07 |
Theory "flash_nodata_certif.Flash_nodata_hint_6": fully verified in 2.49 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 | Timeout (5s) | 1.97 | 0.26 | Timeout (5s) | Timeout (5s) | 0.22 | 0.04 |
Theory "flash_nodata_certif.Flash_nodata_hint_7": fully verified in 2.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_7 | Timeout (5s) | 1.68 | 0.27 | Timeout (5s) | Timeout (5s) | 0.25 | 0.04 |
Theory "flash_nodata_certif.Flash_nodata_hint_8": fully verified in 2.35 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 | Timeout (5s) | 1.80 | 0.32 | Timeout (5s) | Timeout (5s) | 0.18 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_9": fully verified in 2.13 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 | Timeout (5s) | 1.56 | 0.29 | Timeout (5s) | Timeout (5s) | 0.23 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_10": fully verified in 2.03 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 | Timeout (5s) | 1.56 | 0.22 | Timeout (5s) | Timeout (5s) | 0.21 | 0.04 |
Theory "flash_nodata_certif.Flash_nodata_hint_11": fully verified in 2.30 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 | Timeout (5s) | 1.76 | 0.29 | Timeout (5s) | Timeout (5s) | 0.19 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_12": fully verified in 2.15 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 | Timeout (5s) | 1.67 | 0.25 | Timeout (5s) | Timeout (5s) | 0.19 | 0.04 |
Theory "flash_nodata_certif.Flash_nodata_hint_13": fully verified in 2.23 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 | Timeout (5s) | 1.70 | 0.28 | Timeout (5s) | Timeout (5s) | 0.20 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_14": fully verified in 7.19 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 | Timeout (5s) | 3.89 | 3.23 | Timeout (5s) | Timeout (5s) | 5.02 | 0.07 |
Theory "flash_nodata_certif.Flash_nodata_hint_15": fully verified in 9.18 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 | Timeout (5s) | 2.72 | 6.39 | Timeout (5s) | Timeout (5s) | 5.02 | 0.07 |
Theory "flash_nodata_certif.Flash_nodata_hint_16": fully verified in 2.41 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 | Timeout (5s) | 1.85 | 0.29 | Timeout (5s) | Timeout (5s) | 0.22 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_17": fully verified in 2.42 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_17 | Timeout (5s) | 1.82 | 0.29 | Timeout (5s) | Timeout (5s) | 0.25 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_18": fully verified in 2.05 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_18 | Timeout (5s) | 1.53 | 0.28 | Timeout (5s) | Timeout (5s) | 0.20 | 0.04 |
Theory "flash_nodata_certif.Flash_nodata_hint_19": fully verified in 2.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) |
hint_19 | Timeout (5s) | 1.79 | 0.30 | Timeout (5s) | Timeout (5s) | 0.25 | 0.04 |
Theory "flash_nodata_certif.Flash_nodata_hint_20": fully verified in 2.45 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_20 | Timeout (5s) | 1.95 | 0.25 | Timeout (5s) | Timeout (5s) | 0.19 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_21": fully verified in 2.20 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_21 | Timeout (5s) | 1.75 | 0.24 | Timeout (5s) | Timeout (5s) | 0.17 | 0.04 |
Theory "flash_nodata_certif.Flash_nodata_hint_22": fully verified in 6.15 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_22 | Timeout (5s) | 3.15 | 2.94 | Timeout (5s) | Timeout (5s) | 5.02 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_23": fully verified in 7.09 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_23 | Timeout (5s) | 2.93 | 4.11 | Timeout (5s) | Timeout (5s) | 5.02 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_24": fully verified in 4.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_24 | Timeout (5s) | 2.44 | 2.38 | Timeout (5s) | Timeout (5s) | 5.02 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_25": fully verified in 4.75 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_25 | Timeout (5s) | 2.09 | 2.60 | Timeout (5s) | Timeout (5s) | 5.01 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_26": fully verified in 2.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_26 | Timeout (5s) | 1.81 | 0.25 | Timeout (5s) | Timeout (5s) | 0.14 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_27": fully verified in 4.56 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_27 | Timeout (5s) | 2.19 | 2.32 | Timeout (5s) | Timeout (5s) | 5.01 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_28": fully verified in 1.54 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_28 | Timeout (5s) | 1.13 | 0.22 | Timeout (5s) | Timeout (5s) | 0.17 | 0.02 |
Theory "flash_nodata_certif.Flash_nodata_hint_29": fully verified in 6.84 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_29 | Timeout (5s) | 2.07 | 2.47 | Timeout (5s) | Timeout (5s) | 2.24 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_30": fully verified in 6.68 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_30 | Timeout (5s) | 6.62 | Timeout (30s) | Timeout (5s) | Timeout (5s) | 5.04 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_31": fully verified in 5.12 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_31 | Timeout (5s) | 3.07 | 2.00 | Timeout (5s) | Timeout (5s) | 5.03 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_32": fully verified in 6.50 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_32 | Timeout (5s) | 2.19 | 1.83 | Timeout (5s) | Timeout (5s) | 2.43 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_33": fully verified in 3.48 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_33 | Timeout (5s) | 3.42 | Timeout (5s) | Timeout (5s) | Timeout (5s) | 5.01 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_34": fully verified in 4.58 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_34 | Timeout (5s) | 2.23 | 2.30 | Timeout (5s) | Timeout (5s) | 5.00 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_35": fully verified in 7.53 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_35 | Timeout (5s) | 3.32 | 4.15 | Timeout (5s) | Timeout (5s) | 5.00 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_hint_36": fully verified in 4.66 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_36 | Timeout (5s) | 2.03 | 2.58 | Timeout (5s) | Timeout (5s) | 5.00 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_37": fully verified in 7.50 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_37 | Timeout (5s) | 2.89 | 4.56 | Timeout (5s) | Timeout (5s) | 5.01 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_38": fully verified in 2.21 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_38 | Timeout (5s) | 1.63 | 0.27 | Timeout (5s) | Timeout (5s) | 0.26 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_39": fully verified in 2.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_39 | Timeout (5s) | 1.63 | 0.30 | Timeout (5s) | Timeout (5s) | 0.26 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_40": fully verified in 2.27 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_40 | Timeout (5s) | 1.71 | 0.26 | Timeout (5s) | Timeout (5s) | 0.25 | 0.05 |
Theory "flash_nodata_certif.Flash_nodata_hint_41": fully verified in 2.17 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_41 | Timeout (5s) | 1.60 | 0.31 | Timeout (5s) | Timeout (5s) | 0.20 | 0.06 |
Theory "flash_nodata_certif.Flash_nodata_preservation": fully verified in 1.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) |
preservation | Timeout (5s) | 0.26 | 0.21 | 0.59 | Timeout (5s) | 0.20 | 0.02 |