BENCHMARK INFORMATION benchmark definition: run_definitions/bitwuzla_model_QF_FPArith.xml name: bitwuzla_model_QF_FPArith run sets: Bitwuzla,3,ModelValidation.task date: Mon, 2025-06-23 13:53:30 CEST tool: Bitwuzla tool executable: ./unpack/c96f2a17a93a64fe57da002ddcc09f6c1b1187d16ee67ce2a842375a6d7b0b1c/bin/bitwuzla options: property file: benchmarks/properties/SMT.prp resource limits: - memory: 8192.0 MB - time: 240 s - cpu cores: 2 hardware requirements: - cpu model: Intel Core i7 - cpu cores: 2 - memory: 8192.0 MB ------------------------------------------------------------ Bitwuzla,3,ModelValidation.task Run set 1 of 1 with options 'unpack/c96f2a17a93a64fe57da002ddcc09f6c1b1187d16ee67ce2a842375a6d7b0b1c/bin/bitwuzla' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_gsl_benchmarks_sort_smallest_klee.x86_64_query.0545.yml true 0.03 0.03 tc01 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_gsl_benchmarks_sort_smallest_klee_bug.x86_64_query.2163.yml true 0.05 0.06 tc01 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.00002.yml true 0.01 0.01 tc04 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.00053.yml true 0.00 0.00 tc05 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.00750.yml true 0.01 0.01 tc06 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.02025.yml true 0.01 0.01 ws11 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.02320.yml true 0.00 0.00 tc01 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.03273.yml true 0.01 0.01 tc03 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.04181.yml true 0.00 0.00 tc03 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.04206.yml true 0.01 0.01 tc07 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.04464.yml true 0.01 0.01 tc08 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.05650.yml true 0.01 0.01 tc02 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.05703.yml true 0.01 0.01 tc04 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.06306.yml true 0.01 0.01 tc02 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.07300.yml true 0.00 0.00 tc03 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.07511.yml true 0.00 0.00 tc06 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.08474.yml true 0.01 0.01 tc03 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.08961.yml true 0.01 0.01 tc06 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.09945.yml true 0.01 0.01 tc07 QF_BVFP/QF_BVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_rlim_invariant.x86_64_query.258.yml true 0.17 0.17 tc02 QF_BVFPLRA/QF_BVFPLRA_20170501-Heizmann-UltimateAutomizer_Muller_Kahan_true-unreach-call.c_446.yml true 0.00 0.00 tc06 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_Float_div_true-unreach-call.i_1.yml true 0.04 0.04 tc05 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_digits_bad_for_false-unreach-call.i_4.yml true 0.07 0.07 tc06 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0310_true-unreach-call.c_0.yml true 0.00 0.01 tc02 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0330a_true-unreach-call.c_8.yml true 0.01 0.02 tc07 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0490a_true-unreach-call.c_1.yml true 0.00 0.00 tc06 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0520_true-unreach-call.c_6.yml true 0.01 0.01 tc03 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0684a_true-unreach-call.c_1.yml true 0.00 0.00 tc07 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0931_true-unreach-call.c_0.yml true 0.00 0.00 tc04 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0971_true-unreach-call.c_1.yml true 0.00 0.00 tc02 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0920b_true-unreach-call.c_3.yml true 0.08 0.08 tc02 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0930_true-unreach-call.c_0.yml true 0.01 0.01 tc05 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_inv_Newton_false-unreach-call.c_0.yml true 0.00 0.00 tc08 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_newton_1_7_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.yml true 4.10 4.10 tc08 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_newton_2_6_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.yml true 32.90 32.90 tc03 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_newton_2_8_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.yml true 32.72 32.72 tc05 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_5.yml true 0.00 0.00 tc05 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_sqrt_Householder_interval_true-unreach-call.c_1.yml true 0.00 0.00 tc07 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_sqrt_Newton_pseudoconstant_true-unreach-call.c_2.yml true 0.02 0.02 tc03 QF_BVFPLRA/QF_BVFPLRA_20190429-UltimateAutomizerSvcomp2019_square_3_false-unreach-call_true-termination.i_AllErrorsAtOnce_Iteration1_TraceCheck_0.yml true 1.27 1.28 tc04 QF_FP/QF_FP_wintersteiger__abs_abs-has-solution-17873.yml true 0.00 0.00 tc08 QF_FP/QF_FP_wintersteiger__add_add-has-solution-13089.yml true 0.00 0.00 tc07 QF_FP/QF_FP_wintersteiger__add_add-has-solution-17770.yml true 0.00 0.00 tc07 QF_FP/QF_FP_wintersteiger__div_div-has-solution-17517.yml true 0.00 0.00 tc04 QF_FP/QF_FP_wintersteiger__div_div-has-solution-17788.yml true 0.00 0.00 tc01 QF_FP/QF_FP_wintersteiger__eq_eq-has-solution-12071.yml true 0.00 0.00 tc06 QF_FP/QF_FP_wintersteiger__fma_fma-has-solution-3452.yml true 0.00 0.00 tc02 QF_FP/QF_FP_wintersteiger__fma_fma-has-solution-5020.yml true 0.00 0.00 tc05 QF_FP/QF_FP_wintersteiger__gt_gt-has-solution-4007.yml true 0.00 0.00 ws01 QF_FP/QF_FP_wintersteiger__lt_lt-has-solution-2278.yml true 0.00 0.00 tc01 QF_FP/QF_FP_wintersteiger__lt_lt-has-solution-2601.yml true 0.00 0.00 tc07 QF_FP/QF_FP_wintersteiger__min_min-has-solution-10782.yml true 0.00 0.00 tc05 QF_FP/QF_FP_wintersteiger__min_min-has-solution-11704.yml true 0.00 0.00 tc04 QF_FP/QF_FP_wintersteiger__min_min-has-solution-12289.yml true 0.00 0.00 tc08 QF_FP/QF_FP_wintersteiger__min_min-has-solution-4899.yml true 0.00 0.00 tc03 QF_FP/QF_FP_wintersteiger__rem_rem-has-solution-9822.yml true 0.00 0.00 tc01 QF_FP/QF_FP_wintersteiger__sqrt_sqrt-has-solution-16603.yml true 0.00 0.00 tc04 QF_FP/QF_FP_wintersteiger__sub_sub-has-solution-16275.yml true 0.00 0.00 tc04 QF_FP/QF_FP_wintersteiger__toIntegral_toIntegral-has-solution-1055.yml true 0.00 0.00 tc08 QF_FP/QF_FP_wintersteiger__toIntegral_toIntegral-has-solution-949.yml true 0.00 0.00 tc03 QF_FPLRA/QF_FPLRA_20170501-Heizmann-UltimateAutomizer_cos_polynomial_true-unreach-call.c_9.yml true 0.00 0.00 tc06 QF_FPLRA/QF_FPLRA_2019-Gudemann_expLaw.yml true 4.16 4.16 tc04 QF_FPLRA/QF_FPLRA_2019-Gudemann_propLnExp0.yml true 1.20 1.20 tc04 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0260_true-unreach-call.c_3.yml true 0.00 0.00 tc08 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0270a_true-unreach-call.c_19.yml true 0.02 0.02 tc08 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0270a_true-unreach-call.c_2.yml true 0.00 0.00 tc05 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0320_true-unreach-call.c_6.yml true 0.01 0.01 tc02 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0460_true-unreach-call.c_2.yml true 0.00 0.00 tc06 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0490a_true-unreach-call.c_2.yml true 0.00 0.00 tc06 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0490a_true-unreach-call.c_3.yml true 0.00 0.00 tc07 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0520_true-unreach-call.c_0.yml true 0.00 0.00 tc08 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0550b_true-unreach-call.c_9.yml true 0.01 0.01 tc03 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0870b_true-unreach-call.c_3.yml true 0.00 0.00 tc07 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0250b_true-unreach-call.c_4.yml true 0.02 0.02 tc01 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0470_true-unreach-call.c_12.yml true 0.01 0.01 tc07 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0490a_true-unreach-call.c_10.yml true 0.52 0.52 tc02 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0873a_true-unreach-call.c_3.yml true 0.00 0.00 tc06 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_1.yml true 0.01 0.02 tc05 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c_3.yml true 0.02 0.02 tc05 QF_FPLRA/QF_FPLRA_20190429-UltimateAutomizerSvcomp2019_sqrt_Newton_pseudoconstant_true-unreach-call.c_1.yml true 0.02 0.02 tc06 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_gsl_benchmarks_sort_smallest_klee_bug.x86_64_query.0910.yml true 0.03 0.03 tc01 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_exp_loop.c.x86_64_query.103.yml true 0.01 0.01 tc08 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.00015.yml true 0.01 0.01 tc01 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.00030.yml true 0.01 0.01 tc06 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.00714.yml true 0.01 0.01 tc03 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.01576.yml true 0.00 0.01 tc06 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.01992.yml true 0.01 0.01 tc04 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.02287.yml true 0.00 0.00 tc02 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.03242.yml true 0.01 0.01 tc07 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.04152.yml true 0.01 0.01 tc06 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.04437.yml true 0.01 0.01 tc02 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.05626.yml true 0.00 0.00 tc02 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.05702.yml true 0.00 0.00 tc01 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.06284.yml true 0.00 0.00 tc08 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.07194.yml true 0.01 0.01 tc01 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.07491.yml true 0.01 0.01 tc01 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.07512.yml true 0.01 0.01 tc02 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.08457.yml true 0.01 0.01 tc05 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_mea8000.x86_64_query.09932.yml true 0.00 0.00 tc08 QF_ABVFP/QF_ABVFP_20170428-Liew-KLEE__imperial_svcomp_float-benchs_svcomp_rlim_invariant.x86_64_query.235.yml true 0.10 0.10 tc04 QF_ABVFPLRA/QF_ABVFPLRA_20170501-Heizmann-UltimateAutomizer_filter2_iterated_true-unreach-call.c_321.yml true 0.12 0.12 tc03 QF_ABVFPLRA/QF_ABVFPLRA_20170501-Heizmann-UltimateAutomizer_filter2_iterated_true-unreach-call.c_322.yml true 0.15 0.15 tc01 QF_ABVFPLRA/QF_ABVFPLRA_20170501-Heizmann-UltimateAutomizer_filter2_iterated_true-unreach-call.c_329.yml true 0.14 0.14 tc08 QF_ABVFPLRA/QF_ABVFPLRA_20170501-Heizmann-UltimateAutomizer_filter2_iterated_true-unreach-call.c_330.yml true 0.21 0.21 tc07 QF_ABVFPLRA/QF_ABVFPLRA_20170501-Heizmann-UltimateAutomizer_filter2_iterated_true-unreach-call.c_331.yml true 0.32 0.33 tc05 QF_ABVFPLRA/QF_ABVFPLRA_20170501-Heizmann-UltimateAutomizer_filter2_iterated_true-unreach-call.c_70.yml true 0.14 0.14 tc08 QF_ABVFPLRA/QF_ABVFPLRA_20170501-Heizmann-UltimateAutomizer_filter2_iterated_true-unreach-call.c_71.yml true 0.12 0.12 tc03 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0550b_true-unreach-call.c_5.yml true 0.01 0.01 tc03 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0833_true-unreach-call.c_0.yml true 0.01 0.01 tc06 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0874_true-unreach-call.c_4.yml true 0.00 0.01 tc05 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_filter_iir_true-unreach-call.c_0.yml true 4.81 4.81 tc08 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0220b_true-unreach-call.c_0.yml true 0.13 0.13 tc01 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0660b_true-unreach-call.c_1.yml true 0.00 0.00 tc05 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0685a_true-unreach-call.c_9.yml true 0.00 0.00 tc07 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_interpolation2_true-unreach-call.c.v+cfa-reducer.c_0.yml true 0.19 0.19 tc08 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_interpolation2_true-unreach-call_true-termination.c_0.yml true 0.12 0.12 tc05 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_interpolation_true-unreach-call.c.p+cfa-reducer.c_0.yml true 0.10 0.10 tc04 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_sin_interpolated_index_false-unreach-call_true-termination.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.yml true 3.78 3.78 tc07 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_sqrt_poly2_false-unreach-call.c_0.yml true 0.01 0.01 tc03 QF_ABVFPLRA/QF_ABVFPLRA_20190429-UltimateAutomizerSvcomp2019_sqrt_poly2_false-unreach-call.c_AllErrorsAtOnce_Iteration1_TraceCheck_0.yml true 0.56 0.56 tc01 -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 38.56 - Statistics: 120 Files correct: 103 correct true: 103 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 0