# .

* SAT 0
* UNSAT 150
* TIMEOUT 0
* UNKNOWN 645

* ERRORS 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/UFFPDTNIRA.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-UFFPDTNIRA.tar.zst
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/UFFPDTNIRA.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_47_19_assert___00.smt2 |    0.022s | 20.344MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_47_22_assert___00.smt2 |    0.022s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__call_sample2.adb_13_7_call_sample2.adb_28_4_precondition___00.smt2 |    0.023s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b2d859_generic_float_tests-T-defqtvc__00.smt2 |    0.023s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_103_13_precondition___00.smt2 |    0.023s | 20.096MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ca1a1e_generic_float_tests-T-defqtvc__00.smt2 |    0.023s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_bb54cc_generic_float_tests-T-defqtvc__00.smt2 |    0.024s | 20.092MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a34115_generic_float_tests-T-defqtvc__00.smt2 |    0.024s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5fa6e1_generic_float_tests-T-defqtvc__00.smt2 |    0.024s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_42_34_range_check___00.smt2 |    0.025s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_12_31_overflow_check___00.smt2 |    0.025s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_31_32_division_check___00.smt2 |    0.026s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_617_26_precondition___00.smt2 |    0.026s | 19.788MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_49_19_precondition___00.smt2 |    0.026s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1473_19_precondition___00.smt2 |    0.026s | 19.664MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_20_22_assert___00.smt2 |    0.027s | 19.632MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_577b67_generic_float_tests-T-defqtvc__00.smt2 |    0.027s | 20.072MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_56_4_precondition___00.smt2 |    0.027s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level0__hard_stuff.adb_28_17_fp_overflow_check___00.smt2 |    0.028s | 20.364MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_22_20_range_check___00.smt2 |    0.028s | 19.984MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1185_52_precondition___00.smt2 |    0.028s | 19.608MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_20_21_division_check___00.smt2 |    0.028s | 19.612MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_444_27_range_check___00.smt2 |    0.028s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_60_22_range_check___01.smt2 |    0.028s | 19.92MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_22_32_fp_overflow_check___00.smt2 |    0.028s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_15_22_assert___00.smt2 |    0.029s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__biaseddivide.ads_19_14_postcondition___00.smt2 |    0.029s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ea0c9f_generic_float_tests-T-defqtvc__00.smt2 |    0.029s | 19.8MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_44_12_fp_overflow_check___00.smt2 |    0.030s | 19.748MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_133_22_assert___00.smt2 |    0.030s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_25_31_fp_overflow_check___00.smt2 |    0.030s | 20.112MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_34db83_generic_float_tests-T-defqtvc__00.smt2 |    0.031s | 19.736MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_637_21_range_check___00.smt2 |    0.031s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_92_70_contract_case___00.smt2 |    0.031s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_7_14_overflow_check___00.smt2 |    0.031s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_199_14_precondition___00.smt2 |    0.031s | 19.668MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1209_31_fp_overflow_check___00.smt2 |    0.031s | 20.016MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_4aaffb_generic_float_tests-T-defqtvc__00.smt2 |    0.031s | 19.736MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_28_22_assert___00.smt2 |    0.031s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level0__hard_stuff.adb_28_29_fp_overflow_check___00.smt2 |    0.032s | 20.112MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_41_22_assert___00.smt2 |    0.032s | 20.008MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_8_71_challenges.adb_15_14_challenges.adb_24_14_challenges.adb_33_29_challenges.adb_38_10_fp_overflow_check___00.smt2 |    0.032s | 20.132MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3176a4_generic_interval_tests-T-defqtvc__00.smt2 |    0.032s | 19.824MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_cc6bc3_generic_interval_tests-T-defqtvc__00.smt2 |    0.032s | 19.804MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_38_19_postcondition___00.smt2 |    0.032s | 20.096MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_113_14_precondition___00.smt2 |    0.032s | 19.76MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_8_20_fp_overflow_check___00.smt2 |    0.033s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_275c6e_generic_float_tests-T-defqtvc__00.smt2 |    0.033s | 19.724MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_83ffdb_generic_float_tests-T-defqtvc__00.smt2 |    0.033s | 19.792MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_1.adb_30_19_postcondition___00.smt2 |    0.033s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_5_12_range_check___00.smt2 |    0.033s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC04-023__float_conversion__type_conversion.ads_9_21_postcondition___00.smt2 |    0.033s | 19.668MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_16_142_fp_overflow_check___00.smt2 |    0.033s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_391_69_overflow_check___00.smt2 |    0.034s | 19.872MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_16_100_postcondition___00.smt2 |    0.034s | 19.732MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_15_62_contract_case___00.smt2 |    0.034s | 19.584MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_d5baaf_generic_float_tests-T-defqtvc__00.smt2 |    0.034s | 19.62MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_33_fp_overflow_check___00.smt2 |    0.034s | 19.76MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_12_19_assert___00.smt2 |    0.034s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_56_22_assert___00.smt2 |    0.034s | 19.976MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_726911_generic_float_tests-T-defqtvc__00.smt2 |    0.034s | 19.668MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_14_18_fp_overflow_check2___00.smt2 |    0.035s | 20.076MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_19_74_range_check___00.smt2 |    0.035s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_36_14_postcondition___00.smt2 |    0.035s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_62_32_overflow_check___00.smt2 |    0.035s | 20.156MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P310-021__proof_float_remainder__foo.adb_16_17_division_check___00.smt2 |    0.035s | 19.588MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_bbb756_generic_float_tests-T-defqtvc__00.smt2 |    0.035s | 19.588MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O220-024__floats__test_pack.adb_7_32_fp_overflow_check___00.smt2 |    0.035s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_683e07_generic_float_tests-T-defqtvc__00.smt2 |    0.036s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_4_14_overflow_check___00.smt2 |    0.036s | 19.8MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_10_30_fp_overflow_check___00.smt2 |    0.036s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_65_49_overflow_check___00.smt2 |    0.036s | 20.188MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_212f49_generic_interval_tests-T-defqtvc__00.smt2 |    0.036s | 19.92MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_15_17_postcondition___00.smt2 |    0.036s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_26_49_fp_overflow_check___00.smt2 |    0.037s | 20.136MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O810-001__predicate__safety_pack.ads_55_21_range_check___00.smt2 |    0.037s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0fa4d6_generic_float_tests-T-defqtvc__00.smt2 |    0.037s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_d25f13_generic_float_tests-T-defqtvc__00.smt2 |    0.037s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3b4c73_generic_float_tests-T-defqtvc__00.smt2 |    0.037s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_21_15_fp_overflow_check___00.smt2 |    0.037s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1032_47_precondition___00.smt2 |    0.037s | 19.712MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_627_26_precondition___00.smt2 |    0.037s | 20.104MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_24_22_assert___00.smt2 |    0.037s | 19.804MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_53_4_precondition___00.smt2 |    0.037s | 20.036MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_28_22_assert___00.smt2 |    0.037s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__dimensions.ads_377_14_fp_overflow_check___00.smt2 |    0.038s | 20.088MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e9287d_homothetical-T-defqtvc__00.smt2 |    0.038s | 19.652MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_30_22_assert___00.smt2 |    0.038s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_11_31_overflow_check___00.smt2 |    0.038s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_41_55_range_check___00.smt2 |    0.038s | 20.044MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_30_36_fp_overflow_check___00.smt2 |    0.038s | 19.964MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O312-037__flow_pure_subprograms__call.adb_22_51_precondition___00.smt2 |    0.038s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_18_17_range_check___00.smt2 |    0.038s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_35_45_fp_overflow_check___00.smt2 |    0.038s | 20.024MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__range_check.adb_33_12_range_check___00.smt2 |    0.038s | 19.996MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_444_66_overflow_check___00.smt2 |    0.038s | 19.692MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_8_11_fp_overflow_check___00.smt2 |    0.038s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_23_47_division_check___00.smt2 |    0.039s | 19.872MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__ce__counter_examples.adb_8_38_fp_overflow_check___00.smt2 |    0.039s | 19.616MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/QA11-003__itp_example__test.adb_60_14_fp_overflow_check___00.smt2 |    0.039s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_26_26_fp_overflow_check___00.smt2 |    0.039s | 19.924MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O917-065__unreferenced__unref.adb_5_19_postcondition___00.smt2 |    0.039s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5dc342_generic_float_tests-T-defqtvc__00.smt2 |    0.039s | 20.324MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P906-011__exp_division__expo.adb_6_11_division_check___00.smt2 |    0.039s | 19.872MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_44_19_assert___00.smt2 |    0.039s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA20-061__flow_variable_constant__basic_contracts.adb_12_18_division_check___00.smt2 |    0.039s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ffe5a5_generic_float_tests-T-defqtvc__00.smt2 |    0.039s | 20.044MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8a6cb4_generic_float_tests-T-defqtvc__00.smt2 |    0.039s | 20.104MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-018__spurious_discr__useless_discr.adb_19_5_discriminant_check___00.smt2 |    0.039s | 20.06MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_40_14_postcondition___00.smt2 |    0.039s | 20.036MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_92_7_complete_contract_cases___00.smt2 |    0.039s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_41_14_postcondition___00.smt2 |    0.039s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_13_22_assert___00.smt2 |    0.039s | 19.916MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_34_14_division_check___00.smt2 |    0.040s | 19.952MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_106_14_postcondition___00.smt2 |    0.040s | 20.336MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P620-034__float_out_subtype__get_out_subtype.adb_28_33_range_check___00.smt2 |    0.040s | 19.896MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_10_142_fp_overflow_check___00.smt2 |    0.040s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_15_33_loop_invariant_init2___00.smt2 |    0.040s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB25-022__exp__gp_exp.adb_5_14_range_check___00.smt2 |    0.040s | 19.744MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1583cf_generic_float_tests-T-defqtvc__00.smt2 |    0.041s | 20.04MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5dd164_generic_float_tests-T-defqtvc__00.smt2 |    0.041s | 19.756MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_28_17_range_check___00.smt2 |    0.041s | 19.672MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1059_52_precondition___00.smt2 |    0.041s | 19.796MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O224-020__constant_aggr__package_1.adb_12_29_fp_overflow_check___00.smt2 |    0.041s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__division_by_zero.adb_29_14_fp_overflow_check___00.smt2 |    0.041s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB25-022__exp__gp_exp.adb_5_11_overflow_check___00.smt2 |    0.041s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1d2077_generic_interval_tests-T-defqtvc__00.smt2 |    0.041s | 19.744MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_15_24_overflow_check2___00.smt2 |    0.041s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1209_31_division_check___00.smt2 |    0.041s | 19.872MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_31_26_unreachable_branch___00.smt2 |    0.041s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_28_fp_overflow_check___00.smt2 |    0.042s | 19.808MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_26_fp_overflow_check___00.smt2 |    0.042s | 19.676MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b5915a_generic_float_tests-T-defqtvc__00.smt2 |    0.042s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_475713_generic_interval_tests-T-defqtvc__00.smt2 |    0.042s | 19.744MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_579cc3_generic_float_tests-T-defqtvc__00.smt2 |    0.043s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.ads_38_32_range_check___00.smt2 |    0.043s | 20.02MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_11_18_fp_overflow_check___00.smt2 |    0.043s | 20.244MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_22e79d_generic_interval_tests-T-defqtvc__00.smt2 |    0.043s | 20.052MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_2.adb_32_19_postcondition___00.smt2 |    0.043s | 20.348MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_84_14_range_check___00.smt2 |    0.043s | 19.652MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/QA11-003__itp_example__test.adb_56_17_postcondition___00.smt2 |    0.043s | 20.096MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_19_43_division_check___00.smt2 |    0.043s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b32673_generic_float_tests-T-defqtvc__00.smt2 |    0.043s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_8_54_challenges.adb_15_14_challenges.adb_24_14_challenges.adb_33_29_challenges.adb_38_10_range_check___00.smt2 |    0.044s | 20.36MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_36_fp_overflow_check___00.smt2 |    0.044s | 19.788MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P310-021__proof_float_remainder__foo.adb_9_17_division_check___00.smt2 |    0.044s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P909-014__numerics__numerics-algo.adb_19_17_precondition___00.smt2 |    0.044s | 19.904MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_38_32_range_check___00.smt2 |    0.044s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_32_22_assert___00.smt2 |    0.044s | 19.892MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__errorexamplefloat.adb_29_22_assert___00.smt2 |    0.044s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_10_22_assert___00.smt2 |    0.044s | 19.748MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_74_22_assert___00.smt2 |    0.045s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.adb_10_19_precondition___00.smt2 |    0.045s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_float.adb_16_4_precondition___00.smt2 |    0.045s | 19.976MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_142_14_range_check___00.smt2 |    0.045s | 19.812MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_100_75_range_check___00.smt2 |    0.045s | 20.044MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_8_19_assert___00.smt2 |    0.045s | 19.816MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_13_100_postcondition___00.smt2 |    0.045s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_60_22_range_check___00.smt2 |    0.046s | 20.348MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_62_27_overflow_check___00.smt2 |    0.046s | 20.048MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_24_61_challenges.adb_33_29_challenges.adb_38_10_range_check___00.smt2 |    0.046s | 20.216MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_11_19_assert___00.smt2 |    0.046s | 19.768MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_58_22_assert___00.smt2 |    0.047s | 20.104MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_168f5d_generic_float_tests-T-defqtvc__00.smt2 |    0.047s | 19.652MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0354a0_generic_float_tests-T-defqtvc__00.smt2 |    0.047s | 20.056MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6cb1b4_generic_interval_tests-T-defqtvc__00.smt2 |    0.047s | 19.756MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__division_by_zero.adb_39_14_fp_overflow_check___00.smt2 |    0.048s | 19.732MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_18.adb_7_12_fp_overflow_check___00.smt2 |    0.048s | 19.772MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_104_75_range_check___00.smt2 |    0.048s | 20.004MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_18_13_range_check___00.smt2 |    0.048s | 19.972MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_752865_generic_float_tests-T-defqtvc__00.smt2 |    0.049s | 19.728MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_12_25_assert2___00.smt2 |    0.049s | 19.756MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_53_22_assert___00.smt2 |    0.049s | 20.0MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e5004c_generic_interval_tests-T-defqtvc__00.smt2 |    0.049s | 19.564MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero__run.ads_14_19_postcondition___00.smt2 |    0.049s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_11_19_assert___00.smt2 |    0.049s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.adb_10_14_precondition___00.smt2 |    0.050s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_53_19_assert___00.smt2 |    0.050s | 19.94MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_15_22_assert___00.smt2 |    0.050s | 19.928MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_46_22_assert___00.smt2 |    0.050s | 19.708MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_26_36_range_check___00.smt2 |    0.050s | 19.988MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_39_45_fp_overflow_check___00.smt2 |    0.050s | 19.92MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1194_21_range_check___00.smt2 |    0.050s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K831-006__cmp__max.ads_4_19_postcondition___00.smt2 |    0.051s | 19.58MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_25_55_fp_overflow_check___00.smt2 |    0.051s | 19.836MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_45_17_fp_overflow_check___00.smt2 |    0.051s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.adb_10_52_precondition___00.smt2 |    0.051s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/TU__depends_legal__depends_legal_2.adb_45_15_discriminant_check___00.smt2 |    0.051s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_17_22_assert___00.smt2 |    0.051s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_50_31_overflow_check___00.smt2 |    0.051s | 19.808MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_12_22_assert___00.smt2 |    0.052s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P909-014__numerics__numerics-algo.adb_20_17_precondition___00.smt2 |    0.052s | 19.828MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_18_24_overflow_check___00.smt2 |    0.052s | 19.816MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_13_19_assert___00.smt2 |    0.052s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-018__spurious_discr__useless_discr.adb_16_10_range_check___00.smt2 |    0.052s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_18_21_division_check___00.smt2 |    0.052s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1077_52_precondition___00.smt2 |    0.052s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_23_22_assert___00.smt2 |    0.052s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_349_56_fp_overflow_check___00.smt2 |    0.052s | 19.62MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ec718c_generic_float_tests-T-defqtvc__00.smt2 |    0.052s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_55_22_assert___00.smt2 |    0.052s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_12_11_fp_overflow_check___00.smt2 |    0.053s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_15_12_postcondition___00.smt2 |    0.053s | 19.756MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_43_19_assert___00.smt2 |    0.053s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_995c50_generic_float_tests-T-defqtvc__00.smt2 |    0.053s | 19.812MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_64_54_overflow_check___00.smt2 |    0.054s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_9_19_assert___00.smt2 |    0.054s | 19.832MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_457_22_fp_overflow_check___00.smt2 |    0.054s | 19.612MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q208-056__no_denorm_on_target__compute.adb_4_20_overflow_check___00.smt2 |    0.054s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_189_47_precondition___00.smt2 |    0.054s | 19.712MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b64636_generic_float_tests-T-defqtvc__00.smt2 |    0.054s | 19.796MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8222b5_generic_float_tests-T-defqtvc__00.smt2 |    0.054s | 19.904MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_162_22_assert___00.smt2 |    0.054s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_99634e_generic_interval_tests-T-defqtvc__00.smt2 |    0.054s | 19.876MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_16bd7a_generic_float_tests-T-defqtvc__00.smt2 |    0.055s | 19.676MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_5_14_fp_overflow_check___00.smt2 |    0.055s | 19.816MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_16abab_generic_float_tests-T-defqtvc__00.smt2 |    0.055s | 19.7MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_65_44_fp_overflow_check___00.smt2 |    0.055s | 19.748MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__errorexamplefloat.adb_48_22_assert___00.smt2 |    0.055s | 19.732MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_12_19_assert___00.smt2 |    0.055s | 19.668MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_4b6267_generic_interval_tests-T-defqtvc__00.smt2 |    0.056s | 19.744MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_19_38_loop_invariant_preserv___00.smt2 |    0.056s | 19.964MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b9e22d_generic_float_tests-T-defqtvc__00.smt2 |    0.056s | 19.696MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_12_11_division_check___00.smt2 |    0.056s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_31_32_fp_overflow_check___00.smt2 |    0.056s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M227-029__flow_records_and_arrays__message_tests.adb_37_16_fp_overflow_check___00.smt2 |    0.056s | 19.82MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.adb_8_15_precondition___00.smt2 |    0.057s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_51_19_precondition___00.smt2 |    0.057s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_6_11_fp_overflow_check___00.smt2 |    0.057s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_15_24_division_check___00.smt2 |    0.057s | 19.672MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_23_43_fp_overflow_check___00.smt2 |    0.057s | 20.352MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_float.adb_11_14_range_check___00.smt2 |    0.058s | 19.612MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_134_22_assert___00.smt2 |    0.059s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b33c2b_generic_float_tests-T-defqtvc__00.smt2 |    0.059s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_45_14_postcondition___00.smt2 |    0.059s | 20.144MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB02-004__inherited_sub__main.adb_18_27_range_check___00.smt2 |    0.059s | 19.864MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_46_19_assert___00.smt2 |    0.059s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_27_8_precondition___00.smt2 |    0.059s | 19.948MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1219_33_fp_overflow_check___00.smt2 |    0.059s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P620-034__float_out_subtype__get_out_subtype.adb_27_33_range_check___00.smt2 |    0.060s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_9b3454_generic_float_tests-T-defqtvc__00.smt2 |    0.060s | 19.588MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e5185b_generic_float_tests-T-defqtvc__00.smt2 |    0.060s | 20.128MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_31_27_discriminant_check___00.smt2 |    0.060s | 19.728MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_50_38_overflow_check___00.smt2 |    0.061s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e5cfc1_generic_float_tests-T-defqtvc__00.smt2 |    0.061s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_17_35_division_check2___00.smt2 |    0.061s | 19.896MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.ads_29_20_postcondition___00.smt2 |    0.061s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_9be82f_generic_float_tests-T-defqtvc__00.smt2 |    0.061s | 19.828MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_336_42_fp_overflow_check___00.smt2 |    0.061s | 19.764MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_13_46_division_check___00.smt2 |    0.061s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_57_24_range_check___00.smt2 |    0.061s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_63_40_overflow_check___00.smt2 |    0.061s | 20.276MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N121-026__nonlinear__nonlinear.adb_9_20_fp_overflow_check___00.smt2 |    0.061s | 19.816MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.ads_22_20_postcondition___00.smt2 |    0.061s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.ads_13_17_postcondition___00.smt2 |    0.062s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_988971_generic_float_tests-T-defqtvc__00.smt2 |    0.062s | 19.712MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O220-024__floats__test_pack.ads_12_43_fp_overflow_check___00.smt2 |    0.062s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_57_24_range_check___01.smt2 |    0.062s | 19.76MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_24_19_postcondition___00.smt2 |    0.062s | 20.368MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_607_25_precondition___00.smt2 |    0.063s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_19_28_discriminant_check___00.smt2 |    0.063s | 20.104MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c786f0_generic_interval_tests-T-defqtvc__00.smt2 |    0.063s | 19.8MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_66_25_assert___00.smt2 |    0.064s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_577336_generic_float_tests-T-defqtvc__00.smt2 |    0.064s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-038__float_intervals__foo.adb_30_22_assert___00.smt2 |    0.064s | 19.896MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_43_fp_overflow_check___00.smt2 |    0.065s | 19.956MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_34_22_range_check___00.smt2 |    0.066s | 19.724MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_22_22_assert___00.smt2 |    0.066s | 19.972MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_6_18_range_check___00.smt2 |    0.066s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_92_7_disjoint_contract_cases___00.smt2 |    0.066s | 20.368MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_20_54_fp_overflow_check___00.smt2 |    0.067s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_13_48_challenges.adb_24_14_challenges.adb_33_29_challenges.adb_38_10_range_check___00.smt2 |    0.067s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_55_19_assert___00.smt2 |    0.067s | 19.756MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_30_32_fp_overflow_check___00.smt2 |    0.067s | 19.792MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OC30-005__crash.adb_10_18_fp_overflow_check___00.smt2 |    0.067s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_15_14_discriminant_check___00.smt2 |    0.067s | 20.036MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_7_19_assert___00.smt2 |    0.067s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5f8af6_generic_float_tests-T-defqtvc__00.smt2 |    0.067s | 19.724MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_8_37_challenges.adb_15_14_challenges.adb_24_14_challenges.adb_33_29_challenges.adb_38_10_range_check___00.smt2 |    0.067s | 20.12MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_336_22_fp_overflow_check___00.smt2 |    0.068s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_11_22_assert___00.smt2 |    0.068s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_24_18_range_check___00.smt2 |    0.068s | 19.788MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_53_14_postcondition___00.smt2 |    0.068s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_23_9_fp_overflow_check___00.smt2 |    0.068s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_54_22_assert___00.smt2 |    0.068s | 19.832MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_22_20_range_check___00.smt2 |    0.069s | 20.112MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_37_22_assert___00.smt2 |    0.069s | 20.112MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_8_71_challenges.adb_15_14_challenges.adb_24_14_challenges.adb_33_29_challenges.adb_38_10_range_check___00.smt2 |    0.069s | 20.024MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_22_20_fp_overflow_check___00.smt2 |    0.070s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1484_19_precondition___00.smt2 |    0.070s | 19.804MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_10_17_postcondition___00.smt2 |    0.070s | 19.912MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB23-014__float_monotonicity__mul.adb_13_4_precondition___00.smt2 |    0.070s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_71_14_postcondition___00.smt2 |    0.071s | 20.116MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_457_51_fp_overflow_check___00.smt2 |    0.071s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_18_21_fp_overflow_check___00.smt2 |    0.072s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b5e7a0_generic_float_tests-T-defqtvc__00.smt2 |    0.072s | 19.82MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_796bf2_generic_float_tests-T-defqtvc__00.smt2 |    0.072s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5cf5ea_generic_float_tests-T-defqtvc__00.smt2 |    0.072s | 19.904MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_28_8_unreachable_branch___00.smt2 |    0.073s | 20.024MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S603-051__dimensions__image_golf_hole.adb_16_10_image_golf_hole.adb_32_10_predicate_check_on_default_value___00.smt2 |    0.073s | 20.34MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_827c21_generic_float_tests-T-defqtvc__00.smt2 |    0.073s | 20.364MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_45_38_overflow_check___00.smt2 |    0.073s | 19.824MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_10_65_fp_overflow_check___00.smt2 |    0.073s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S603-051__dimensions__dimensions.ads_377_11_fp_overflow_check___00.smt2 |    0.074s | 20.184MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_10_11_fp_overflow_check___00.smt2 |    0.074s | 19.752MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.ads_18_19_postcondition___00.smt2 |    0.074s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8f06c6_generic_interval_tests-T-defqtvc__00.smt2 |    0.074s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_106_75_division_check___00.smt2 |    0.074s | 20.424MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_475293_generic_float_tests-T-defqtvc__00.smt2 |    0.075s | 19.576MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_10_42_overflow_check___00.smt2 |    0.075s | 19.624MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_19_108_postcondition___00.smt2 |    0.075s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_21_22_assert___00.smt2 |    0.075s | 19.68MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_40_22_assert___00.smt2 |    0.075s | 20.432MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_25_32_fp_overflow_check___00.smt2 |    0.075s | 19.896MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f2780c_generic_float_tests-T-defqtvc__00.smt2 |    0.076s | 20.26MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_10_100_postcondition___00.smt2 |    0.076s | 20.004MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0d36c5_generic_float_tests-T-defqtvc__00.smt2 |    0.076s | 19.88MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_30_22_discriminant_check___00.smt2 |    0.076s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_11_33_loop_invariant_init2___00.smt2 |    0.076s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_43_34_range_check___00.smt2 |    0.077s | 20.168MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3d969b_generic_float_tests-T-defqtvc__00.smt2 |    0.077s | 19.768MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_54_22_assert___00.smt2 |    0.077s | 20.34MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero__run.ads_19_19_postcondition___00.smt2 |    0.077s | 20.088MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__errorexamplefloat.adb_39_65_fp_overflow_check___00.smt2 |    0.077s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O429-046__flow_tasking_contracts__watchdog.ads_6_9_ceiling__priority_protocol___00.smt2 |    0.078s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N121-026__nonlinear__nonlinear.adb_10_20_fp_overflow_check___00.smt2 |    0.078s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_19_22_assert___00.smt2 |    0.078s | 20.204MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_76_56_fp_overflow_check___00.smt2 |    0.078s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_336b10_generic_interval_tests-T-defqtvc__00.smt2 |    0.078s | 19.664MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_8_14_fp_overflow_check___00.smt2 |    0.078s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_98_22_assert___00.smt2 |    0.078s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_014768_generic_interval_tests-T-defqtvc__00.smt2 |    0.078s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_19_150_fp_overflow_check___00.smt2 |    0.078s | 19.58MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_104_22_assert___00.smt2 |    0.078s | 20.048MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1158_47_precondition___00.smt2 |    0.079s | 19.796MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_7_19_range_check___00.smt2 |    0.079s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero__run.ads_24_19_postcondition___00.smt2 |    0.079s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e30a85_generic_float_tests-T-defqtvc__00.smt2 |    0.079s | 19.716MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_16_22_assert___00.smt2 |    0.080s | 20.224MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_dc2c61_generic_interval_tests-T-defqtvc__00.smt2 |    0.080s | 19.8MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_30_19_assert___00.smt2 |    0.080s | 20.104MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_23_43_division_check___00.smt2 |    0.080s | 20.12MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_22_22_assert___00.smt2 |    0.081s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O430-013__return_unchecked_conversion__prover_crash.adb_14_23_range_check___00.smt2 |    0.081s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__discriminant_check.adb_19_8_discriminant_check___00.smt2 |    0.081s | 20.008MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S603-051__dimensions__dimensions.ads_377_7_fp_overflow_check___00.smt2 |    0.081s | 19.748MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA20-061__flow_variable_constant__basic_contracts.adb_10_22_assert___00.smt2 |    0.081s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_6_31_overflow_check___00.smt2 |    0.081s | 19.98MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S603-051__dimensions__image_golf_hole.adb_19_18_image_golf_hole.adb_32_10_predicate_check___00.smt2 |    0.081s | 20.112MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q522-022__codepeer__proof.adb_25_15_precondition___00.smt2 |    0.082s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_377_30_range_check___00.smt2 |    0.082s | 20.352MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_21_fp_overflow_check___00.smt2 |    0.082s | 19.876MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_20_34_overflow_check___00.smt2 |    0.082s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_75_22_assert___00.smt2 |    0.082s | 20.12MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_627_26_range_check___00.smt2 |    0.082s | 19.904MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_45_16_division_check___00.smt2 |    0.082s | 19.652MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__division_by_zero.adb_39_14_division_check___00.smt2 |    0.082s | 19.98MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e7ad50_generic_interval_tests-T-defqtvc__00.smt2 |    0.083s | 20.112MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_17_62_contract_case___00.smt2 |    0.083s | 19.968MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level2__hard_stuff.adb_12_22_assert___00.smt2 |    0.083s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.ads_15_10_postcondition___00.smt2 |    0.083s | 19.8MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_36_14_postcondition___00.smt2 |    0.083s | 20.36MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_50886f_generic_interval_tests-T-defqtvc__00.smt2 |    0.083s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_fd32b1_generic_interval_tests-T-defqtvc__00.smt2 |    0.083s | 20.152MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N121-026__nonlinear__nonlinear.adb_11_19_assert___00.smt2 |    0.084s | 19.652MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB23-014__float_literal__u.adb_12_20_assert___00.smt2 |    0.084s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_42_22_assert___00.smt2 |    0.084s | 19.832MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P310-021__proof_float_remainder__foo.adb_16_17_range_check___00.smt2 |    0.084s | 19.612MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_22_31_overflow_check___00.smt2 |    0.084s | 19.892MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__assertionproperties.adb_36_22_assert___00.smt2 |    0.084s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_19_150_division_check___00.smt2 |    0.084s | 19.608MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_19_22_assert___00.smt2 |    0.084s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_30_32_division_check___00.smt2 |    0.084s | 20.024MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P620-034__float_out_subtype__get_out_subtype.adb_27_58_range_check___00.smt2 |    0.084s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_5_31_overflow_check___00.smt2 |    0.085s | 19.548MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f4b86f_generic_interval_tests-T-defqtvc__00.smt2 |    0.085s | 19.892MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB23-014__float_literal__u.adb_13_20_assert___00.smt2 |    0.085s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.adb_11_43_range_check___00.smt2 |    0.085s | 20.052MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O220-024__floats__test_pack.ads_14_42_fp_overflow_check___00.smt2 |    0.085s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_49_4_precondition___00.smt2 |    0.085s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level2__hard_stuff.adb_7_22_assert___00.smt2 |    0.085s | 19.664MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_8_8_refined_post___00.smt2 |    0.085s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB25-022__exp__gp_exp.adb_7_11_fp_overflow_check___00.smt2 |    0.085s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_60_4_precondition___00.smt2 |    0.085s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_30_57_range_check___00.smt2 |    0.085s | 20.368MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_de2268_generic_float_tests-T-defqtvc__00.smt2 |    0.085s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_37_19_assert___00.smt2 |    0.085s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_5_19_assert___00.smt2 |    0.086s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_41a5f2_generic_float_tests-T-defqtvc__00.smt2 |    0.086s | 19.728MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_20_36_range_check___00.smt2 |    0.086s | 19.904MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_10_54_fp_overflow_check___00.smt2 |    0.086s | 20.008MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_14d53b_generic_interval_tests-T-defqtvc__00.smt2 |    0.086s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_22_19_assert___00.smt2 |    0.086s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3ce9bc_generic_interval_tests-T-defqtvc__00.smt2 |    0.086s | 19.656MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a2c9b8_generic_interval_tests-T-defqtvc__00.smt2 |    0.086s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_28_34_overflow_check___00.smt2 |    0.086s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_390_22_overflow_check___00.smt2 |    0.087s | 20.116MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1041_52_precondition___00.smt2 |    0.087s | 19.772MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_64_25_assert___00.smt2 |    0.087s | 20.14MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_376_22_overflow_check___00.smt2 |    0.087s | 20.124MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6f649f_generic_float_tests-T-defqtvc__00.smt2 |    0.087s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_16_22_assert___00.smt2 |    0.087s | 20.136MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/TU__depends_legal__depends_legal_2.adb_48_12_discriminant_check___00.smt2 |    0.087s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c522c9_generic_interval_tests-T-defqtvc__00.smt2 |    0.087s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_457_42_fp_overflow_check___00.smt2 |    0.087s | 19.76MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_60_39_contract_case___00.smt2 |    0.087s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_122_14_range_check___00.smt2 |    0.087s | 20.616MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_658b29_generic_interval_tests-T-defqtvc__00.smt2 |    0.087s | 19.636MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b9b5ec_generic_interval_tests-T-defqtvc__00.smt2 |    0.088s | 19.792MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_52_19_assert___00.smt2 |    0.088s | 20.156MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0f9517_generic_float_tests-T-defqtvc__00.smt2 |    0.088s | 19.768MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M122-006__assign2__p.adb_8_9_discriminant_check___00.smt2 |    0.088s | 20.076MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_10_20_fp_overflow_check___00.smt2 |    0.088s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_11_35_overflow_check___00.smt2 |    0.088s | 19.936MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_34_14_range_check___00.smt2 |    0.088s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c12b1d_generic_float_tests-T-defqtvc__00.smt2 |    0.088s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_41_35_fp_overflow_check___00.smt2 |    0.088s | 20.056MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_13_142_fp_overflow_check___00.smt2 |    0.088s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_2.adb_16_18_overflow_check___00.smt2 |    0.088s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b06d51_generic_interval_tests-T-defqtvc__00.smt2 |    0.088s | 19.824MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_28_22_assert___00.smt2 |    0.088s | 19.72MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB23-014__float_monotonicity__add.adb_10_16_postcondition___00.smt2 |    0.088s | 20.196MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_35_14_range_check___00.smt2 |    0.088s | 20.296MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_46_14_postcondition___00.smt2 |    0.089s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_363_68_overflow_check___00.smt2 |    0.089s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_71_17_predicate_check___00.smt2 |    0.089s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.adb_10_51_range_check___00.smt2 |    0.089s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P310-021__proof_float_remainder__foo.adb_9_17_range_check___00.smt2 |    0.089s | 19.98MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_9_58_fp_overflow_check___00.smt2 |    0.089s | 20.008MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_492bd7_generic_float_tests-T-defqtvc__00.smt2 |    0.089s | 20.524MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P830-027__flow_variables_in_float__f.adb_4_12_range_check___00.smt2 |    0.090s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_98_75_division_check___00.smt2 |    0.090s | 20.34MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_43_21_fp_overflow_check___00.smt2 |    0.090s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_93_14_range_check___00.smt2 |    0.090s | 20.364MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_29_21_unreachable_branch___00.smt2 |    0.090s | 20.22MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_30_57_fp_overflow_check___00.smt2 |    0.090s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_72685b_generic_float_tests-T-defqtvc__00.smt2 |    0.090s | 19.808MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_218eda_generic_float_tests-T-defqtvc__00.smt2 |    0.090s | 19.896MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__call_sample2.adb_23_7_call_sample2.adb_27_4_precondition___00.smt2 |    0.090s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_4.adb_40_19_postcondition___00.smt2 |    0.091s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__sample.ads_37_17_postcondition___00.smt2 |    0.091s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__ce__counter_examples.adb_9_16_fp_overflow_check___00.smt2 |    0.091s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_53b78c_generic_interval_tests-T-defqtvc__00.smt2 |    0.091s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_7c2c0b_generic_float_tests-T-defqtvc__00.smt2 |    0.091s | 19.972MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_46_22_assert___00.smt2 |    0.091s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_20_32_range_check___00.smt2 |    0.091s | 19.956MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f1b856_generic_interval_tests-T-defqtvc__00.smt2 |    0.091s | 20.016MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_facb24_generic_interval_tests-T-defqtvc__00.smt2 |    0.091s | 19.768MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_76_22_assert___00.smt2 |    0.091s | 20.088MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_float.adb_8_14_postcondition___00.smt2 |    0.092s | 20.092MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_15_12_postcondition___00.smt2 |    0.092s | 19.884MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_26_22_assert___00.smt2 |    0.092s | 20.008MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_11_28_range_check___00.smt2 |    0.092s | 19.748MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_50_19_precondition___00.smt2 |    0.092s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_37_54_fp_overflow_check___00.smt2 |    0.092s | 20.144MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_161_13_precondition___00.smt2 |    0.092s | 20.088MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_59_14_postcondition___00.smt2 |    0.092s | 20.384MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB23-014__float_monotonicity__add.adb_13_4_precondition___00.smt2 |    0.092s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_49c130_generic_float_tests-T-defqtvc__00.smt2 |    0.092s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__original_sample.ads_39_17_postcondition___00.smt2 |    0.092s | 20.2MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_3_7_overflow_check___00.smt2 |    0.092s | 19.708MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_33_14_division_check___00.smt2 |    0.092s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_637_21_precondition___00.smt2 |    0.093s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_76_22_assert___00.smt2 |    0.093s | 20.34MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b94afa_generic_interval_tests-T-defqtvc__00.smt2 |    0.093s | 19.984MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_10_25_assert___00.smt2 |    0.093s | 19.996MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e982c9_generic_interval_tests-T-defqtvc__00.smt2 |    0.093s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_17_24_fp_overflow_check___00.smt2 |    0.093s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_23_17_range_check___00.smt2 |    0.093s | 19.924MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__biaseddivide.ads_19_20_fp_overflow_check___00.smt2 |    0.093s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_44_14_postcondition___00.smt2 |    0.094s | 20.004MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_69_17_predicate_check___00.smt2 |    0.094s | 20.088MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_45_16_fp_overflow_check___00.smt2 |    0.094s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1d5454_generic_float_tests-T-defqtvc__00.smt2 |    0.094s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0d33ae_generic_float_tests-T-defqtvc__00.smt2 |    0.094s | 19.712MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_10_29_fp_overflow_check___00.smt2 |    0.094s | 19.892MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_18_18_fp_overflow_check2___00.smt2 |    0.094s | 20.06MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_36_17_range_check___00.smt2 |    0.094s | 20.116MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_13_23_division_check2___00.smt2 |    0.094s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8f72d3_generic_float_tests-T-defqtvc__00.smt2 |    0.094s | 19.808MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3f27e3_generic_float_tests-T-defqtvc__00.smt2 |    0.094s | 19.908MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_20_37_fp_overflow_check2___00.smt2 |    0.094s | 20.324MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_45_31_overflow_check___00.smt2 |    0.095s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_13_18_fp_overflow_check___00.smt2 |    0.095s | 19.88MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_9_35_range_check___00.smt2 |    0.095s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_16_14_fp_overflow_check___00.smt2 |    0.095s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_28_19_postcondition___00.smt2 |    0.096s | 20.076MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_81_22_assert___00.smt2 |    0.096s | 20.54MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_10_29_overflow_check___00.smt2 |    0.096s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_21_51_fp_overflow_check___00.smt2 |    0.096s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P620-034__float_out_subtype__get_out_subtype.adb_27_58_range_check___01.smt2 |    0.096s | 19.904MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_20_21_fp_overflow_check___00.smt2 |    0.096s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_31_22_assert___00.smt2 |    0.096s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_15_fp_overflow_check___00.smt2 |    0.096s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8f1e69_generic_float_tests-T-defqtvc__00.smt2 |    0.096s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_31_22_assert___00.smt2 |    0.096s | 19.94MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_607_25_range_check___00.smt2 |    0.096s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_363_29_range_check___00.smt2 |    0.096s | 20.096MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.ads_38_19_postcondition___00.smt2 |    0.097s | 20.132MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_2cfc0a_generic_interval_tests-T-defqtvc__00.smt2 |    0.097s | 19.98MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_14_19_assert___00.smt2 |    0.097s | 20.096MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_40_8_discriminant_check___00.smt2 |    0.097s | 20.26MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1068_47_precondition___00.smt2 |    0.097s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.ads_30_19_postcondition___00.smt2 |    0.097s | 19.62MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c1c2bc_generic_float_tests-T-defqtvc__00.smt2 |    0.097s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_25_26_fp_overflow_check___00.smt2 |    0.097s | 20.072MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_59_38_contract_case___00.smt2 |    0.097s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__original_sample.ads_38_35_fp_overflow_check___00.smt2 |    0.097s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_73_17_predicate_check___00.smt2 |    0.097s | 20.072MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_34_17_range_check___00.smt2 |    0.098s | 19.708MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_60_15_range_check___00.smt2 |    0.098s | 20.336MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_219_14_precondition___00.smt2 |    0.098s | 19.824MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8c6282_generic_float_tests-T-defqtvc__00.smt2 |    0.098s | 19.824MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_8_54_challenges.adb_15_14_challenges.adb_24_14_challenges.adb_33_29_challenges.adb_38_10_fp_overflow_check___00.smt2 |    0.098s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_10_24_overflow_check___00.smt2 |    0.098s | 19.696MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_8_19_assert___00.smt2 |    0.098s | 20.32MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_142_14_precondition___00.smt2 |    0.098s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_62_4_precondition___00.smt2 |    0.098s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_21_34_fp_overflow_check___00.smt2 |    0.098s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_92_132_fp_overflow_check___00.smt2 |    0.098s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1d4733_generic_float_tests-T-defqtvc__00.smt2 |    0.099s | 19.8MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_01f2bc_generic_float_tests-T-defqtvc__00.smt2 |    0.099s | 19.808MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_12_11_postcondition___00.smt2 |    0.099s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__call_sample.adb_6_4_precondition___00.smt2 |    0.100s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_45_17_range_check___00.smt2 |    0.100s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_91_41_fp_overflow_check___00.smt2 |    0.100s | 19.972MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_float.adb_17_19_assert___00.smt2 |    0.100s | 20.304MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_52_19_precondition___00.smt2 |    0.100s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__sample.ads_57_17_postcondition___00.smt2 |    0.100s | 19.796MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_11_55_overflow_check___00.smt2 |    0.100s | 20.016MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_42_19_assert___00.smt2 |    0.100s | 19.996MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.ads_15_19_postcondition___00.smt2 |    0.101s | 19.744MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_29fea4_generic_interval_tests-T-defqtvc__00.smt2 |    0.101s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_471921_generic_float_tests-T-defqtvc__00.smt2 |    0.101s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O224-020__constant_aggr__package_1.adb_11_29_fp_overflow_check___00.smt2 |    0.101s | 19.876MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_57b4e3_generic_float_tests-T-defqtvc__00.smt2 |    0.101s | 19.696MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_9_58_division_check___00.smt2 |    0.101s | 20.004MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_cfc699_generic_float_tests-T-defqtvc__00.smt2 |    0.101s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_2.adb_32_32_range_check___00.smt2 |    0.101s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O303-041__flow_pure_implies_null_global__foo.adb_5_9_precondition___00.smt2 |    0.101s | 19.816MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_23_22_assert___00.smt2 |    0.102s | 20.076MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_17_fp_overflow_check___00.smt2 |    0.102s | 19.744MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N703-010__float_conversion__foo.adb_13_15_range_check___00.smt2 |    0.102s | 20.088MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_26_22_assert___00.smt2 |    0.103s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_31_fp_overflow_check___00.smt2 |    0.103s | 19.728MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_7_20_fp_overflow_check___00.smt2 |    0.103s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_105_22_assert___00.smt2 |    0.103s | 19.8MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_7_19_assert___00.smt2 |    0.103s | 19.812MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_391_30_range_check___00.smt2 |    0.103s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_23_16_postcondition___00.smt2 |    0.103s | 20.068MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_443_22_overflow_check___00.smt2 |    0.103s | 20.104MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_13_31_overflow_check___00.smt2 |    0.103s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_441ad2_generic_float_tests-T-defqtvc__00.smt2 |    0.104s | 19.7MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_22_22_assert___00.smt2 |    0.104s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_470_22_fp_overflow_check___00.smt2 |    0.104s | 19.772MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.adb_10_42_precondition___00.smt2 |    0.104s | 19.948MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b7f9fd_generic_float_tests-T-defqtvc__00.smt2 |    0.104s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB04-007__float_conversion__floatround.adb_11_15_precondition___00.smt2 |    0.104s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_29_22_discriminant_check___00.smt2 |    0.105s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_151_14_range_check___00.smt2 |    0.105s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_4_37_range_check___00.smt2 |    0.105s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_86_22_assert___00.smt2 |    0.105s | 19.968MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_21_22_assert___00.smt2 |    0.105s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_9b412c_generic_float_tests-T-defqtvc__00.smt2 |    0.105s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_283cca_generic_float_tests-T-defqtvc__00.smt2 |    0.105s | 19.62MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1253ee_generic_interval_tests-T-defqtvc__00.smt2 |    0.106s | 19.7MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.ads_13_18_postcondition___00.smt2 |    0.106s | 19.808MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1176_47_precondition___00.smt2 |    0.107s | 19.728MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.ads_25_19_postcondition___00.smt2 |    0.107s | 20.124MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_9_19_assert___00.smt2 |    0.107s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_41_21_fp_overflow_check___00.smt2 |    0.107s | 19.608MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_349_47_fp_overflow_check___00.smt2 |    0.107s | 19.636MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q906-010__float_volatile__copy_values.adb_8_25_fp_overflow_check___00.smt2 |    0.107s | 19.876MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_30_101_fp_overflow_check___00.smt2 |    0.107s | 19.904MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level3__hard_stuff.adb_21_22_assert___00.smt2 |    0.107s | 19.836MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_31_58_fp_overflow_check___00.smt2 |    0.108s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_20_29_discriminant_check___00.smt2 |    0.108s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_11_33_loop_invariant_preserv2___00.smt2 |    0.108s | 20.168MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_77_22_assert___00.smt2 |    0.108s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_23_19_fp_overflow_check___00.smt2 |    0.108s | 19.832MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_27_14_postcondition___00.smt2 |    0.108s | 20.116MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a0c4ad_generic_float_tests-T-defqtvc__00.smt2 |    0.109s | 20.264MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6fdf6d_generic_float_tests-T-defqtvc__00.smt2 |    0.109s | 19.816MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.ads_15_19_postcondition___00.smt2 |    0.109s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_38_19_assert___00.smt2 |    0.109s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_6_12_overflow_check___00.smt2 |    0.109s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P906-011__exp_division__expo.adb_6_11_fp_overflow_check___00.smt2 |    0.109s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_4110a0_generic_interval_tests-T-defqtvc__00.smt2 |    0.110s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_23_45_fp_overflow_check___00.smt2 |    0.110s | 20.128MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1050_47_precondition___00.smt2 |    0.110s | 19.608MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB25-022__exp__gp_exp.adb_6_11_overflow_check___00.smt2 |    0.110s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_d7746d_generic_float_tests-T-defqtvc__00.smt2 |    0.110s | 19.848MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e70870_generic_float_tests-T-defqtvc__00.smt2 |    0.111s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_bce863_generic_float_tests-T-defqtvc__00.smt2 |    0.111s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_19_62_contract_case___00.smt2 |    0.111s | 19.936MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_8_31_overflow_check___00.smt2 |    0.111s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M122-006__assign__p.adb_14_9_discriminant_check___00.smt2 |    0.111s | 20.356MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_79bf65_generic_interval_tests-T-defqtvc__00.smt2 |    0.111s | 19.872MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_39_45_division_check___00.smt2 |    0.111s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_19_38_loop_invariant_init___00.smt2 |    0.112s | 19.964MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_36_53_fp_overflow_check___00.smt2 |    0.112s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_36_22_assert___00.smt2 |    0.112s | 20.3MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_17_24_division_check___00.smt2 |    0.112s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f38e09_generic_float_tests-T-defqtvc__00.smt2 |    0.112s | 19.712MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_163_22_assert___00.smt2 |    0.113s | 20.332MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_113_14_range_check___00.smt2 |    0.114s | 19.836MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_fd3c3b_generic_interval_tests-T-defqtvc__00.smt2 |    0.114s | 19.632MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_48_19_precondition___00.smt2 |    0.114s | 20.088MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_04ae02_generic_float_tests-T-defqtvc__00.smt2 |    0.114s | 19.916MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_7_31_overflow_check___00.smt2 |    0.114s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB16-021__float_range__test_float.adb_5_19_assert___00.smt2 |    0.115s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b1475f_generic_interval_tests-T-defqtvc__00.smt2 |    0.115s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_18_26_precondition___00.smt2 |    0.115s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b72bc0_generic_interval_tests-T-defqtvc__00.smt2 |    0.116s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_29_22_assert___00.smt2 |    0.116s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_14_31_overflow_check___00.smt2 |    0.116s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_7_25_division_check___00.smt2 |    0.116s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_35_22_assert___00.smt2 |    0.116s | 20.272MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_204f1e_generic_interval_tests-T-defqtvc__00.smt2 |    0.116s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_20_45_range_check___00.smt2 |    0.116s | 20.04MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.ads_15_37_fp_overflow_check___00.smt2 |    0.116s | 20.048MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_4.adb_40_32_range_check___00.smt2 |    0.117s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_30_31_overflow_check___00.smt2 |    0.117s | 20.112MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_67_17_predicate_check___00.smt2 |    0.117s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_29_14_postcondition___00.smt2 |    0.117s | 20.576MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6ab862_generic_float_tests-T-defqtvc__00.smt2 |    0.117s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f4d109_generic_interval_tests-T-defqtvc__00.smt2 |    0.118s | 19.632MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_60_18_range_check___00.smt2 |    0.118s | 20.056MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N703-010__float_conversion__foo.adb_23_15_range_check___00.smt2 |    0.118s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__abs_controller_oem_with_property.adb_56_43_fp_overflow_check___00.smt2 |    0.119s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f7e0e0_generic_interval_tests-T-defqtvc__00.smt2 |    0.119s | 19.572MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_31_47_range_check___00.smt2 |    0.119s | 20.24MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_62_14_postcondition___00.smt2 |    0.119s | 20.36MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O312-037__flow_pure_subprograms__call.adb_22_51_range_check___00.smt2 |    0.120s | 20.032MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA20-061__flow_variable_constant__basic_contracts.adb_12_18_fp_overflow_check___00.smt2 |    0.120s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b5cd90_generic_float_tests-T-defqtvc__00.smt2 |    0.120s | 19.616MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_6_29_range_check___00.smt2 |    0.120s | 19.884MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0b989e_generic_float_tests-T-defqtvc__00.smt2 |    0.121s | 19.692MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_61_19_assert___00.smt2 |    0.122s | 20.172MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__original_sample.ads_59_17_postcondition___00.smt2 |    0.123s | 19.7MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_90cfbd_generic_float_tests-T-defqtvc__00.smt2 |    0.123s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_7_9_discriminant_check___00.smt2 |    0.124s | 20.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1167_52_precondition___00.smt2 |    0.125s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ff055b_generic_interval_tests-T-defqtvc__00.smt2 |    0.125s | 19.668MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_121_13_precondition___00.smt2 |    0.126s | 20.576MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_42_46_range_check___00.smt2 |    0.126s | 20.184MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_21_22_fp_overflow_check___00.smt2 |    0.127s | 20.34MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P830-027__flow_variables_in_float__f.adb_3_12_range_check___00.smt2 |    0.128s | 20.18MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c6aff8_generic_float_tests-T-defqtvc__00.smt2 |    0.128s | 19.696MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_20_12_postcondition___00.smt2 |    0.128s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_13_24_fp_overflow_check___00.smt2 |    0.128s | 20.056MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_12_58_fp_overflow_check___00.smt2 |    0.128s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_47_15_range_check___00.smt2 |    0.129s | 19.832MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_38_48_fp_overflow_check___00.smt2 |    0.129s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e2dbad_generic_interval_tests-T-defqtvc__00.smt2 |    0.130s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_9_25_assert___00.smt2 |    0.130s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_50_4_precondition___00.smt2 |    0.130s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_14_22_assert___00.smt2 |    0.131s | 20.052MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level2__hard_stuff.adb_20_52_division_check___00.smt2 |    0.132s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e1269d_generic_float_tests-T-defqtvc__00.smt2 |    0.132s | 19.636MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_349_22_fp_overflow_check___00.smt2 |    0.132s | 19.844MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_11_19_assert___00.smt2 |    0.132s | 20.084MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__discriminant_check.adb_14_15_discriminant_check___00.smt2 |    0.132s | 19.896MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_90d7ec_generic_interval_tests-T-defqtvc__00.smt2 |    0.133s | 19.88MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_2cf678_generic_float_tests-T-defqtvc__00.smt2 |    0.134s | 20.328MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_617_26_range_check___00.smt2 |    0.134s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_29_16_postcondition___00.smt2 |    0.134s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_37_53_fp_overflow_check___00.smt2 |    0.135s | 19.968MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_12_29_division_check___00.smt2 |    0.135s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__abs_controller_oem_with_property.adb_88_22_assert___00.smt2 |    0.136s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_028c17_homothetical-T-defqtvc__00.smt2 |    0.136s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB04-017__float__p.adb_4_13_range_check___00.smt2 |    0.137s | 19.824MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_64_14_range_check___00.smt2 |    0.137s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_6_19_assert___00.smt2 |    0.138s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_70_22_assert___00.smt2 |    0.138s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_7_19_assert___00.smt2 |    0.138s | 19.824MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_28_25_fp_overflow_check___00.smt2 |    0.138s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.ads_20_19_postcondition___00.smt2 |    0.138s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_12_48_challenges.adb_24_14_challenges.adb_33_29_challenges.adb_38_10_range_check___00.smt2 |    0.139s | 20.12MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB16-021__float_range__test_float.adb_6_19_assert___00.smt2 |    0.139s | 20.108MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__division_by_zero.adb_29_14_division_check___00.smt2 |    0.139s | 19.696MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_16_25_assert2___00.smt2 |    0.139s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_18.adb_7_19_fp_overflow_check___00.smt2 |    0.139s | 20.052MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_63_25_assert___00.smt2 |    0.139s | 20.004MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_12_23_fp_overflow_check___00.smt2 |    0.139s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_55_14_range_check___00.smt2 |    0.140s | 20.092MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_37_32_fp_overflow_check___00.smt2 |    0.140s | 20.136MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M122-006__assign2__p.adb_14_9_discriminant_check___00.smt2 |    0.140s | 20.128MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_65_25_assert___00.smt2 |    0.142s | 19.832MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_9cfb3a_generic_interval_tests-T-defqtvc__00.smt2 |    0.142s | 20.052MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__biaseddivide.adb_24_16_fp_overflow_check___00.smt2 |    0.144s | 19.76MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_647_14_precondition___00.smt2 |    0.145s | 19.596MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB04-017__float__p.adb_3_9_range_check___00.smt2 |    0.145s | 19.672MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_6_14_fp_overflow_check___00.smt2 |    0.145s | 20.004MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_336_51_fp_overflow_check___00.smt2 |    0.145s | 19.588MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_36_19_assert___00.smt2 |    0.145s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O723-005__generic_in_entry__a-tiflio.ads_78_8_p.adb_9_10_precondition___00.smt2 |    0.145s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_27_32_fp_overflow_check___00.smt2 |    0.146s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_28_32_fp_overflow_check___00.smt2 |    0.146s | 19.908MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_63_62_overflow_check___00.smt2 |    0.147s | 20.052MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_20_22_assert___00.smt2 |    0.147s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_57_26_range_check___00.smt2 |    0.147s | 19.628MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a83df9_generic_interval_tests-T-defqtvc__00.smt2 |    0.147s | 19.764MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b9c8dc_generic_float_tests-T-defqtvc__00.smt2 |    0.147s | 19.82MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_25_22_assert___00.smt2 |    0.147s | 20.116MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1a226b_generic_float_tests-T-defqtvc__00.smt2 |    0.148s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_904c31_generic_float_tests-T-defqtvc__00.smt2 |    0.148s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_41_19_assert___00.smt2 |    0.148s | 19.868MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_17_division_check___00.smt2 |    0.148s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N121-026__nonlinear__nonlinear.adb_10_16_fp_overflow_check___00.smt2 |    0.148s | 19.648MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f9f0b1_generic_interval_tests-T-defqtvc__00.smt2 |    0.148s | 19.768MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_23_30_overflow_check___00.smt2 |    0.148s | 20.284MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5c42fa_generic_interval_tests-T-defqtvc__00.smt2 |    0.148s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_28_21_fp_overflow_check___00.smt2 |    0.149s | 19.996MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_39_19_assert___00.smt2 |    0.149s | 20.084MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S320-040__flow_blocking__a-tiflio.ads_78_8_p.adb_28_7_precondition___00.smt2 |    0.150s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_24_22_assert___00.smt2 |    0.150s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_62_45_overflow_check___00.smt2 |    0.151s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_42_14_postcondition___00.smt2 |    0.151s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_69_41_fp_overflow_check___00.smt2 |    0.151s | 20.368MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_23_8_discriminant_check___00.smt2 |    0.151s | 20.28MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f5b2b3_generic_interval_tests-T-defqtvc__00.smt2 |    0.151s | 19.892MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_14_29_division_check___00.smt2 |    0.151s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_2.adb_19_18_overflow_check___00.smt2 |    0.151s | 19.636MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_15_24_fp_overflow_check___00.smt2 |    0.151s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_12_30_fp_overflow_check___00.smt2 |    0.151s | 19.928MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_132_13_precondition___00.smt2 |    0.151s | 19.86MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a2c713_generic_interval_tests-T-defqtvc__00.smt2 |    0.152s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f00b23_generic_interval_tests-T-defqtvc__00.smt2 |    0.152s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_377_69_overflow_check___00.smt2 |    0.152s | 19.66MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_15_24_range_check___00.smt2 |    0.152s | 20.06MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_cc80a4_generic_float_tests-T-defqtvc__00.smt2 |    0.152s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_9_22_assert___00.smt2 |    0.152s | 20.1MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_bee7c4_generic_float_tests-T-defqtvc__00.smt2 |    0.152s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_45_22_range_check___00.smt2 |    0.152s | 19.892MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_150_13_precondition___00.smt2 |    0.152s | 19.836MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_19_50_range_check___00.smt2 |    0.152s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_2b1e11_generic_float_tests-T-defqtvc__00.smt2 |    0.152s | 19.652MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_10_19_assert___00.smt2 |    0.152s | 19.764MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_23_26_fp_overflow_check___00.smt2 |    0.152s | 19.9MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_470_47_fp_overflow_check___00.smt2 |    0.152s | 19.616MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_17_14_discriminant_check___00.smt2 |    0.153s | 20.108MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__challenges.adb_8_37_challenges.adb_15_14_challenges.adb_24_14_challenges.adb_33_29_challenges.adb_38_10_precondition___00.smt2 |    0.153s | 20.38MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_21_44_fp_overflow_check___00.smt2 |    0.153s | 20.096MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__abs_controller_oem_with_property.adb_33_22_assert___00.smt2 |    0.153s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_db64dc_generic_float_tests-T-defqtvc__00.smt2 |    0.153s | 20.0MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_27_22_assert___00.smt2 |    0.153s | 19.852MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_394d11_generic_interval_tests-T-defqtvc__00.smt2 |    0.154s | 19.768MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB23-014__float_monotonicity__mul.adb_10_16_postcondition___00.smt2 |    0.154s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_84_14_precondition___00.smt2 |    0.154s | 20.112MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_10_41_fp_overflow_check___00.smt2 |    0.154s | 19.872MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA20-061__flow_variable_constant__basic_contracts.adb_6_17_postcondition___00.smt2 |    0.154s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_13_19_assert___00.smt2 |    0.154s | 19.748MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__assertionproperties.adb_43_22_assert___00.smt2 |    0.155s | 19.788MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level3__hard_stuff.adb_11_14_fp_overflow_check___00.smt2 |    0.155s | 20.192MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC08-035__missing_range_check_on_out_param__demo.adb_6_7_demo.adb_14_7_range_check___00.smt2 |    0.155s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6f02ee_generic_float_tests-T-defqtvc__00.smt2 |    0.155s | 19.604MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_19_24_overflow_check2___00.smt2 |    0.155s | 19.996MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_93_75_contract_case___00.smt2 |    0.155s | 19.98MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB02-004__inherited_sub__main.adb_9_24_range_check___00.smt2 |    0.155s | 19.908MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_470_56_fp_overflow_check___00.smt2 |    0.155s | 19.6MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_18_54_fp_overflow_check___00.smt2 |    0.156s | 19.752MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_17_22_assert___00.smt2 |    0.156s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3eabed_generic_float_tests-T-defqtvc__00.smt2 |    0.157s | 19.632MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_30_21_unreachable_branch___00.smt2 |    0.157s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_843777_generic_float_tests-T-defqtvc__00.smt2 |    0.157s | 19.704MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__biaseddivide.ads_19_20_division_check___00.smt2 |    0.157s | 19.84MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_38_22_assert___00.smt2 |    0.158s | 20.004MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_26_24_overflow_check___00.smt2 |    0.158s | 19.72MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_18_22_assert___00.smt2 |    0.158s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_15_33_loop_invariant_preserv2___00.smt2 |    0.158s | 19.836MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_20_37_overflow_check___00.smt2 |    0.158s | 19.956MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_362_22_overflow_check___00.smt2 |    0.158s | 19.976MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_19_21_fp_overflow_check___00.smt2 |    0.158s | 20.044MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_18.adb_4_16_postcondition___00.smt2 |    0.159s | 19.856MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_29_32_fp_overflow_check___00.smt2 |    0.159s | 19.724MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_10_15_range_check___00.smt2 |    0.159s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/TU__depends_legal__depends_legal_2.adb_43_15_discriminant_check___00.smt2 |    0.159s | 19.904MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_29_17_range_check___00.smt2 |    0.159s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_49_14_postcondition___00.smt2 |    0.159s | 19.888MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_92_13_precondition___00.smt2 |    0.159s | 19.592MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ddd17d_generic_float_tests-T-defqtvc__00.smt2 |    0.159s | 19.896MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero__run.ads_29_19_postcondition___00.smt2 |    0.160s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_d30160_generic_interval_tests-T-defqtvc__00.smt2 |    0.160s | 19.816MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level3__hard_stuff.adb_29_25_assert___00.smt2 |    0.160s | 20.136MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_235444_generic_float_tests-T-defqtvc__00.smt2 |    0.160s | 19.864MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_21_22_assert___00.smt2 |    0.160s | 20.08MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6a7512_generic_float_tests-T-defqtvc__00.smt2 |    0.160s | 19.664MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_72f01f_generic_float_tests-T-defqtvc__00.smt2 |    0.160s | 19.912MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_208_47_precondition___00.smt2 |    0.161s | 19.64MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_61b4e3_generic_float_tests-T-defqtvc__00.smt2 |    0.161s | 19.644MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_1.adb_30_32_range_check___00.smt2 |    0.161s | 19.868MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_41_14_postcondition___00.smt2 |    0.161s | 20.156MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q522-022__codepeer__proof.adb_11_15_precondition___00.smt2 |    0.161s | 19.684MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M122-006__assign__p.adb_8_9_discriminant_check___00.smt2 |    0.161s | 20.108MiB| unknown | 0 |  |  |