# .

* SAT 58
* UNSAT 551
* TIMEOUT 185
* UNKNOWN 1

* 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 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_7_25_division_check___00.smt2 |    0.024s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_134_22_assert___00.smt2 |    0.028s | 20.032MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_11_33_loop_invariant_init2___00.smt2 |    0.028s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_60_39_contract_case___00.smt2 |    0.028s | 20.36MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1185_52_precondition___00.smt2 |    0.029s | 20.932MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6ab862_generic_float_tests-T-defqtvc__00.smt2 |    0.029s | 20.788MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1041_52_precondition___00.smt2 |    0.030s | 21.004MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_10_11_fp_overflow_check___00.smt2 |    0.032s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_10_15_range_check___00.smt2 |    0.032s | 19.912MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_31_22_assert___00.smt2 |    0.032s | 19.556MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_60_4_precondition___00.smt2 |    0.032s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_28_34_overflow_check___00.smt2 |    0.032s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.adb_10_52_precondition___00.smt2 |    0.033s | 19.46MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_19_150_fp_overflow_check___00.smt2 |    0.033s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_8_11_fp_overflow_check___00.smt2 |    0.033s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_19_74_range_check___00.smt2 |    0.034s | 19.696MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_60_22_range_check___00.smt2 |    0.034s | 21.44MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/TU__depends_legal__depends_legal_2.adb_43_15_discriminant_check___00.smt2 |    0.034s | 19.84MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_52_19_precondition___00.smt2 |    0.034s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_12_11_fp_overflow_check___00.smt2 |    0.035s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_69_17_predicate_check___00.smt2 |    0.035s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P310-021__proof_float_remainder__foo.adb_9_17_division_check___00.smt2 |    0.035s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_17_division_check___00.smt2 |    0.035s | 19.528MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_10_24_overflow_check___00.smt2 |    0.035s | 20.392MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB04-017__float__p.adb_3_9_range_check___00.smt2 |    0.035s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__call_sample.adb_6_4_precondition___00.smt2 |    0.035s | 19.688MiB| 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.035s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_31_32_division_check___00.smt2 |    0.036s | 19.82MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB02-004__inherited_sub__main.adb_18_27_range_check___00.smt2 |    0.036s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__abs_controller_oem_with_property.adb_33_22_assert___00.smt2 |    0.036s | 19.484MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_18_17_range_check___00.smt2 |    0.036s | 19.756MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_45_16_division_check___00.smt2 |    0.036s | 20.3MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_12_23_fp_overflow_check___00.smt2 |    0.036s | 19.676MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_475293_generic_float_tests-T-defqtvc__00.smt2 |    0.037s | 20.26MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_30_21_unreachable_branch___00.smt2 |    0.037s | 19.708MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3d969b_generic_float_tests-T-defqtvc__00.smt2 |    0.037s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_41_19_assert___00.smt2 |    0.037s | 19.808MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_48_19_precondition___00.smt2 |    0.037s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_62_32_overflow_check___00.smt2 |    0.037s | 20.012MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/TU__depends_legal__depends_legal_2.adb_48_12_discriminant_check___00.smt2 |    0.037s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_53_4_precondition___00.smt2 |    0.037s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_20_22_assert___00.smt2 |    0.038s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_18_13_range_check___00.smt2 |    0.038s | 20.588MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_36_19_assert___00.smt2 |    0.038s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.adb_8_15_precondition___00.smt2 |    0.039s | 20.264MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_10_22_assert___00.smt2 |    0.039s | 20.42MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_7_31_overflow_check___00.smt2 |    0.039s | 19.56MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_9b412c_generic_float_tests-T-defqtvc__00.smt2 |    0.039s | 20.448MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e1269d_generic_float_tests-T-defqtvc__00.smt2 |    0.040s | 19.96MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1167_52_precondition___00.smt2 |    0.040s | 21.044MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_50_31_overflow_check___00.smt2 |    0.040s | 20.588MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_19_50_range_check___00.smt2 |    0.040s | 19.812MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_33_14_division_check___00.smt2 |    0.040s | 20.32MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_34db83_generic_float_tests-T-defqtvc__00.smt2 |    0.041s | 20.572MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1158_47_precondition___00.smt2 |    0.041s | 20.904MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_579cc3_generic_float_tests-T-defqtvc__00.smt2 |    0.041s | 20.888MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__division_by_zero.adb_29_14_division_check___00.smt2 |    0.041s | 20.28MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__biaseddivide.ads_19_20_fp_overflow_check___00.smt2 |    0.041s | 19.492MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N703-010__float_conversion__foo.adb_23_15_range_check___00.smt2 |    0.041s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_13_100_postcondition___00.smt2 |    0.041s | 19.88MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_17_14_discriminant_check___00.smt2 |    0.042s | 20.028MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA20-061__flow_variable_constant__basic_contracts.adb_6_17_postcondition___00.smt2 |    0.042s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_40_14_postcondition___00.smt2 |    0.042s | 20.708MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_20_45_range_check___00.smt2 |    0.042s | 20.752MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_11_19_assert___00.smt2 |    0.042s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_53_19_assert___00.smt2 |    0.043s | 21.128MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_98_75_division_check___00.smt2 |    0.043s | 21.184MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_577336_generic_float_tests-T-defqtvc__00.smt2 |    0.043s | 19.828MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_2.adb_19_18_overflow_check___00.smt2 |    0.043s | 20.96MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_4_37_range_check___00.smt2 |    0.044s | 19.5MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_20_12_postcondition___00.smt2 |    0.044s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_16abab_generic_float_tests-T-defqtvc__00.smt2 |    0.044s | 28.068MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_41_14_postcondition___00.smt2 |    0.044s | 20.644MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_13_19_assert___00.smt2 |    0.044s | 20.72MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_471921_generic_float_tests-T-defqtvc__00.smt2 |    0.045s | 20.648MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c12b1d_generic_float_tests-T-defqtvc__00.smt2 |    0.045s | 20.212MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_46_22_assert___00.smt2 |    0.045s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__assertionproperties.adb_36_22_assert___00.smt2 |    0.045s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_219_14_precondition___00.smt2 |    0.046s | 20.98MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_106_14_postcondition___00.smt2 |    0.046s | 20.872MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_6_29_range_check___00.smt2 |    0.046s | 20.372MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O303-041__flow_pure_implies_null_global__foo.adb_5_9_precondition___00.smt2 |    0.046s | 20.86MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero__run.ads_29_19_postcondition___00.smt2 |    0.047s | 19.704MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_44_14_postcondition___00.smt2 |    0.047s | 20.76MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_20_29_discriminant_check___00.smt2 |    0.047s | 20.352MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_01f2bc_generic_float_tests-T-defqtvc__00.smt2 |    0.047s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_92_70_contract_case___00.smt2 |    0.047s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_15_22_assert___00.smt2 |    0.047s | 20.58MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA20-061__flow_variable_constant__basic_contracts.adb_12_18_division_check___00.smt2 |    0.047s | 19.892MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N703-010__float_conversion__foo.adb_13_15_range_check___00.smt2 |    0.047s | 20.956MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB23-014__float_monotonicity__mul.adb_10_16_postcondition___00.smt2 |    0.048s | 19.688MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q208-056__no_denorm_on_target__compute.adb_4_20_overflow_check___00.smt2 |    0.048s | 19.536MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.ads_15_19_postcondition___00.smt2 |    0.049s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5dd164_generic_float_tests-T-defqtvc__00.smt2 |    0.049s | 20.66MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_23_22_assert___00.smt2 |    0.049s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b06d51_generic_interval_tests-T-defqtvc__00.smt2 |    0.049s | 21.98MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6fdf6d_generic_float_tests-T-defqtvc__00.smt2 |    0.050s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_45_17_fp_overflow_check___00.smt2 |    0.050s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_11_35_overflow_check___00.smt2 |    0.050s | 19.528MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_28_22_assert___00.smt2 |    0.050s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_283cca_generic_float_tests-T-defqtvc__00.smt2 |    0.050s | 23.436MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_7_9_discriminant_check___00.smt2 |    0.051s | 20.804MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_64_54_overflow_check___00.smt2 |    0.052s | 19.74MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__assertionproperties.adb_43_22_assert___00.smt2 |    0.052s | 21.472MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_6_11_fp_overflow_check___00.smt2 |    0.052s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P909-014__numerics__numerics-algo.adb_19_17_precondition___00.smt2 |    0.052s | 20.904MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_235444_generic_float_tests-T-defqtvc__00.smt2 |    0.053s | 20.768MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_16_100_postcondition___00.smt2 |    0.053s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_20_34_overflow_check___00.smt2 |    0.054s | 19.544MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_73_17_predicate_check___00.smt2 |    0.054s | 20.288MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__call_sample2.adb_13_7_call_sample2.adb_28_4_precondition___00.smt2 |    0.055s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_10_142_fp_overflow_check___00.smt2 |    0.055s | 19.624MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M122-006__assign2__p.adb_14_9_discriminant_check___00.smt2 |    0.055s | 19.672MiB| 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.056s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_67_17_predicate_check___00.smt2 |    0.056s | 19.568MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M122-006__assign2__p.adb_8_9_discriminant_check___00.smt2 |    0.056s | 19.768MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_cfc699_generic_float_tests-T-defqtvc__00.smt2 |    0.056s | 22.136MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.ads_22_20_postcondition___00.smt2 |    0.056s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e70870_generic_float_tests-T-defqtvc__00.smt2 |    0.057s | 22.1MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_40_8_discriminant_check___00.smt2 |    0.057s | 21.06MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_23_8_discriminant_check___00.smt2 |    0.057s | 20.496MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_9_58_division_check___00.smt2 |    0.057s | 21.076MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_11_55_overflow_check___00.smt2 |    0.057s | 20.876MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1a226b_generic_float_tests-T-defqtvc__00.smt2 |    0.058s | 19.98MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1d4733_generic_float_tests-T-defqtvc__00.smt2 |    0.058s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b72bc0_generic_interval_tests-T-defqtvc__00.smt2 |    0.058s | 21.172MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_50_4_precondition___00.smt2 |    0.058s | 19.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_14_29_division_check___00.smt2 |    0.058s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ca1a1e_generic_float_tests-T-defqtvc__00.smt2 |    0.058s | 20.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_39_45_division_check___00.smt2 |    0.058s | 20.828MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.ads_15_37_fp_overflow_check___00.smt2 |    0.058s | 19.716MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_float.adb_8_14_postcondition___00.smt2 |    0.059s | 22.716MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_db64dc_generic_float_tests-T-defqtvc__00.smt2 |    0.059s | 22.124MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA20-061__flow_variable_constant__basic_contracts.adb_12_18_fp_overflow_check___00.smt2 |    0.060s | 19.712MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_29_16_postcondition___00.smt2 |    0.060s | 20.348MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_15_24_division_check___00.smt2 |    0.061s | 20.024MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_16_25_assert2___00.smt2 |    0.061s | 19.664MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_24_19_postcondition___00.smt2 |    0.061s | 20.984MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.adb_10_19_precondition___00.smt2 |    0.062s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_7_19_assert___00.smt2 |    0.062s | 20.34MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_58_22_assert___00.smt2 |    0.063s | 21.404MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b9e22d_generic_float_tests-T-defqtvc__00.smt2 |    0.063s | 28.28MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_10_29_overflow_check___00.smt2 |    0.063s | 19.648MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3ce9bc_generic_interval_tests-T-defqtvc__00.smt2 |    0.063s | 21.332MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__range_check.adb_33_12_range_check___00.smt2 |    0.063s | 20.232MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__call_sample2.adb_23_7_call_sample2.adb_27_4_precondition___00.smt2 |    0.063s | 19.668MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0b989e_generic_float_tests-T-defqtvc__00.smt2 |    0.064s | 20.872MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_9_22_assert___00.smt2 |    0.064s | 20.548MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_50886f_generic_interval_tests-T-defqtvc__00.smt2 |    0.064s | 21.368MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB02-004__inherited_sub__main.adb_9_24_range_check___00.smt2 |    0.064s | 19.7MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_23_47_division_check___00.smt2 |    0.065s | 19.784MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_60_22_range_check___01.smt2 |    0.065s | 21.888MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB23-014__float_literal__u.adb_13_20_assert___00.smt2 |    0.066s | 19.748MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_11_28_range_check___00.smt2 |    0.066s | 20.528MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_49_4_precondition___00.smt2 |    0.066s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b5915a_generic_float_tests-T-defqtvc__00.smt2 |    0.067s | 20.876MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_796bf2_generic_float_tests-T-defqtvc__00.smt2 |    0.067s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_61_19_assert___00.smt2 |    0.067s | 21.64MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8222b5_generic_float_tests-T-defqtvc__00.smt2 |    0.068s | 25.056MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_60_15_range_check___00.smt2 |    0.069s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8c6282_generic_float_tests-T-defqtvc__00.smt2 |    0.069s | 20.224MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_57_24_range_check___01.smt2 |    0.069s | 21.116MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q522-022__codepeer__proof.adb_11_15_precondition___00.smt2 |    0.069s | 20.788MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_53_14_postcondition___00.smt2 |    0.069s | 20.524MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_2b1e11_generic_float_tests-T-defqtvc__00.smt2 |    0.069s | 24.836MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_de2268_generic_float_tests-T-defqtvc__00.smt2 |    0.069s | 22.18MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_275c6e_generic_float_tests-T-defqtvc__00.smt2 |    0.070s | 20.748MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_59_14_postcondition___00.smt2 |    0.070s | 21.132MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_13_46_division_check___00.smt2 |    0.070s | 20.132MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_12_29_division_check___00.smt2 |    0.070s | 19.52MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_43_19_assert___00.smt2 |    0.071s | 19.86MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e2dbad_generic_interval_tests-T-defqtvc__00.smt2 |    0.071s | 26.532MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-018__spurious_discr__useless_discr.adb_19_5_discriminant_check___00.smt2 |    0.071s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3eabed_generic_float_tests-T-defqtvc__00.smt2 |    0.072s | 21.972MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.ads_30_19_postcondition___00.smt2 |    0.072s | 19.792MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_31_27_discriminant_check___00.smt2 |    0.072s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_52_19_assert___00.smt2 |    0.073s | 20.14MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1068_47_precondition___00.smt2 |    0.073s | 19.632MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_10_30_fp_overflow_check___00.smt2 |    0.073s | 19.9MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_4aaffb_generic_float_tests-T-defqtvc__00.smt2 |    0.073s | 21.18MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_34_14_division_check___00.smt2 |    0.074s | 19.452MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_208_47_precondition___00.smt2 |    0.074s | 20.896MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.ads_20_19_postcondition___00.smt2 |    0.074s | 22.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_15_12_postcondition___00.smt2 |    0.075s | 21.672MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_29_22_discriminant_check___00.smt2 |    0.075s | 19.684MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_3_7_overflow_check___00.smt2 |    0.075s | 20.904MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_51_19_precondition___00.smt2 |    0.076s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_72f01f_generic_float_tests-T-defqtvc__00.smt2 |    0.076s | 22.02MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_99634e_generic_interval_tests-T-defqtvc__00.smt2 |    0.077s | 26.256MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O917-065__unreferenced__unref.adb_5_19_postcondition___00.smt2 |    0.078s | 19.564MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5c42fa_generic_interval_tests-T-defqtvc__00.smt2 |    0.078s | 21.368MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b9c8dc_generic_float_tests-T-defqtvc__00.smt2 |    0.079s | 20.476MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB23-014__float_monotonicity__add.adb_10_16_postcondition___00.smt2 |    0.079s | 19.48MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_6_14_fp_overflow_check___00.smt2 |    0.080s | 22.404MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/QA11-003__itp_example__test.adb_60_14_fp_overflow_check___00.smt2 |    0.081s | 29.876MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_5_12_range_check___00.smt2 |    0.081s | 19.692MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0fa4d6_generic_float_tests-T-defqtvc__00.smt2 |    0.081s | 19.884MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_20_22_assert___00.smt2 |    0.081s | 20.656MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1d5454_generic_float_tests-T-defqtvc__00.smt2 |    0.081s | 20.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1077_52_precondition___00.smt2 |    0.081s | 19.464MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f1b856_generic_interval_tests-T-defqtvc__00.smt2 |    0.081s | 27.852MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3176a4_generic_interval_tests-T-defqtvc__00.smt2 |    0.081s | 26.9MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_12_31_overflow_check___00.smt2 |    0.081s | 19.956MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_53b78c_generic_interval_tests-T-defqtvc__00.smt2 |    0.082s | 23.924MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f9f0b1_generic_interval_tests-T-defqtvc__00.smt2 |    0.082s | 23.212MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_92_7_complete_contract_cases___00.smt2 |    0.082s | 20.608MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_19_43_division_check___00.smt2 |    0.082s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_13_19_assert___00.smt2 |    0.083s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_43_21_fp_overflow_check___00.smt2 |    0.083s | 30.056MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_62_14_postcondition___00.smt2 |    0.083s | 21.44MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_492bd7_generic_float_tests-T-defqtvc__00.smt2 |    0.084s | 22.16MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_7_14_overflow_check___00.smt2 |    0.085s | 19.896MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_38_19_assert___00.smt2 |    0.085s | 19.724MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O312-037__flow_pure_subprograms__call.adb_22_51_precondition___00.smt2 |    0.085s | 20.928MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_189_47_precondition___00.smt2 |    0.085s | 20.884MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_24_18_range_check___00.smt2 |    0.085s | 23.104MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c522c9_generic_interval_tests-T-defqtvc__00.smt2 |    0.085s | 22.184MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_bbb756_generic_float_tests-T-defqtvc__00.smt2 |    0.086s | 20.052MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_46_19_assert___00.smt2 |    0.087s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1209_31_division_check___00.smt2 |    0.088s | 21.248MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a0c4ad_generic_float_tests-T-defqtvc__00.smt2 |    0.089s | 25.3MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_55_19_assert___00.smt2 |    0.089s | 21.28MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_15_62_contract_case___00.smt2 |    0.089s | 25.284MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_218eda_generic_float_tests-T-defqtvc__00.smt2 |    0.089s | 25.08MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_45_14_postcondition___00.smt2 |    0.090s | 20.616MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__errorexamplefloat.adb_29_22_assert___00.smt2 |    0.090s | 19.656MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_13_22_assert___00.smt2 |    0.090s | 20.648MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_19_28_discriminant_check___00.smt2 |    0.091s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_11_19_assert___00.smt2 |    0.091s | 20.408MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/QA11-003__itp_example__test.adb_56_17_postcondition___00.smt2 |    0.092s | 29.84MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ec718c_generic_float_tests-T-defqtvc__00.smt2 |    0.093s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_30_31_overflow_check___00.smt2 |    0.094s | 21.124MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K831-006__cmp__max.ads_4_19_postcondition___00.smt2 |    0.095s | 20.244MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_17_35_division_check2___00.smt2 |    0.095s | 20.888MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_21_22_assert___00.smt2 |    0.095s | 19.644MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.ads_27_14_postcondition___00.smt2 |    0.095s | 21.172MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_22_20_fp_overflow_check___00.smt2 |    0.096s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P830-027__flow_variables_in_float__f.adb_4_12_range_check___00.smt2 |    0.096s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_22_20_range_check___00.smt2 |    0.096s | 23.692MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3b4c73_generic_float_tests-T-defqtvc__00.smt2 |    0.096s | 28.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_8_19_assert___00.smt2 |    0.096s | 22.604MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/TU__depends_legal__depends_legal_2.adb_45_15_discriminant_check___00.smt2 |    0.096s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_13_31_overflow_check___00.smt2 |    0.096s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_50_19_precondition___00.smt2 |    0.097s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0d36c5_generic_float_tests-T-defqtvc__00.smt2 |    0.097s | 28.56MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_float.adb_17_19_assert___00.smt2 |    0.097s | 20.56MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q522-022__codepeer__proof.adb_25_15_precondition___00.smt2 |    0.098s | 20.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB16-021__float_range__test_float.adb_5_19_assert___00.smt2 |    0.098s | 20.88MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ddd17d_generic_float_tests-T-defqtvc__00.smt2 |    0.098s | 24.82MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_45_31_overflow_check___00.smt2 |    0.099s | 20.592MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-018__spurious_discr__useless_discr.adb_16_10_range_check___00.smt2 |    0.099s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_44_19_assert___00.smt2 |    0.099s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_30_22_discriminant_check___00.smt2 |    0.099s | 19.952MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__tagged_discr.adb_15_14_discriminant_check___00.smt2 |    0.099s | 20.076MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_37_19_assert___00.smt2 |    0.099s | 19.68MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_71_14_postcondition___00.smt2 |    0.100s | 20.416MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_16_142_fp_overflow_check___00.smt2 |    0.100s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_dc2c61_generic_interval_tests-T-defqtvc__00.smt2 |    0.100s | 23.18MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.adb_10_14_precondition___00.smt2 |    0.101s | 23.28MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6a7512_generic_float_tests-T-defqtvc__00.smt2 |    0.102s | 24.752MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_13_142_fp_overflow_check___00.smt2 |    0.103s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.adb_10_42_precondition___00.smt2 |    0.103s | 20.076MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_47_15_range_check___00.smt2 |    0.104s | 23.088MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_float.adb_16_4_precondition___00.smt2 |    0.104s | 19.628MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5dc342_generic_float_tests-T-defqtvc__00.smt2 |    0.104s | 29.432MiB| 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.104s | 21.164MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_28_22_assert___00.smt2 |    0.104s | 21.008MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_9be82f_generic_float_tests-T-defqtvc__00.smt2 |    0.105s | 25.02MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_72685b_generic_float_tests-T-defqtvc__00.smt2 |    0.105s | 24.968MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_62_4_precondition___00.smt2 |    0.105s | 19.636MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_92_7_disjoint_contract_cases___00.smt2 |    0.105s | 20.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_4_14_overflow_check___00.smt2 |    0.106s | 20.628MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8a6cb4_generic_float_tests-T-defqtvc__00.smt2 |    0.106s | 24.844MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_6_31_overflow_check___00.smt2 |    0.106s | 20.32MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_14_31_overflow_check___00.smt2 |    0.107s | 19.604MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1032_47_precondition___00.smt2 |    0.107s | 20.896MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f00b23_generic_interval_tests-T-defqtvc__00.smt2 |    0.108s | 23.428MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_39_19_assert___00.smt2 |    0.108s | 19.66MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_8_31_overflow_check___00.smt2 |    0.108s | 19.8MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_23_43_division_check___00.smt2 |    0.108s | 19.944MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_19_38_loop_invariant_init___00.smt2 |    0.109s | 20.124MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_752865_generic_float_tests-T-defqtvc__00.smt2 |    0.109s | 22.172MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P830-027__flow_variables_in_float__f.adb_3_12_range_check___00.smt2 |    0.109s | 19.576MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1059_52_precondition___00.smt2 |    0.109s | 21.116MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_10_100_postcondition___00.smt2 |    0.110s | 19.848MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_658b29_generic_interval_tests-T-defqtvc__00.smt2 |    0.110s | 26.488MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level2__hard_stuff.adb_20_52_division_check___00.smt2 |    0.111s | 20.064MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_41_21_fp_overflow_check___00.smt2 |    0.111s | 30.1MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P310-021__proof_float_remainder__foo.adb_16_17_division_check___00.smt2 |    0.111s | 20.64MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB04-007__float_conversion__floatround.adb_11_15_precondition___00.smt2 |    0.111s | 19.764MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_168f5d_generic_float_tests-T-defqtvc__00.smt2 |    0.112s | 20.788MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f38e09_generic_float_tests-T-defqtvc__00.smt2 |    0.112s | 25.184MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M122-006__assign__p.adb_14_9_discriminant_check___00.smt2 |    0.112s | 20.608MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_57_24_range_check___00.smt2 |    0.112s | 22.112MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P620-034__float_out_subtype__get_out_subtype.adb_27_58_range_check___00.smt2 |    0.112s | 19.616MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b2d859_generic_float_tests-T-defqtvc__00.smt2 |    0.113s | 20.112MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_56_4_precondition___00.smt2 |    0.113s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_d7746d_generic_float_tests-T-defqtvc__00.smt2 |    0.113s | 19.852MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB23-014__float_monotonicity__add.adb_13_4_precondition___00.smt2 |    0.113s | 20.476MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8f1e69_generic_float_tests-T-defqtvc__00.smt2 |    0.113s | 20.884MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_47_19_assert___00.smt2 |    0.114s | 20.092MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O430-013__return_unchecked_conversion__prover_crash.adb_14_23_range_check___00.smt2 |    0.115s | 20.896MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O224-020__constant_aggr__package_1.adb_12_29_fp_overflow_check___00.smt2 |    0.115s | 23.204MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_36_17_range_check___00.smt2 |    0.115s | 20.624MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_7_19_assert___00.smt2 |    0.115s | 20.164MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_14d53b_generic_interval_tests-T-defqtvc__00.smt2 |    0.116s | 28.824MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_22_31_overflow_check___00.smt2 |    0.116s | 20.832MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_11_31_overflow_check___00.smt2 |    0.117s | 19.608MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_22_22_assert___00.smt2 |    0.117s | 19.744MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_17_24_division_check___00.smt2 |    0.117s | 20.316MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_27_8_precondition___00.smt2 |    0.117s | 20.364MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5f8af6_generic_float_tests-T-defqtvc__00.smt2 |    0.117s | 20.724MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_18_21_division_check___00.smt2 |    0.118s | 28.072MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_133_22_assert___00.smt2 |    0.118s | 19.824MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ffe5a5_generic_float_tests-T-defqtvc__00.smt2 |    0.118s | 28.592MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5fa6e1_generic_float_tests-T-defqtvc__00.smt2 |    0.118s | 20.04MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_13_24_fp_overflow_check___00.smt2 |    0.119s | 26.152MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_19_150_division_check___00.smt2 |    0.119s | 20.584MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c1c2bc_generic_float_tests-T-defqtvc__00.smt2 |    0.120s | 24.876MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b33c2b_generic_float_tests-T-defqtvc__00.smt2 |    0.121s | 21.128MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a2c713_generic_interval_tests-T-defqtvc__00.smt2 |    0.121s | 23.504MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c6aff8_generic_float_tests-T-defqtvc__00.smt2 |    0.121s | 21.3MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_22e79d_generic_interval_tests-T-defqtvc__00.smt2 |    0.121s | 26.996MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e9287d_homothetical-T-defqtvc__00.smt2 |    0.122s | 25.504MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_7_20_fp_overflow_check___00.smt2 |    0.122s | 20.096MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_4b6267_generic_interval_tests-T-defqtvc__00.smt2 |    0.122s | 23.432MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_9b3454_generic_float_tests-T-defqtvc__00.smt2 |    0.122s | 28.94MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB23-014__float_monotonicity__mul.adb_13_4_precondition___00.smt2 |    0.122s | 20.368MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1050_47_precondition___00.smt2 |    0.123s | 20.78MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_fd32b1_generic_interval_tests-T-defqtvc__00.smt2 |    0.123s | 22.064MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_20_21_division_check___00.smt2 |    0.124s | 28.048MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_10_25_assert___00.smt2 |    0.125s | 30.228MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__numerics.ads_19_108_postcondition___00.smt2 |    0.126s | 20.408MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_6_18_range_check___00.smt2 |    0.126s | 19.572MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1176_47_precondition___00.smt2 |    0.127s | 20.828MiB| sat | 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.127s | 26.948MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_bb54cc_generic_float_tests-T-defqtvc__00.smt2 |    0.127s | 24.208MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8f06c6_generic_interval_tests-T-defqtvc__00.smt2 |    0.128s | 22.156MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_50_38_overflow_check___00.smt2 |    0.129s | 19.832MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_103_13_precondition___00.smt2 |    0.129s | 28.456MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_17_22_assert___00.smt2 |    0.129s | 30.452MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_132_13_precondition___00.smt2 |    0.130s | 28.44MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__ce__counter_examples.adb_8_38_fp_overflow_check___00.smt2 |    0.131s | 23.664MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_9_19_assert___00.smt2 |    0.131s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__precise.adb_12_11_division_check___00.smt2 |    0.132s | 19.612MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_79bf65_generic_interval_tests-T-defqtvc__00.smt2 |    0.132s | 23.18MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_12_22_assert___00.smt2 |    0.133s | 20.672MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a83df9_generic_interval_tests-T-defqtvc__00.smt2 |    0.133s | 23.576MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_45_17_range_check___00.smt2 |    0.134s | 23.968MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f4d109_generic_interval_tests-T-defqtvc__00.smt2 |    0.135s | 27.044MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b5cd90_generic_float_tests-T-defqtvc__00.smt2 |    0.136s | 20.384MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O429-046__flow_tasking_contracts__watchdog.ads_6_9_ceiling__priority_protocol___00.smt2 |    0.138s | 19.596MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.ads_29_20_postcondition___00.smt2 |    0.138s | 36.824MiB| unsat | 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.138s | 20.952MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero__run.ads_19_19_postcondition___00.smt2 |    0.138s | 23.004MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K720-019__floats__pack.ads_18_19_postcondition___00.smt2 |    0.139s | 26.108MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC04-023__float_conversion__type_conversion.ads_9_21_postcondition___00.smt2 |    0.139s | 29.58MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB23-014__float_literal__u.adb_12_20_assert___00.smt2 |    0.140s | 19.5MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_d30160_generic_interval_tests-T-defqtvc__00.smt2 |    0.141s | 23.184MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OC30-005__crash.adb_10_18_fp_overflow_check___00.smt2 |    0.143s | 23.18MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_92_132_fp_overflow_check___00.smt2 |    0.144s | 20.1MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_2.adb_16_18_overflow_check___00.smt2 |    0.145s | 21.096MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_18.adb_7_12_fp_overflow_check___00.smt2 |    0.146s | 23.208MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e5185b_generic_float_tests-T-defqtvc__00.smt2 |    0.147s | 25.492MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_106_75_division_check___00.smt2 |    0.147s | 27.38MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O224-020__constant_aggr__package_1.adb_11_29_fp_overflow_check___00.smt2 |    0.150s | 23.896MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b9b5ec_generic_interval_tests-T-defqtvc__00.smt2 |    0.151s | 23.692MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/OB16-021__float_range__test_float.adb_6_19_assert___00.smt2 |    0.152s | 20.832MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_83ffdb_generic_float_tests-T-defqtvc__00.smt2 |    0.155s | 25.228MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f5b2b3_generic_interval_tests-T-defqtvc__00.smt2 |    0.155s | 23.208MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b64636_generic_float_tests-T-defqtvc__00.smt2 |    0.155s | 28.968MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_6_12_overflow_check___00.smt2 |    0.156s | 21.2MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_13_23_division_check2___00.smt2 |    0.157s | 35.268MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6cb1b4_generic_interval_tests-T-defqtvc__00.smt2 |    0.157s | 26.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_42_19_assert___00.smt2 |    0.157s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_904c31_generic_float_tests-T-defqtvc__00.smt2 |    0.158s | 21.42MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f7e0e0_generic_interval_tests-T-defqtvc__00.smt2 |    0.160s | 32.672MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_8_19_assert___00.smt2 |    0.160s | 32.316MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_29_21_unreachable_branch___00.smt2 |    0.161s | 19.856MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_44_12_fp_overflow_check___00.smt2 |    0.162s | 23.688MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_988971_generic_float_tests-T-defqtvc__00.smt2 |    0.162s | 24.964MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_5_31_overflow_check___00.smt2 |    0.163s | 19.592MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P909-014__numerics__numerics-algo.adb_20_17_precondition___00.smt2 |    0.163s | 36.924MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_441ad2_generic_float_tests-T-defqtvc__00.smt2 |    0.163s | 30.876MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.adb_19_22_assert___00.smt2 |    0.163s | 19.76MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-033__in_range__p.adb_49_19_precondition___00.smt2 |    0.164s | 19.876MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_15_17_postcondition___00.smt2 |    0.165s | 23.832MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_20_54_fp_overflow_check___00.smt2 |    0.166s | 25.748MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b5e7a0_generic_float_tests-T-defqtvc__00.smt2 |    0.166s | 19.888MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_34_17_range_check___00.smt2 |    0.167s | 20.392MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_29fea4_generic_interval_tests-T-defqtvc__00.smt2 |    0.167s | 27.156MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e982c9_generic_interval_tests-T-defqtvc__00.smt2 |    0.167s | 26.872MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_199_14_precondition___00.smt2 |    0.167s | 20.976MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a34115_generic_float_tests-T-defqtvc__00.smt2 |    0.168s | 25.176MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_60_18_range_check___00.smt2 |    0.168s | 19.64MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_63_40_overflow_check___00.smt2 |    0.169s | 19.844MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_5_19_assert___00.smt2 |    0.170s | 20.408MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_10_42_overflow_check___00.smt2 |    0.170s | 20.892MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_10_20_fp_overflow_check___00.smt2 |    0.170s | 34.324MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_71_17_predicate_check___00.smt2 |    0.170s | 19.6MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_59_38_contract_case___00.smt2 |    0.171s | 19.916MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_54_22_assert___00.smt2 |    0.174s | 26.396MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-038__float_intervals__foo.adb_30_22_assert___00.smt2 |    0.174s | 20.628MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_475713_generic_interval_tests-T-defqtvc__00.smt2 |    0.175s | 32.968MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b94afa_generic_interval_tests-T-defqtvc__00.smt2 |    0.177s | 23.836MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_d25f13_generic_float_tests-T-defqtvc__00.smt2 |    0.177s | 22.356MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_15_33_loop_invariant_init2___00.smt2 |    0.177s | 19.652MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_7c2c0b_generic_float_tests-T-defqtvc__00.smt2 |    0.178s | 25.032MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_577b67_generic_float_tests-T-defqtvc__00.smt2 |    0.180s | 28.048MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_cc6bc3_generic_interval_tests-T-defqtvc__00.smt2 |    0.180s | 28.968MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level2__hard_stuff.adb_12_22_assert___00.smt2 |    0.181s | 25.22MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level2__hard_stuff.adb_7_22_assert___00.smt2 |    0.183s | 22.464MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_90d7ec_generic_interval_tests-T-defqtvc__00.smt2 |    0.183s | 38.56MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_float.adb_11_14_range_check___00.smt2 |    0.184s | 23.42MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_c786f0_generic_interval_tests-T-defqtvc__00.smt2 |    0.186s | 23.332MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O205-003__dynamic_float__test_dynamic_property.adb_21_15_fp_overflow_check___00.smt2 |    0.186s | 23.692MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_683e07_generic_float_tests-T-defqtvc__00.smt2 |    0.189s | 30.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e30a85_generic_float_tests-T-defqtvc__00.smt2 |    0.190s | 24.644MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_15_12_postcondition___00.smt2 |    0.193s | 29.364MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_995c50_generic_float_tests-T-defqtvc__00.smt2 |    0.193s | 30.248MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0354a0_generic_float_tests-T-defqtvc__00.smt2 |    0.194s | 21.608MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_7_19_assert___00.smt2 |    0.195s | 30.356MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_2cfc0a_generic_interval_tests-T-defqtvc__00.smt2 |    0.196s | 23.292MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_21_22_assert___00.smt2 |    0.198s | 35.752MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_014768_generic_interval_tests-T-defqtvc__00.smt2 |    0.198s | 26.9MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_3f27e3_generic_float_tests-T-defqtvc__00.smt2 |    0.201s | 30.688MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f4b86f_generic_interval_tests-T-defqtvc__00.smt2 |    0.205s | 38.52MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_161_13_precondition___00.smt2 |    0.205s | 28.536MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e7ad50_generic_interval_tests-T-defqtvc__00.smt2 |    0.209s | 27.156MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_8_20_fp_overflow_check___00.smt2 |    0.210s | 32.004MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1253ee_generic_interval_tests-T-defqtvc__00.smt2 |    0.213s | 24.064MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_336b10_generic_interval_tests-T-defqtvc__00.smt2 |    0.228s | 27.236MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_726911_generic_float_tests-T-defqtvc__00.smt2 |    0.228s | 30.42MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_18_54_fp_overflow_check___00.smt2 |    0.230s | 25.732MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6f649f_generic_float_tests-T-defqtvc__00.smt2 |    0.231s | 30.268MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_04ae02_generic_float_tests-T-defqtvc__00.smt2 |    0.237s | 30.808MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level3__hard_stuff.adb_21_22_assert___00.smt2 |    0.238s | 50.336MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_6_19_assert___00.smt2 |    0.243s | 24.524MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_20_32_range_check___00.smt2 |    0.243s | 39.588MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_28_17_range_check___00.smt2 |    0.244s | 24.8MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_8f72d3_generic_float_tests-T-defqtvc__00.smt2 |    0.249s | 30.548MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O220-024__floats__test_pack.ads_14_42_fp_overflow_check___00.smt2 |    0.251s | 23.948MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_24_22_assert___00.smt2 |    0.252s | 37.3MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_26_22_assert___00.smt2 |    0.255s | 38.168MiB| unsat | 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.256s | 32.78MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_21_51_fp_overflow_check___00.smt2 |    0.258s | 23.892MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_394d11_generic_interval_tests-T-defqtvc__00.smt2 |    0.263s | 27.2MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_028c17_homothetical-T-defqtvc__00.smt2 |    0.264s | 59.292MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b1475f_generic_interval_tests-T-defqtvc__00.smt2 |    0.276s | 27.404MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_fd3c3b_generic_interval_tests-T-defqtvc__00.smt2 |    0.278s | 32.72MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_19_62_contract_case___00.smt2 |    0.294s | 26.26MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_2.adb_32_32_range_check___00.smt2 |    0.297s | 53.628MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_1.adb_30_32_range_check___00.smt2 |    0.299s | 53.612MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_204f1e_generic_interval_tests-T-defqtvc__00.smt2 |    0.301s | 27.388MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O220-024__floats__test_pack.ads_12_43_fp_overflow_check___00.smt2 |    0.302s | 23.824MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_57b4e3_generic_float_tests-T-defqtvc__00.smt2 |    0.304s | 25.756MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level3__hard_stuff.adb_11_14_fp_overflow_check___00.smt2 |    0.306s | 25.26MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_29_22_assert___00.smt2 |    0.312s | 39.488MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_637_21_precondition___00.smt2 |    0.321s | 27.372MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_6f02ee_generic_float_tests-T-defqtvc__00.smt2 |    0.323s | 27.14MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.ads_15_10_postcondition___00.smt2 |    0.328s | 57.52MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_19_21_fp_overflow_check___00.smt2 |    0.332s | 27.14MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N121-026__nonlinear__nonlinear.adb_9_20_fp_overflow_check___00.smt2 |    0.333s | 23.872MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_19_22_assert___00.smt2 |    0.336s | 78.784MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_bce863_generic_float_tests-T-defqtvc__00.smt2 |    0.369s | 22.78MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_20_36_range_check___00.smt2 |    0.370s | 28.416MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_8_14_fp_overflow_check___00.smt2 |    0.395s | 29.972MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.ads_17_62_contract_case___00.smt2 |    0.398s | 26.32MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_45_22_range_check___00.smt2 |    0.416s | 31.676MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_22_22_assert___00.smt2 |    0.421s | 39.116MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_18.adb_4_16_postcondition___00.smt2 |    0.427s | 27.384MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_24_22_assert___00.smt2 |    0.440s | 83.48MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_9_19_assert___00.smt2 |    0.456s | 32.364MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero__run.ads_24_19_postcondition___00.smt2 |    0.457s | 24.248MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_212f49_generic_interval_tests-T-defqtvc__00.smt2 |    0.486s | 27.648MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_54_22_assert___00.smt2 |    0.497s | 83.292MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q906-010__float_volatile__copy_values.adb_8_25_fp_overflow_check___00.smt2 |    0.518s | 23.756MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_16_22_assert___00.smt2 |    0.528s | 32.204MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_10_19_assert___00.smt2 |    0.538s | 34.584MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_9cfb3a_generic_interval_tests-T-defqtvc__00.smt2 |    0.549s | 27.24MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_27_22_assert___00.smt2 |    0.569s | 44.104MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_4110a0_generic_interval_tests-T-defqtvc__00.smt2 |    0.604s | 27.088MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N116-016__floating_point__test_18.adb_7_19_fp_overflow_check___00.smt2 |    0.606s | 27.048MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__biaseddivide.ads_19_14_postcondition___00.smt2 |    0.613s | 150.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_12_19_assert___00.smt2 |    0.618s | 34.568MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.ads_15_19_postcondition___00.smt2 |    0.622s | 24.36MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M603-018__float__testfloat.adb_32_22_assert___00.smt2 |    0.654s | 44.196MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero_numerics__run.ads_25_19_postcondition___00.smt2 |    0.662s | 24.108MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P912-012__float_zero__run.ads_14_19_postcondition___00.smt2 |    0.669s | 24.616MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_23_26_fp_overflow_check___00.smt2 |    0.715s | 43.116MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__original_sample.ads_59_17_postcondition___00.smt2 |    0.734s | 27.732MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_12_11_postcondition___00.smt2 |    0.752s | 36.432MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_4.adb_40_32_range_check___00.smt2 |    0.792s | 136.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_69_41_fp_overflow_check___00.smt2 |    0.794s | 24.668MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O312-037__flow_pure_subprograms__call.adb_22_51_range_check___00.smt2 |    0.809s | 27.108MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_91_41_fp_overflow_check___00.smt2 |    0.840s | 24.692MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-021__float__p.adb_11_19_assert___00.smt2 |    0.843s | 34.584MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_22_22_assert___00.smt2 |    0.849s | 38.248MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__biaseddivide.ads_19_20_division_check___00.smt2 |    0.863s | 150.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_45_16_fp_overflow_check___00.smt2 |    0.891s | 38.848MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_22_20_range_check___00.smt2 |    0.906s | 29.008MiB| sat | 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.911s | 90.432MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e5004c_generic_interval_tests-T-defqtvc__00.smt2 |    0.934s | 64.488MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_11_33_loop_invariant_preserv2___00.smt2 |    1.017s | 160.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_19_38_loop_invariant_preserv___00.smt2 |    1.038s | 144.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/L402-004__exp__p.adb_5_14_fp_overflow_check___00.smt2 |    1.039s | 27.576MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_62_27_overflow_check___00.smt2 |    1.073s | 152.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__ce__counter_examples.adb_9_16_fp_overflow_check___00.smt2 |    1.080s | 27.22MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_23_17_range_check___00.smt2 |    1.141s | 35.288MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__sample.ads_57_17_postcondition___00.smt2 |    1.150s | 27.796MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_15_24_range_check___00.smt2 |    1.151s | 31.396MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_30_57_range_check___00.smt2 |    1.243s | 248.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_36_22_assert___00.smt2 |    1.281s | 252.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_15_22_assert___00.smt2 |    1.295s | 32.9MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_14_22_assert___00.smt2 |    1.358s | 32.608MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b7f9fd_generic_float_tests-T-defqtvc__00.smt2 |    1.397s | 32.216MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_827c21_generic_float_tests-T-defqtvc__00.smt2 |    1.481s | 26.168MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_457_42_fp_overflow_check___00.smt2 |    1.563s | 81.104MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_31_58_fp_overflow_check___00.smt2 |    1.603s | 391.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_31_47_range_check___00.smt2 |    1.632s | 250.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_92_13_precondition___00.smt2 |    1.638s | 29.992MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_facb24_generic_interval_tests-T-defqtvc__00.smt2 |    1.693s | 36.084MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_28_19_postcondition___00.smt2 |    1.738s | 148.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_637_21_range_check___00.smt2 |    1.759s | 37.028MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_46_22_assert___00.smt2 |    1.794s | 33.016MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_150_13_precondition___00.smt2 |    1.816s | 29.972MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_142_14_precondition___00.smt2 |    1.827s | 29.824MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_336_42_fp_overflow_check___00.smt2 |    1.846s | 81.108MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N121-026__nonlinear__nonlinear.adb_10_20_fp_overflow_check___00.smt2 |    1.856s | 31.168MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_21_22_assert___00.smt2 |    1.919s | 39.116MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N313-022__float_range__fr.adb_34_14_range_check___00.smt2 |    2.088s | 31.88MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_113_14_precondition___00.smt2 |    2.098s | 29.94MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_41a5f2_generic_float_tests-T-defqtvc__00.smt2 |    2.104s | 26.96MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_84_14_precondition___00.smt2 |    2.145s | 29.88MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_121_13_precondition___00.smt2 |    2.162s | 29.976MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_35_14_range_check___00.smt2 |    2.172s | 33.116MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_15_33_loop_invariant_preserv2___00.smt2 |    2.274s | 283.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_cc80a4_generic_float_tests-T-defqtvc__00.smt2 |    2.300s | 26.46MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_33_fp_overflow_check___00.smt2 |    2.538s | 90.032MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.ads_38_19_postcondition___00.smt2 |    2.580s | 347.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_70_22_assert___00.smt2 |    2.706s | 247.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_20_21_fp_overflow_check___00.smt2 |    2.729s | 78.808MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_31_22_assert___00.smt2 |    2.780s | 250.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.ads_38_32_range_check___00.smt2 |    2.815s | 346.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_104_22_assert___00.smt2 |    2.815s | 37.08MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_41_55_range_check___00.smt2 |    2.915s | 345.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_162_22_assert___00.smt2 |    2.919s | 35.916MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_42_46_range_check___00.smt2 |    2.969s | 346.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_42_34_range_check___00.smt2 |    2.970s | 29.088MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1194_21_range_check___00.smt2 |    2.987s | 37.988MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_18_21_fp_overflow_check___00.smt2 |    2.995s | 78.656MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA20-061__flow_variable_constant__basic_contracts.adb_10_22_assert___00.smt2 |    3.215s | 30.456MiB| unknown | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1d2077_generic_interval_tests-T-defqtvc__00.smt2 |    3.242s | 35.864MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_30_101_fp_overflow_check___00.smt2 |    3.259s | 424.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_75_22_assert___00.smt2 |    3.409s | 37.208MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_38_19_postcondition___00.smt2 |    3.548s | 485.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_151_14_range_check___00.smt2 |    3.576s | 35.948MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_a2c9b8_generic_interval_tests-T-defqtvc__00.smt2 |    3.576s | 35.996MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N121-026__nonlinear__nonlinear.adb_10_16_fp_overflow_check___00.smt2 |    3.667s | 35.016MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_26_22_assert___00.smt2 |    3.677s | 93.896MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_84_14_range_check___00.smt2 |    3.785s | 37.032MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_20_37_fp_overflow_check2___00.smt2 |    4.064s | 288.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_55_14_range_check___00.smt2 |    4.110s | 37.132MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_16_14_fp_overflow_check___00.smt2 |    4.116s | 33.252MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_142_14_range_check___00.smt2 |    4.243s | 36.436MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_29_14_postcondition___00.smt2 |    4.653s | 603.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_113_14_range_check___00.smt2 |    4.757s | 43.02MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_16bd7a_generic_float_tests-T-defqtvc__00.smt2 |    4.845s | 39.14MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_34_22_range_check___00.smt2 |    4.861s | 33.148MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ea0c9f_generic_float_tests-T-defqtvc__00.smt2 |    4.881s | 39.176MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__division_by_zero.adb_29_14_fp_overflow_check___00.smt2 |    5.507s | 39.62MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_38_32_range_check___00.smt2 |    5.603s | 682.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_93_14_range_check___00.smt2 |    6.061s | 38.12MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_64_14_range_check___00.smt2 |    6.223s | 38.268MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_26_36_range_check___00.smt2 |    6.378s | 42.444MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_122_14_range_check___00.smt2 |    6.640s | 42.96MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_21_44_fp_overflow_check___00.smt2 |    6.836s | 33.884MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P405-006__arithmetic_from_dafny__div_lemmas.adb_42_14_postcondition___00.smt2 |    7.560s | 40.084MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_ff055b_generic_interval_tests-T-defqtvc__00.smt2 |    7.630s | 68.516MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_77_22_assert___00.smt2 |    8.139s | 262.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_43_34_range_check___00.smt2 |    8.144s | 36.984MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_163_22_assert___00.smt2 |    8.438s | 41.468MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_26_49_fp_overflow_check___00.smt2 |    8.892s | 95.924MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_1583cf_generic_float_tests-T-defqtvc__00.smt2 |    9.270s | 64.972MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC17-036__gnatVa__protectedfloat.adb_17_24_fp_overflow_check___00.smt2 |    9.348s | 92.224MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_61b4e3_generic_float_tests-T-defqtvc__00.smt2 |    9.744s | 64.964MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/MC13-026__float_div__protectedfloat.adb_15_24_fp_overflow_check___00.smt2 |    9.754s | 92.38MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_35_45_fp_overflow_check___00.smt2 |   10.258s | 253.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_28_fp_overflow_check___00.smt2 |   10.441s | 91.276MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_21_22_fp_overflow_check___00.smt2 |   11.403s | 40.576MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_56_22_assert___00.smt2 |   11.899s | 95.672MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__division_by_zero.adb_39_14_division_check___00.smt2 |   12.213s | 200.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_25_31_fp_overflow_check___00.smt2 |   12.317s | 53.812MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_105_22_assert___00.smt2 |   12.856s | 42.092MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_47_22_assert___00.smt2 |   13.127s | 37.588MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_29_17_range_check___00.smt2 |   13.215s | 49.288MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P906-011__exp_division__expo.adb_6_11_division_check___00.smt2 |   13.468s | 39.232MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q607-007__floats__normalize.adb_76_22_assert___00.smt2 |   13.716s | 42.268MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_457_51_fp_overflow_check___00.smt2 |   14.303s | 104.0MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_e5cfc1_generic_float_tests-T-defqtvc__00.smt2 |   15.768s | 36.716MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_26_26_fp_overflow_check___00.smt2 |   16.319s | 48.768MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__abs_controller_oem_with_property.adb_56_43_fp_overflow_check___00.smt2 |   16.657s | 177.0MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_43_fp_overflow_check___00.smt2 |   17.677s | 110.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_21_fp_overflow_check___00.smt2 |   17.934s | 103.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_336_51_fp_overflow_check___00.smt2 |   18.463s | 104.0MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_27_32_fp_overflow_check___00.smt2 |   18.616s | 205.0MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_25_32_fp_overflow_check___00.smt2 |   18.703s | 96.616MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P310-021__proof_float_remainder__foo.adb_16_17_range_check___00.smt2 |   19.146s | 414.0MiB| sat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0d33ae_generic_float_tests-T-defqtvc__00.smt2 |   19.813s | 35.172MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S603-051__dimensions__dimensions.ads_377_7_fp_overflow_check___00.smt2 |   19.944s | 76.616MiB| unsat | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_37_53_fp_overflow_check___00.smt2 |   20.016s | 54.148MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M122-006__assign__p.adb_8_9_discriminant_check___00.smt2 |   20.017s | 56.636MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_12_25_assert2___00.smt2 |   20.018s | 45.564MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_391_30_range_check___00.smt2 |   20.018s | 71.24MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_14_19_assert___00.smt2 |   20.019s | 98.408MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB04-017__float__p.adb_4_13_range_check___00.smt2 |   20.020s | 57.74MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P620-034__float_out_subtype__get_out_subtype.adb_27_33_range_check___00.smt2 |   20.020s | 57.252MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.ads_93_75_contract_case___00.smt2 |   20.020s | 98.312MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_17_22_assert___00.smt2 |   20.020s | 58.404MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O220-024__floats__test_pack.adb_7_32_fp_overflow_check___00.smt2 |   20.020s | 45.916MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_17_fp_overflow_check___00.smt2 |   20.021s | 98.904MiB| timeout | 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 |   20.021s | 96.48MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_20_37_overflow_check___00.smt2 |   20.021s | 74.328MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_15_fp_overflow_check___00.smt2 |   20.021s | 99.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_21_34_fp_overflow_check___00.smt2 |   20.021s | 49.368MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O401-034__float_pred__safety_pack.adb_57_26_range_check___00.smt2 |   20.022s | 38.5MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_bee7c4_generic_float_tests-T-defqtvc__00.smt2 |   20.022s | 99.0MiB| timeout | 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 |   20.022s | 65.168MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_647_14_precondition___00.smt2 |   20.023s | 53.744MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_18_22_assert___00.smt2 |   20.024s | 88.428MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_363_29_range_check___00.smt2 |   20.024s | 71.08MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_55_22_assert___00.smt2 |   20.024s | 98.824MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_13_18_fp_overflow_check___00.smt2 |   20.025s | 76.432MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_10_54_fp_overflow_check___00.smt2 |   20.025s | 75.128MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__biaseddivide.adb_24_16_fp_overflow_check___00.smt2 |   20.025s | 158.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level3__hard_stuff.adb_29_25_assert___00.smt2 |   20.026s | 121.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_9_25_assert___00.smt2 |   20.026s | 37.508MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_10_17_postcondition___00.smt2 |   20.026s | 77.836MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_28_8_unreachable_branch___00.smt2 |   20.027s | 23.512MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_100_75_range_check___00.smt2 |   20.027s | 103.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S603-051__dimensions__dimensions.ads_377_11_fp_overflow_check___00.smt2 |   20.028s | 90.992MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_9_35_range_check___00.smt2 |   20.029s | 37.696MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_444_66_overflow_check___00.smt2 |   20.029s | 70.04MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_49_14_postcondition___00.smt2 |   20.030s | 175.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_25_22_assert___00.smt2 |   20.031s | 97.864MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.adb_23_30_overflow_check___00.smt2 |   20.032s | 225.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_36_14_postcondition___00.smt2 |   20.033s | 38.224MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S427-002__inline_dim__dimensions.ads_377_14_fp_overflow_check___00.smt2 |   20.034s | 50.256MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_607_25_range_check___00.smt2 |   20.034s | 289.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_4.adb_40_19_postcondition___00.smt2 |   20.035s | 135.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_63_62_overflow_check___00.smt2 |   20.035s | 173.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_35_22_assert___00.smt2 |   20.036s | 251.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M227-029__flow_records_and_arrays__message_tests.adb_37_16_fp_overflow_check___00.smt2 |   20.036s | 58.988MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P620-034__float_out_subtype__get_out_subtype.adb_27_58_range_check___01.smt2 |   20.037s | 57.948MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_f2780c_generic_float_tests-T-defqtvc__00.smt2 |   20.038s | 32.088MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_23_19_fp_overflow_check___00.smt2 |   20.038s | 54.74MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__abs_controller_oem_with_property.adb_88_22_assert___00.smt2 |   20.038s | 204.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_28_32_fp_overflow_check___00.smt2 |   20.039s | 204.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_1.adb_30_19_postcondition___00.smt2 |   20.040s | 64.052MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_10_41_fp_overflow_check___00.smt2 |   20.040s | 112.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__division_by_zero.adb_39_14_fp_overflow_check___00.smt2 |   20.041s | 215.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_28_25_fp_overflow_check___00.smt2 |   20.041s | 196.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_26_24_overflow_check___00.smt2 |   20.042s | 100.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_62_45_overflow_check___00.smt2 |   20.043s | 175.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_2.adb_32_19_postcondition___00.smt2 |   20.043s | 63.768MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_b32673_generic_float_tests-T-defqtvc__00.smt2 |   20.043s | 34.788MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_41_14_postcondition___00.smt2 |   20.043s | 71.084MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_19_24_overflow_check2___00.smt2 |   20.044s | 288.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_470_47_fp_overflow_check___00.smt2 |   20.044s | 372.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_10_29_fp_overflow_check___00.smt2 |   20.045s | 109.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_443_22_overflow_check___00.smt2 |   20.045s | 73.784MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_12_30_fp_overflow_check___00.smt2 |   20.045s | 57.928MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_843777_generic_float_tests-T-defqtvc__00.smt2 |   20.047s | 346.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/S118-010__zeros_counterex__math.adb_25_26_fp_overflow_check___00.smt2 |   20.048s | 51.644MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_15_24_overflow_check2___00.smt2 |   20.048s | 169.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_2cf678_generic_float_tests-T-defqtvc__00.smt2 |   20.049s | 281.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__sample.ads_37_17_postcondition___00.smt2 |   20.049s | 94.116MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_42_22_assert___00.smt2 |   20.049s | 357.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_390_22_overflow_check___00.smt2 |   20.050s | 70.5MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.adb_9_58_fp_overflow_check___00.smt2 |   20.050s | 70.9MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_23_22_assert___00.smt2 |   20.051s | 100.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1473_19_precondition___00.smt2 |   20.051s | 56.66MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_23_43_fp_overflow_check___00.smt2 |   20.052s | 126.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1209_31_fp_overflow_check___00.smt2 |   20.052s | 149.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_98_22_assert___00.smt2 |   20.053s | 170.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level0__hard_stuff.adb_28_29_fp_overflow_check___00.smt2 |   20.054s | 198.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_363_68_overflow_check___00.smt2 |   20.055s | 70.528MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__discriminant_check.adb_14_15_discriminant_check___00.smt2 |   20.055s | 57.792MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_349_47_fp_overflow_check___00.smt2 |   20.055s | 372.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_25_55_fp_overflow_check___00.smt2 |   20.056s | 99.044MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.adb_36_53_fp_overflow_check___00.smt2 |   20.056s | 60.328MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_12_58_fp_overflow_check___00.smt2 |   20.056s | 78.544MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_12_19_assert___00.smt2 |   20.056s | 162.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level1__hard_stuff.adb_28_21_fp_overflow_check___00.smt2 |   20.057s | 189.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_86_22_assert___00.smt2 |   20.057s | 168.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_362_22_overflow_check___00.smt2 |   20.057s | 71.476MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_30_57_fp_overflow_check___00.smt2 |   20.059s | 464.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC20-032__succ_pred__p.adb_46_14_postcondition___00.smt2 |   20.060s | 160.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M919-035__floating_point__dynamic_float.adb_7_19_range_check___00.smt2 |   20.061s | 34.668MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_23_45_fp_overflow_check___00.smt2 |   20.061s | 93.224MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O416-002__dyn_pred_rte__pred.adb_31_26_unreachable_branch___00.smt2 |   20.061s | 25.868MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_31_fp_overflow_check___00.smt2 |   20.062s | 105.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_22_32_fp_overflow_check___00.smt2 |   20.063s | 70.864MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_377_69_overflow_check___00.smt2 |   20.064s | 70.652MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_65_25_assert___00.smt2 |   20.065s | 336.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_470_22_fp_overflow_check___00.smt2 |   20.065s | 531.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_49c130_generic_float_tests-T-defqtvc__00.smt2 |   20.065s | 98.0MiB| timeout | 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 |   20.065s | 166.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_39_45_fp_overflow_check___00.smt2 |   20.067s | 70.876MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_36_fp_overflow_check___00.smt2 |   20.068s | 109.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_391_69_overflow_check___00.smt2 |   20.072s | 70.564MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_29_32_fp_overflow_check___00.smt2 |   20.072s | 207.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_37_54_fp_overflow_check___00.smt2 |   20.072s | 251.0MiB| timeout | 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 |   20.073s | 90.452MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_31_32_fp_overflow_check___00.smt2 |   20.073s | 218.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_457_22_fp_overflow_check___00.smt2 |   20.074s | 118.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/R123-048__tasks__psu_monitoring.adb_104_75_range_check___00.smt2 |   20.075s | 75.66MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1219_33_fp_overflow_check___00.smt2 |   20.075s | 149.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_40_22_assert___00.smt2 |   20.076s | 356.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_30_22_assert___00.smt2 |   20.077s | 250.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O826-006__float_exponential__float_expon.adb_10_26_fp_overflow_check___00.smt2 |   20.077s | 98.22MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O810-001__predicate__safety_pack.ads_55_21_range_check___00.smt2 |   20.078s | 38.428MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_74_22_assert___00.smt2 |   20.079s | 261.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_41_35_fp_overflow_check___00.smt2 |   20.079s | 358.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.adb_11_43_range_check___00.smt2 |   20.080s | 280.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_38_22_assert___00.smt2 |   20.081s | 251.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_28_22_assert___00.smt2 |   20.081s | 248.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_627_26_range_check___00.smt2 |   20.082s | 289.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P620-034__float_out_subtype__get_out_subtype.adb_28_33_range_check___00.smt2 |   20.082s | 56.532MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_65_44_fp_overflow_check___00.smt2 |   20.082s | 162.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_53_22_assert___00.smt2 |   20.083s | 97.156MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__errorexamplefloat.adb_48_22_assert___00.smt2 |   20.085s | 158.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_627_26_precondition___00.smt2 |   20.086s | 287.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__smoothing.adb_76_56_fp_overflow_check___00.smt2 |   20.087s | 167.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_30_36_fp_overflow_check___00.smt2 |   20.088s | 250.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P310-021__proof_float_remainder__foo.adb_9_17_range_check___00.smt2 |   20.088s | 227.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_607_25_precondition___00.smt2 |   20.089s | 287.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KC22-015__succ_overflow__p.adb_45_38_overflow_check___00.smt2 |   20.089s | 96.916MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/proofinuse__lat_long__lat_long.ads_18_26_precondition___00.smt2 |   20.091s | 50.88MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_76_22_assert___00.smt2 |   20.091s | 286.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_444_27_range_check___00.smt2 |   20.092s | 71.456MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_66_25_assert___00.smt2 |   20.092s | 361.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_617_26_precondition___00.smt2 |   20.092s | 287.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_63_25_assert___00.smt2 |   20.092s | 326.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_37_22_assert___00.smt2 |   20.093s | 251.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_1484_19_precondition___00.smt2 |   20.093s | 59.24MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_65_49_overflow_check___00.smt2 |   20.094s | 485.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/Q424-012__succ_floats_copy_z3__succ_floats.adb_22_19_assert___00.smt2 |   20.097s | 97.68MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N709-001__tagged_discr__classwide.ads_36_14_postcondition___00.smt2 |   20.097s | 188.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_376_22_overflow_check___00.smt2 |   20.098s | 71.276MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_30_19_assert___00.smt2 |   20.098s | 97.392MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler.adb_14_18_fp_overflow_check2___00.smt2 |   20.099s | 379.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__discriminant_check.adb_19_8_discriminant_check___00.smt2 |   20.099s | 57.34MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__errorexamplefloat.adb_39_65_fp_overflow_check___00.smt2 |   20.099s | 154.0MiB| timeout | 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 |   20.099s | 161.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC05-013__interval_overflow__mult.adb_11_22_assert___00.smt2 |   20.101s | 40.808MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_81_22_assert___00.smt2 |   20.103s | 545.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_30_32_fp_overflow_check___00.smt2 |   20.103s | 206.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O325-024__abstract_state__stabilizer_pack.adb_23_9_fp_overflow_check___00.smt2 |   20.103s | 75.196MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PB16-052__float_invariant__attempt_3.adb_64_25_assert___00.smt2 |   20.105s | 485.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P906-011__exp_division__expo.adb_6_11_fp_overflow_check___00.smt2 |   20.107s | 62.416MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O715-033__level0__hard_stuff.adb_28_17_fp_overflow_check___00.smt2 |   20.108s | 133.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_470_56_fp_overflow_check___00.smt2 |   20.111s | 476.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_0f9517_generic_float_tests-T-defqtvc__00.smt2 |   20.112s | 145.0MiB| timeout | 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 |   20.112s | 63.612MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_d5baaf_generic_float_tests-T-defqtvc__00.smt2 |   20.113s | 281.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N121-026__nonlinear__nonlinear.adb_11_19_assert___00.smt2 |   20.114s | 41.512MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/N122-021__succ_floats__succ_floats.adb_18_24_overflow_check___00.smt2 |   20.115s | 96.736MiB| timeout | 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 |   20.115s | 90.164MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M422-023__from_int__sgs.ads_13_17_postcondition___00.smt2 |   20.122s | 31.88MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_377_30_range_check___00.smt2 |   20.124s | 70.6MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__original_sample.ads_38_35_fp_overflow_check___00.smt2 |   20.124s | 288.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P615-019__silver__overflow_check.adb_30_32_division_check___00.smt2 |   20.125s | 199.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_16_22_assert___00.smt2 |   20.127s | 56.62MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_90cfbd_generic_float_tests-T-defqtvc__00.smt2 |   20.128s | 145.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.ads_13_18_postcondition___00.smt2 |   20.129s | 76.528MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/O512-022__number_theory__number_theory.ads_23_16_postcondition___00.smt2 |   20.130s | 121.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_349_56_fp_overflow_check___00.smt2 |   20.130s | 476.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_37_32_fp_overflow_check___00.smt2 |   20.131s | 250.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC05-005__float_division__pi_euler_2.adb_18_18_fp_overflow_check2___00.smt2 |   20.133s | 289.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_336_22_fp_overflow_check___00.smt2 |   20.137s | 117.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PA21-002__floatdiv__basic_contracts.adb_10_51_range_check___00.smt2 |   20.138s | 278.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P315-010__float__original_sample.ads_39_17_postcondition___00.smt2 |   20.142s | 95.128MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/NC06-004__init__shapes5.adb_8_8_refined_post___00.smt2 |   20.158s | 57.772MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_617_26_range_check___00.smt2 |   20.160s | 283.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/M809-005__float_basics__why_5cf5ea_generic_float_tests-T-defqtvc__00.smt2 |   20.165s | 346.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_10_65_fp_overflow_check___00.smt2 |   20.171s | 81.132MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/K719-019__flight_mgr__flight_manager.ads_11_18_fp_overflow_check___00.smt2 |   20.172s | 80.088MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_38_48_fp_overflow_check___00.smt2 |   20.177s | 251.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/P201-069__simulink__simulink_functions.adb_349_22_fp_overflow_check___00.smt2 |   20.193s | 531.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/PC07-014__float_conversion__simple_trajectory.adb_41_22_assert___00.smt2 |   20.204s | 362.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB25-022__exp__gp_exp.adb_6_11_overflow_check___00.smt2 |   20.225s | 1923.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB25-022__exp__gp_exp.adb_7_11_fp_overflow_check___00.smt2 |   20.249s | 1983.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB25-022__exp__gp_exp.adb_5_14_range_check___00.smt2 |   20.252s | 1507.0MiB| timeout | 0 |  |  |
|non-incremental/UFFPDTNIRA/20200306-Kanig/spark2014bench/KB25-022__exp__gp_exp.adb_5_11_overflow_check___00.smt2 |   20.268s | 1878.0MiB| timeout | 0 |  |  |