# . * SAT 0 * UNSAT 44 * TIMEOUT 73 * UNKNOWN 0 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/AUFBVFPDTNIRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-AUFBVFPDTNIRA.tar.
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 4a90d3105054796562079406e125b9480ac3472b
Z3 branch: master
Z3 options: "-T:20 model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/AUFBVFPDTNIRA.tar.zst?download=1
Z3 commit message: Update tptp_frontend.cpp
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_22_53_unreachable_branch___00.smt2 | 0.025s | 20.196MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_13_19_precondition___00.smt2 | 0.025s | 20.104MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_26_36_loop_invariant_init___00.smt2 | 0.025s | 20.076MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_16_28_assert___00.smt2 | 0.027s | 20.296MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_45_85_range_check___00.smt2 | 0.028s | 20.332MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_19_61_range_check___00.smt2 | 0.029s | 19.856MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_9_23_precondition___00.smt2 | 0.030s | 20.368MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_25_22_unreachable_branch___00.smt2 | 0.036s | 20.14MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-026__overlayed_objects__p2.ads_27_22_postcondition___00.smt2 | 0.037s | 20.344MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_52_25_assert___00.smt2 | 0.039s | 21.288MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_14_4_precondition___00.smt2 | 0.053s | 19.896MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-024__flow_crash__p.ads_27_22_postcondition___00.smt2 | 0.054s | 20.368MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_15_23_precondition___00.smt2 | 0.054s | 20.132MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_26_36_loop_invariant_preserv___00.smt2 | 0.056s | 19.864MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_10_4_precondition___00.smt2 | 0.057s | 20.384MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_11_19_precondition___00.smt2 | 0.059s | 19.892MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_24_61_range_check___00.smt2 | 0.060s | 20.028MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_24_18_unreachable_branch___00.smt2 | 0.060s | 19.86MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_62_14_postcondition___00.smt2 | 0.060s | 20.1MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_12_27_range_check___00.smt2 | 0.060s | 19.848MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_73_78_range_check___00.smt2 | 0.061s | 20.12MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_12_4_precondition___00.smt2 | 0.063s | 19.74MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_18_50_range_check___00.smt2 | 0.063s | 20.096MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_58_25_assert___00.smt2 | 0.063s | 21.604MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_22_18_unreachable_branch___00.smt2 | 0.063s | 20.376MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_40_85_range_check___00.smt2 | 0.064s | 19.908MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_68_78_range_check___00.smt2 | 0.064s | 19.708MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_39_73_range_check___00.smt2 | 0.066s | 21.672MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_49_31_range_check___00.smt2 | 0.067s | 21.412MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/P816-010__prefix_inline__generic_queue.ads_73_32_some_package.adb_8_4_range_check___00.smt2 | 0.067s | 21.024MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_23_9_disjoint_contract_cases___00.smt2 | 0.067s | 20.9MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/P816-010__prefix_inline__generic_queue.ads_46_32_some_package.adb_8_4_range_check___00.smt2 | 0.068s | 21.188MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_38_22_assert___00.smt2 | 0.069s | 20.788MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/P816-010__prefix_inline__generic_queue.ads_65_32_some_package.adb_8_4_range_check___00.smt2 | 0.070s | 21.16MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_50_25_assert___00.smt2 | 0.073s | 21.132MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_51_30_unreachable_branch___00.smt2 | 0.073s | 21.112MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_37_76_range_check___00.smt2 | 0.074s | 20.884MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_18_16_loop_invariant_init___00.smt2 | 0.074s | 21.148MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_25_64_contract_case___00.smt2 | 0.075s | 21.64MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_54_25_assert___00.smt2 | 0.076s | 21.796MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_67_66_range_check___00.smt2 | 0.079s | 21.636MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_18_16_loop_invariant_preserv___00.smt2 | 0.083s | 21.924MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_34_19_contract_case___00.smt2 | 0.087s | 21.632MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_29_80_contract_case___00.smt2 | 0.090s | 21.916MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_61_14_inconsistent_pre___00.smt2 | 20.011s | 24.488MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_71_65_unreachable_branch___00.smt2 | 20.012s | 30.84MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_41_21_unreachable_branch___00.smt2 | 20.012s | 25.064MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_74_34_unreachable_branch___00.smt2 | 20.013s | 26.252MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_42_35_range_check___00.smt2 | 20.013s | 32.34MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_71_30_unreachable_branch___00.smt2 | 20.013s | 24.724MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_40_27_unreachable_branch___00.smt2 | 20.013s | 31.14MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_53_30_unreachable_branch___00.smt2 | 20.013s | 30.872MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_9_19_assert___00.smt2 | 20.014s | 30.6MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_39_14_unreachable_branch___00.smt2 | 20.014s | 35.78MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_43_52_unreachable_branch___00.smt2 | 20.015s | 26.692MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_58_17_unreachable_branch___00.smt2 | 20.015s | 25.892MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_35_14_unreachable_branch___00.smt2 | 20.018s | 25.324MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_39_52_unreachable_branch___00.smt2 | 20.021s | 26.04MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_76_25_assert___00.smt2 | 20.022s | 26.188MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_41_22_assert___00.smt2 | 20.022s | 24.384MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-026__overlayed_objects__p.adb_31_28_overflow_check___00.smt2 | 20.022s | 24.248MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.ads_50_9_postcondition___00.smt2 | 20.023s | 32.004MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_56_14_postcondition___00.smt2 | 20.023s | 30.892MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_7_7_precondition___00.smt2 | 20.024s | 27.572MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_46_31_range_check___00.smt2 | 20.026s | 32.144MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_43_17_unreachable_branch___00.smt2 | 20.038s | 25.892MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_26_14_unreachable_branch___00.smt2 | 20.039s | 23.9MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_11_16_dead_code___00.smt2 | 20.039s | 26.06MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_78_10_dead_code___00.smt2 | 20.040s | 31.016MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_15_19_assert___00.smt2 | 20.040s | 24.396MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_45_27_range_check___00.smt2 | 20.041s | 32.148MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_63_17_unreachable_branch___00.smt2 | 20.041s | 24.324MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_49_10_dead_code___00.smt2 | 20.041s | 30.848MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_42_28_unreachable_branch___00.smt2 | 20.042s | 31.08MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-026__overlayed_objects__p2.adb_40_28_fp_overflow_check___00.smt2 | 20.044s | 29.268MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_20_22_unreachable_branch___00.smt2 | 20.046s | 24.264MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_13_19_assert___00.smt2 | 20.046s | 26.68MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_38_61_range_check___00.smt2 | 20.047s | 32.164MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_29_39_unreachable_branch___00.smt2 | 20.047s | 25.16MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_40_17_unreachable_branch___00.smt2 | 20.047s | 23.856MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_30_14_unreachable_branch___00.smt2 | 20.047s | 24.832MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_43_27_unreachable_branch___00.smt2 | 20.048s | 24.448MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_63_62_unreachable_branch___00.smt2 | 20.048s | 24.4MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_67_27_unreachable_branch___00.smt2 | 20.049s | 31.46MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.ads_50_55_range_check___00.smt2 | 20.049s | 32.024MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_61_28_unreachable_branch___00.smt2 | 20.049s | 31.94MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_11_19_assert___00.smt2 | 20.049s | 24.948MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_73_30_unreachable_branch___00.smt2 | 20.050s | 31.0MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_28_17_dead_code___00.smt2 | 20.050s | 25.072MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-026__overlayed_objects__p2.adb_39_28_overflow_check___00.smt2 | 20.050s | 24.152MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_37_14_unreachable_branch___00.smt2 | 20.050s | 25.456MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_69_34_unreachable_branch___00.smt2 | 20.051s | 29.584MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_42_59_unreachable_branch___00.smt2 | 20.051s | 24.308MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_57_28_unreachable_branch___00.smt2 | 20.051s | 31.852MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_59_54_unreachable_branch___00.smt2 | 20.052s | 24.204MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_65_27_unreachable_branch___00.smt2 | 20.052s | 30.788MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_55_13_inconsistent_pre___00.smt2 | 20.052s | 29.308MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_45_17_unreachable_branch___00.smt2 | 20.052s | 25.708MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_62_25_assert___00.smt2 | 20.052s | 32.392MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_46_20_length_check___00.smt2 | 20.052s | 32.136MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_12_16_dead_code___00.smt2 | 20.052s | 25.328MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-024__flow_crash__p.adb_32_28_fp_overflow_check___00.smt2 | 20.053s | 29.24MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_55_54_unreachable_branch___00.smt2 | 20.053s | 24.536MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_39_22_assert___00.smt2 | 20.053s | 31.316MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_42_35_length_check___00.smt2 | 20.053s | 32.364MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_42_23_length_check___00.smt2 | 20.053s | 31.98MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_9_23_dead_code___00.smt2 | 20.054s | 30.756MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_65_69_range_check___00.smt2 | 20.054s | 31.26MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_46_20_range_check___00.smt2 | 20.055s | 31.976MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_14_16_dead_code___00.smt2 | 20.055s | 25.504MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_7_7_dead_code___00.smt2 | 20.055s | 33.076MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_68_30_unreachable_branch___00.smt2 | 20.056s | 31.556MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_57_17_unreachable_branch___00.smt2 | 20.056s | 30.312MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_44_23_length_check___00.smt2 | 20.058s | 32.18MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_46_21_unreachable_branch___00.smt2 | 20.058s | 31.888MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_19_18_unreachable_branch___00.smt2 | 20.059s | 24.016MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_39_13_range_check___00.smt2 | 20.060s | 32.084MiB| timeout | 0 | | |