# . * 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-1
Z3 repo: Z3Prover/z3
Z3 commit: 8c989f8840e2c5789cd31aa9465dd2527852d453
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 front-end
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_12_4_precondition___00.smt2 | 0.016s | 19.328MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_73_78_range_check___00.smt2 | 0.016s | 19.324MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_12_27_range_check___00.smt2 | 0.017s | 19.304MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_14_4_precondition___00.smt2 | 0.019s | 19.492MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_9_23_precondition___00.smt2 | 0.022s | 19.792MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_13_19_precondition___00.smt2 | 0.022s | 19.268MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_40_85_range_check___00.smt2 | 0.022s | 19.32MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_22_53_unreachable_branch___00.smt2 | 0.025s | 19.188MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_19_61_range_check___00.smt2 | 0.026s | 19.196MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_26_36_loop_invariant_init___00.smt2 | 0.026s | 19.28MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_26_36_loop_invariant_preserv___00.smt2 | 0.026s | 19.284MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_18_50_range_check___00.smt2 | 0.027s | 19.28MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_38_22_assert___00.smt2 | 0.027s | 20.144MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_15_23_precondition___00.smt2 | 0.027s | 19.2MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_22_18_unreachable_branch___00.smt2 | 0.027s | 19.284MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_25_22_unreachable_branch___00.smt2 | 0.028s | 19.164MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-026__overlayed_objects__p2.ads_27_22_postcondition___00.smt2 | 0.028s | 19.84MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_62_14_postcondition___00.smt2 | 0.028s | 19.304MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_23_9_disjoint_contract_cases___00.smt2 | 0.028s | 20.048MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-024__flow_crash__p.ads_27_22_postcondition___00.smt2 | 0.029s | 19.684MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_52_25_assert___00.smt2 | 0.030s | 20.48MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_49_31_range_check___00.smt2 | 0.031s | 20.472MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_24_61_range_check___00.smt2 | 0.031s | 19.248MiB| 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.031s | 20.152MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_10_4_precondition___00.smt2 | 0.032s | 19.892MiB| 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.034s | 20.312MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_67_66_range_check___00.smt2 | 0.034s | 21.072MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_16_28_assert___00.smt2 | 0.036s | 19.284MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_58_25_assert___00.smt2 | 0.037s | 20.868MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_39_73_range_check___00.smt2 | 0.038s | 21.112MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_24_18_unreachable_branch___00.smt2 | 0.039s | 19.376MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_68_78_range_check___00.smt2 | 0.039s | 19.284MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_37_76_range_check___00.smt2 | 0.040s | 20.476MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_11_19_precondition___00.smt2 | 0.041s | 19.316MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_51_30_unreachable_branch___00.smt2 | 0.041s | 20.564MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_54_25_assert___00.smt2 | 0.042s | 21.116MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_25_64_contract_case___00.smt2 | 0.043s | 20.956MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_45_85_range_check___00.smt2 | 0.044s | 19.416MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_18_16_loop_invariant_init___00.smt2 | 0.045s | 20.212MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_34_19_contract_case___00.smt2 | 0.046s | 21.132MiB| 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.046s | 20.348MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_50_25_assert___00.smt2 | 0.048s | 20.504MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_29_80_contract_case___00.smt2 | 0.050s | 21.084MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_18_16_loop_invariant_preserv___00.smt2 | 0.089s | 21.48MiB| unsat | 1 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_43_52_unreachable_branch___00.smt2 | 20.006s | 25.588MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_15_19_assert___00.smt2 | 20.006s | 23.632MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_46_21_unreachable_branch___00.smt2 | 20.006s | 30.084MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_58_17_unreachable_branch___00.smt2 | 20.006s | 25.3MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_65_27_unreachable_branch___00.smt2 | 20.007s | 29.624MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_39_13_range_check___00.smt2 | 20.007s | 31.456MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_74_34_unreachable_branch___00.smt2 | 20.007s | 25.796MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_71_30_unreachable_branch___00.smt2 | 20.007s | 24.164MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_42_59_unreachable_branch___00.smt2 | 20.007s | 23.52MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_46_31_range_check___00.smt2 | 20.007s | 31.468MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-026__overlayed_objects__p2.adb_39_28_overflow_check___00.smt2 | 20.007s | 23.2MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_40_17_unreachable_branch___00.smt2 | 20.007s | 23.032MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_46_20_length_check___00.smt2 | 20.007s | 31.476MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_20_22_unreachable_branch___00.smt2 | 20.008s | 23.688MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-024__flow_crash__p.adb_32_28_fp_overflow_check___00.smt2 | 20.008s | 27.324MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_39_22_assert___00.smt2 | 20.008s | 29.04MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_55_13_inconsistent_pre___00.smt2 | 20.008s | 28.244MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_63_17_unreachable_branch___00.smt2 | 20.008s | 23.776MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_28_17_dead_code___00.smt2 | 20.008s | 24.56MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_41_22_assert___00.smt2 | 20.008s | 23.784MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_9_19_assert___00.smt2 | 20.008s | 29.4MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_57_28_unreachable_branch___00.smt2 | 20.008s | 30.656MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-026__overlayed_objects__p2.adb_40_28_fp_overflow_check___00.smt2 | 20.008s | 27.276MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MC12-026__overlayed_objects__p.adb_31_28_overflow_check___00.smt2 | 20.008s | 23.06MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_62_25_assert___00.smt2 | 20.008s | 30.86MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_61_14_inconsistent_pre___00.smt2 | 20.008s | 23.688MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_53_30_unreachable_branch___00.smt2 | 20.008s | 29.956MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_43_27_unreachable_branch___00.smt2 | 20.009s | 23.792MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_67_27_unreachable_branch___00.smt2 | 20.009s | 30.348MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_78_10_dead_code___00.smt2 | 20.009s | 29.0MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_55_54_unreachable_branch___00.smt2 | 20.009s | 23.64MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_14_16_dead_code___00.smt2 | 20.009s | 24.964MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_7_7_dead_code___00.smt2 | 20.009s | 29.26MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_26_14_unreachable_branch___00.smt2 | 20.010s | 23.432MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_29_39_unreachable_branch___00.smt2 | 20.010s | 24.056MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_61_28_unreachable_branch___00.smt2 | 20.010s | 30.736MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_45_17_unreachable_branch___00.smt2 | 20.010s | 24.604MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_42_35_length_check___00.smt2 | 20.010s | 31.492MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_40_27_unreachable_branch___00.smt2 | 20.011s | 29.052MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.ads_50_55_range_check___00.smt2 | 20.012s | 31.488MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_71_65_unreachable_branch___00.smt2 | 20.012s | 29.756MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_49_10_dead_code___00.smt2 | 20.012s | 28.98MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_59_54_unreachable_branch___00.smt2 | 20.013s | 23.668MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_9_23_dead_code___00.smt2 | 20.013s | 29.404MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_73_30_unreachable_branch___00.smt2 | 20.014s | 29.528MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_42_35_range_check___00.smt2 | 20.014s | 31.48MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_41_21_unreachable_branch___00.smt2 | 20.014s | 24.332MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_19_18_unreachable_branch___00.smt2 | 20.014s | 23.332MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_13_19_assert___00.smt2 | 20.014s | 25.772MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_7_7_precondition___00.smt2 | 20.014s | 25.684MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_57_17_unreachable_branch___00.smt2 | 20.015s | 28.424MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_37_14_unreachable_branch___00.smt2 | 20.015s | 24.868MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_39_52_unreachable_branch___00.smt2 | 20.016s | 25.58MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.ads_50_9_postcondition___00.smt2 | 20.017s | 31.476MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_44_23_length_check___00.smt2 | 20.017s | 31.536MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_30_14_unreachable_branch___00.smt2 | 20.017s | 24.264MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_46_20_range_check___00.smt2 | 20.018s | 31.48MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_42_23_length_check___00.smt2 | 20.018s | 31.56MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_35_14_unreachable_branch___00.smt2 | 20.019s | 24.748MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_68_30_unreachable_branch___00.smt2 | 20.019s | 30.396MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_12_16_dead_code___00.smt2 | 20.019s | 23.976MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_38_61_range_check___00.smt2 | 20.021s | 31.424MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__test_failsafe.adb_11_19_assert___00.smt2 | 20.021s | 24.4MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_69_34_unreachable_branch___00.smt2 | 20.025s | 28.02MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_56_14_postcondition___00.smt2 | 20.025s | 29.32MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_11_16_dead_code___00.smt2 | 20.026s | 24.836MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_43_17_unreachable_branch___00.smt2 | 20.026s | 24.728MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_76_25_assert___00.smt2 | 20.027s | 25.328MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.ads_39_14_unreachable_branch___00.smt2 | 20.034s | 29.784MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_65_69_range_check___00.smt2 | 20.034s | 29.936MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/MA16-036__flow_missing_globals__logger.adb_45_27_range_check___00.smt2 | 20.035s | 31.48MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_42_28_unreachable_branch___00.smt2 | 20.035s | 30.304MiB| timeout | 0 | | | |non-incremental/AUFBVFPDTNIRA/20200306-Kanig/spark2014bench/OA21-028__failsafe__failsafe.adb_63_62_unreachable_branch___00.smt2 | 20.036s | 23.768MiB| timeout | 0 | | |