# . * SAT 80 * UNSAT 64 * TIMEOUT 2 * 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/QF_UFDTLIRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_UFDTLIRA.tar.zs
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 459629c662eb7abf25a010b7383431a9f729d234
Z3 branch: master
Z3 options: "-T:20 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify sls-smt)" model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_UFDTLIRA.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_24_37_unreachable_branch___00.smt2 | 0.021s | 19.696MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/stopwatch__user.ads_19_17_ceiling__priority_protocol___00.smt2 | 0.022s | 19.596MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/R123-023__flow_unused_variable__q.adb_2_21_range_check___00.smt2 | 0.023s | 19.632MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_138_22_assert___00.smt2 | 0.023s | 19.568MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_37_19_range_check___00.smt2 | 0.025s | 19.604MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q130-019__missing_discr_check__p_init.ads_14_24_range_check___00.smt2 | 0.032s | 19.98MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P511-009__test_attributes__storage_place_attributes.adb_51_22_assert___00.smt2 | 0.032s | 19.84MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P602-007__protected_no_return__p.adb_28_8_precondition___00.smt2 | 0.032s | 19.852MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q412-006__assert_true__p.ads_17_4_assert___00.smt2 | 0.032s | 19.84MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/O402-017__tagged__no_primitive_use.adb_7_4_precondition___00.smt2 | 0.032s | 19.6MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_33_22_assert___00.smt2 | 0.032s | 19.688MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P712-004__prot_discr__main.adb_7_19_assert___00.smt2 | 0.033s | 19.828MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S920-003__flow_implicit_noret__p.adb_10_10_precondition___00.smt2 | 0.033s | 19.66MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_23_31_range_check___00.smt2 | 0.033s | 19.888MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/N915-008__flow_acats_oo__cc1311a.adb_279_17_cc1311a.adb_441_6_range_check___00.smt2 | 0.033s | 19.64MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_87_40_unreachable_branch___00.smt2 | 0.034s | 19.504MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_37_38_overflow_check___00.smt2 | 0.048s | 19.676MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_32_18_range_check___00.smt2 | 0.051s | 19.868MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__functions.adb_22_10_precondition___00.smt2 | 0.051s | 19.848MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_29_18_range_check___00.smt2 | 0.051s | 19.732MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/OB16-016__system_default_priority__main.adb_3_11_ceiling__priority_protocol___00.smt2 | 0.051s | 19.92MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__decl_only.ads_8_18_inconsistent_pre___00.smt2 | 0.051s | 19.504MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_24_22_assert___00.smt2 | 0.051s | 19.684MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__nested_packages.adb_56_13_dead_code___00.smt2 | 0.052s | 19.664MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S711-051__constrained_attr__test_constrained.adb_34_28_null_pointer_dereference___00.smt2 | 0.052s | 19.592MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S729-004__inline_dispatching__p.adb_6_22_assert___00.smt2 | 0.052s | 19.868MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P511-009__test_attributes__storage_place_attributes.adb_95_22_assert___00.smt2 | 0.052s | 19.676MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/NC11-033__variant__variants.ads_13_20_range_check___00.smt2 | 0.054s | 19.528MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q512-013__flow_type_aspects__a.adb_9_7_dead_code___00.smt2 | 0.054s | 19.62MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__nonreturning_spec.ads_2_14_inconsistent_post___00.smt2 | 0.054s | 19.508MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/R220-054__fixed_point_small__fp_test.adb_6_17_overflow_check___00.smt2 | 0.055s | 19.62MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S702-024__record_attributes_in_allocators__test_constr.adb_39_37_null_pointer_dereference___00.smt2 | 0.055s | 19.672MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P511-009__test_attributes__storage_place_attributes.adb_73_22_assert___00.smt2 | 0.056s | 19.888MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_33_37_unreachable_branch___00.smt2 | 0.056s | 19.724MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__imported.adb_10_7_precondition___00.smt2 | 0.057s | 19.612MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M524-002__demorgan__test.adb_10_22_assert___00.smt2 | 0.057s | 19.584MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/L316-015__all__a2.adb_4_5_precondition___00.smt2 | 0.057s | 19.596MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/NC11-033__variant__variants.ads_14_20_range_check___00.smt2 | 0.057s | 19.688MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q130-019__missing_discr_check__p_init.ads_15_24_range_check___00.smt2 | 0.059s | 19.552MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_29_29_overflow_check___00.smt2 | 0.059s | 19.704MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P511-009__test_attributes__component_size_attribute.adb_37_7_assert___00.smt2 | 0.059s | 19.644MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/OB17-029__ceiling_elaboration_task__t.ads_2_9_task_termination___00.smt2 | 0.060s | 19.644MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/O429-052__flow_tasking_exclusivity_checks__task_type_array_single_so.ads_7_14_task_termination___00.smt2 | 0.060s | 19.74MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_32_29_overflow_check___00.smt2 | 0.060s | 19.624MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KB04-032__lib_level__p.adb_6_19_assert___00.smt2 | 0.060s | 19.832MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S702-024__record_attributes_in_allocators__test_constr.adb_39_22_assert___00.smt2 | 0.060s | 19.704MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M604-044__overflow__misovattr.adb_6_35_range_check___00.smt2 | 0.060s | 19.52MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M604-044__overflow__misovattr.adb_8_35_range_check___00.smt2 | 0.060s | 19.656MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M604-044__overflow__misovattr.adb_6_22_assert___00.smt2 | 0.060s | 19.584MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/O429-052__flow_tasking_review__unsync_access__bar.adb_16_17_range_check___00.smt2 | 0.060s | 19.76MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P725-016__recursive_spec__main.adb_5_19_assert___00.smt2 | 0.060s | 19.596MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KB10-018__cursor_location__cursor_location.ads_11_24_unreachable_branch___00.smt2 | 0.060s | 19.752MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KB10-018__cursor_location__cursor_location.ads_10_23_unreachable_branch___00.smt2 | 0.060s | 19.536MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_21_31_range_check___00.smt2 | 0.060s | 19.6MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/O429-052__flow_tasking_exclusivity_checks__two_task_type_objects_single_so.ads_7_14_task_termination___00.smt2 | 0.060s | 19.9MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_19_37_unreachable_branch___00.smt2 | 0.060s | 19.552MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__nested_packages.adb_27_16_dead_code___00.smt2 | 0.061s | 19.608MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M524-002__demorgan__test.adb_6_22_assert___00.smt2 | 0.061s | 19.512MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S325-002__rec_pointers_bad__use_incomplete_type_auto.ads_4_19_assert___00.smt2 | 0.061s | 19.728MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__nest_in_proc.adb_21_13_dead_code___00.smt2 | 0.065s | 20.076MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/K512-016__task__t.ads_3_9_task_termination___00.smt2 | 0.065s | 19.6MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_37_31_overflow_check___00.smt2 | 0.068s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/stopwatch__timer.adb_16_17_ceiling__priority_protocol___00.smt2 | 0.070s | 20.092MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_44_22_assert___00.smt2 | 0.071s | 19.592MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q906-011__counterexample__copy_values.adb_6_22_assert___00.smt2 | 0.072s | 19.86MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S920-003__flow_noret__noret.adb_6_7_raise___00.smt2 | 0.076s | 19.82MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S818-002__might_not_return__pack.adb_5_7_raise___00.smt2 | 0.077s | 20.092MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_51_22_assert___00.smt2 | 0.080s | 19.84MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P511-009__test_attributes__component_size_attribute.adb_49_7_assert___00.smt2 | 0.082s | 19.692MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__nested_blocks.adb_11_29_dead_code___00.smt2 | 0.087s | 20.096MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_45_22_assert___00.smt2 | 0.090s | 19.596MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P602-007__protected_no_return__p.adb_23_6_precondition___00.smt2 | 0.095s | 20.068MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S702-024__record_attributes_in_allocators__test_constr.adb_24_30_null_pointer_dereference___00.smt2 | 0.096s | 19.96MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/L316-015__all__a1.adb_4_5_precondition___00.smt2 | 0.102s | 19.828MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q818-007__projection__sc_status_type.adb_5_22_assert___00.smt2 | 0.102s | 20.076MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M604-044__overflow__misovattr.adb_9_35_range_check___00.smt2 | 0.106s | 19.836MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P511-009__test_attributes__component_size_attribute.adb_55_7_assert___00.smt2 | 0.106s | 19.608MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__nested_packages.adb_62_10_dead_code___00.smt2 | 0.111s | 20.384MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/N609-025__private_type_discr__record_discr.adb_24_28_discriminant_check___00.smt2 | 0.111s | 20.308MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_54_22_assert___00.smt2 | 0.113s | 20.064MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/stopwatch__user.ads_12_17_ceiling__priority_protocol___00.smt2 | 0.120s | 19.584MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q508-012__flow_null_proc__nullproc.ads_7_9_task_termination___00.smt2 | 0.121s | 20.068MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_112_22_assert___00.smt2 | 0.124s | 19.512MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/PA11-007__depchain__a-reatim.ads_6_4_assert___00.smt2 | 0.125s | 20.312MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/L531-021__discr__special.ads_6_32_range_check___00.smt2 | 0.127s | 20.092MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KB28-003__succ__p.adb_12_23_range_check___00.smt2 | 0.128s | 19.94MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P712-004__prot_discr__p.ads_7_13_range_check___00.smt2 | 0.128s | 19.82MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_41_31_overflow_check___00.smt2 | 0.130s | 19.888MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_77_22_assert___00.smt2 | 0.131s | 19.84MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__enums__enums.adb_194_29_range_check___00.smt2 | 0.135s | 19.676MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_87_22_assert___00.smt2 | 0.138s | 19.86MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_18_22_assert___00.smt2 | 0.139s | 19.804MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S702-024__record_attributes_in_allocators__test_constr.adb_24_22_assert___00.smt2 | 0.142s | 20.332MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__r.adb_53_7_precondition___00.smt2 | 0.143s | 19.476MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__real_world__real_world.adb_44_22_assert___00.smt2 | 0.144s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_71_22_assert___00.smt2 | 0.144s | 19.708MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__imported.ads_14_13_inconsistent_pre___00.smt2 | 0.148s | 19.628MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_29_36_overflow_check___00.smt2 | 0.150s | 19.892MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P712-004__prot_discr__p.ads_6_13_range_check___00.smt2 | 0.151s | 19.7MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/O429-052__flow_tasking_exclusivity_checks__two_tasks_single_so.ads_9_9_task_termination___00.smt2 | 0.154s | 19.912MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/L531-021__discr__subty.ads_5_20_range_check___00.smt2 | 0.154s | 19.904MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_80_22_assert___00.smt2 | 0.154s | 20.132MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_21_38_range_check___00.smt2 | 0.155s | 19.608MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_27_22_assert___00.smt2 | 0.155s | 19.648MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P511-009__test_attributes__component_size_attribute.adb_43_7_assert___00.smt2 | 0.155s | 20.148MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_19_22_assert___00.smt2 | 0.155s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_139_33_unreachable_branch___00.smt2 | 0.155s | 19.596MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P929-043__flow_pkg_elaboration_in_direct_calls__nest_in_proc.adb_9_7_precondition___00.smt2 | 0.156s | 19.604MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M809-022__scenario__q.adb_6_7_assert___00.smt2 | 0.156s | 19.848MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_66_22_assert___00.smt2 | 0.156s | 20.072MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M604-044__overflow__misovattr.adb_7_35_range_check___00.smt2 | 0.156s | 19.88MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_41_19_range_check___00.smt2 | 0.157s | 19.6MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P725-016__recursive_spec__main.adb_5_19_precondition___00.smt2 | 0.157s | 19.832MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/O521-002__no_return__p.adb_23_6_precondition___00.smt2 | 0.157s | 19.888MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/S920-003__flow_implicit_noret__p.adb_5_10_raise___00.smt2 | 0.157s | 20.32MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_41_38_overflow_check___00.smt2 | 0.157s | 19.792MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_32_36_overflow_check___00.smt2 | 0.157s | 19.752MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P126-025__generic_procedure_renaming__c.adb_8_4_precondition___00.smt2 | 0.157s | 20.072MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/PA27-015__nested_no_return__nest_in_proc.adb_14_4_precondition___00.smt2 | 0.158s | 19.588MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_40_18_inconsistent_pre___00.smt2 | 0.158s | 19.828MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_139_44_unreachable_branch___00.smt2 | 0.158s | 19.732MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/stopwatch__user.ads_26_17_ceiling__priority_protocol___00.smt2 | 0.158s | 20.02MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/KB28-003__succ__p.adb_6_23_range_check___00.smt2 | 0.158s | 19.788MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q512-018__null_task_id__main.adb_7_41_precondition___00.smt2 | 0.159s | 19.868MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/R220-054__fixed_point_small__fp_test.ads_13_23_overflow_check___00.smt2 | 0.159s | 19.84MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/R123-023__flow_unused_variable__q.adb_7_17_discriminant_check___00.smt2 | 0.159s | 19.844MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__functions.adb_9_10_dead_code___00.smt2 | 0.159s | 19.5MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__p.adb_22_10_dead_code___00.smt2 | 0.160s | 20.092MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/L323-005__recursive__p.adb_6_23_assert___00.smt2 | 0.160s | 20.144MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_20_33_unreachable_branch___00.smt2 | 0.160s | 19.864MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__r.adb_46_10_dead_code___00.smt2 | 0.160s | 19.636MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q512-013__flow_type_aspects__a.adb_7_10_dead_code___00.smt2 | 0.160s | 19.86MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M604-044__overflow__misovattr.adb_8_22_assert___00.smt2 | 0.160s | 19.824MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_14_18_inconsistent_pre___00.smt2 | 0.160s | 19.632MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/L323-005__recursive__p.ads_7_36_postcondition___00.smt2 | 0.161s | 19.584MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/O429-052__flow_tasking_exclusivity_checks__two_tasks_single_so.ads_7_9_task_termination___00.smt2 | 0.161s | 19.688MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M524-002__demorgan__test.adb_8_22_assert___00.smt2 | 0.161s | 19.52MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_30_22_assert___00.smt2 | 0.161s | 19.608MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__functions.adb_16_7_functions.adb_29_4_precondition___00.smt2 | 0.161s | 19.584MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/Q508-012__flow_null_proc__expanded.ads_7_9_task_termination___00.smt2 | 0.162s | 19.868MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__real_world__real_world.adb_45_21_range_check___00.smt2 | 0.166s | 19.86MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/OC09-042__po_in_spec_only_pkg__main.adb_3_11_ceiling__priority_protocol___00.smt2 | 0.169s | 19.644MiB| unsat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/P715-019__flow_subprogram_termination__call_proc_no_body.adb_4_7_precondition___00.smt2 | 0.170s | 19.844MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_74_22_assert___00.smt2 | 0.171s | 19.944MiB| sat | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/M524-002__demorgan__test.adb_12_22_assert___00.smt2 | 20.012s | 19.732MiB| timeout | 0 | | | |non-incremental/QF_UFDTLIRA/20200306-Kanig/spark2014bench/riposte__logic__logic.adb_115_22_assert___00.smt2 | 20.145s | 19.848MiB| timeout | 0 | | |