BENCHMARK INFORMATION benchmark definition: run_definitions/ultimateeliminatormathsat_FPArith.xml name: ultimateeliminatormathsat_FPArith run sets: UltimateEliminator+MathSAT,0,SingleQuery.task date: Mon, 2025-06-23 13:25:48 CEST tool: UltimateEliminator+MathSAT tool executable: ./unpack/18bc68b64c9813eae2f9ce64c6441fd8c4476b0c4e6b37b51b69c3f1181f7d50/ultimateeliminator.sh 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 ------------------------------------------------------------ UltimateEliminator+MathSAT,0,SingleQuery.task Run set 1 of 1 with options 'unpack/18bc68b64c9813eae2f9ce64c6441fd8c4476b0c4e6b37b51b69c3f1181f7d50/ultimateeliminator.sh' and propertyfile 'benchmarks/properties/SMT.prp' inputfile status cpu time wall time host --------------------------------------------------------------------------------------------------------------------------------------------------------------------------- BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0490a_true-unreach-call.c_4.yml unknown 0.00 0.00 tc05 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0670_true-unreach-call.c_2.yml unknown 0.00 0.00 tc08 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0971_true-unreach-call.c_10.yml unknown 0.00 0.00 tc03 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_double_req_bl_1052d_true-unreach-call.c_17.yml unknown 0.00 0.00 tc08 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_double_req_bl_1122a_true-unreach-call.c_2.yml unknown 0.00 0.00 tc06 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0620b_true-unreach-call.c_3.yml unknown 0.00 0.00 tc04 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0681a_true-unreach-call.c_4.yml unknown 0.00 0.00 tc08 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0683a_true-unreach-call.c_2.yml unknown 0.00 0.00 tc04 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0685a_true-unreach-call.c_4.yml unknown 0.00 0.00 tc05 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0686a_true-unreach-call.c_4.yml unknown 0.00 0.00 tc08 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0730b_true-unreach-call.c_2.yml unknown 0.00 0.00 tc08 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0730b_true-unreach-call.c_20.yml unknown 0.00 0.00 tc08 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0730b_true-unreach-call.c_5.yml unknown 0.00 0.00 tc06 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0876_true-unreach-call.c_14.yml unknown 0.01 0.01 tc06 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0876_true-unreach-call.c_15.yml unknown 0.00 0.00 tc05 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0876_true-unreach-call.c_16.yml unknown 0.00 0.00 tc05 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_1012a_true-unreach-call.c_19.yml unknown 0.01 0.01 tc02 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_1012a_true-unreach-call.c_9.yml unknown 0.00 0.01 tc07 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_1270b_true-unreach-call.c_4.yml unknown 0.00 0.01 tc01 BVFP/BVFP_20190429-UltimateAutomizerSvcomp2019_float_req_bl_1271a_true-unreach-call.c_4.yml unknown 0.00 0.00 tc03 BVFPLRA/BVFPLRA_20170501-Heizmann-UltimateAutomizer_bary_diverge_true-unreach-call.c_3027.yml unknown 0.01 0.01 tc01 BVFPLRA/BVFPLRA_20170501-Heizmann-UltimateAutomizer_rlim_invariant_true-unreach-call.c_1081.yml unknown 0.00 0.00 tc07 BVFPLRA/BVFPLRA_20170501-Heizmann-UltimateAutomizer_rlim_invariant_true-unreach-call.c_1768.yml unknown 0.01 0.01 tc05 BVFPLRA/BVFPLRA_20170501-Heizmann-UltimateAutomizer_zonotope_loose_true-unreach-call.c_156.yml unknown 0.00 0.01 tc02 BVFPLRA/BVFPLRA_20170501-Heizmann-UltimateAutomizer_zonotope_loose_true-unreach-call.c_161.yml unknown 0.00 0.00 tc03 BVFPLRA/BVFPLRA_20170501-Heizmann-UltimateAutomizer_zonotope_tight_true-unreach-call.c_41.yml unknown 0.00 0.01 tc02 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0620a_true-unreach-call.c_4.yml unknown 0.00 0.00 tc01 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0883_true-unreach-call.c_8.yml unknown 0.00 0.00 tc08 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_1092a_true-unreach-call.c_3.yml unknown 0.00 0.00 tc06 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0682a_true-unreach-call.c_2.yml unknown 0.00 0.00 tc03 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0685a_true-unreach-call.c_2.yml unknown 0.01 0.01 tc03 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0875_true-unreach-call.c_26.yml unknown 0.00 0.00 tc06 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0880_true-unreach-call.c_16.yml unknown 0.00 0.00 tc01 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0880_true-unreach-call.c_17.yml unknown 0.00 0.00 tc03 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0880_true-unreach-call.c_4.yml unknown 0.00 0.00 tc03 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0930_true-unreach-call.c_6.yml unknown 0.00 0.00 tc04 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_1012a_true-unreach-call.c_4.yml unknown 0.00 0.00 tc07 BVFPLRA/BVFPLRA_20190429-UltimateAutomizerSvcomp2019_sin_interpolated_smallrange_true-unreach-call.c_5.yml unknown 0.00 0.00 tc07 BVFPLRA/BVFPLRA_20230321-UltimateAutomizerSvcomp2023_filter1.c.p+cfa-reducer.c_1.yml unknown 0.00 0.00 tc02 BVFPLRA/BVFPLRA_20230321-UltimateAutomizerSvcomp2023_loop3.c_9.yml unknown 0.00 0.00 tc07 FP/FP_2019-Preiner_11_53_RNA_fp.rem_fp.isNormal1.yml unknown 0.00 0.00 tc02 FP/FP_2019-Preiner_11_53_RNE_fp.rem_fp.isInfinite0.yml unknown 0.00 0.00 tc02 FP/FP_2019-Preiner_11_53_RTN_fp.sub_fp.lt0.yml unknown 0.00 0.00 tc07 FP/FP_2019-Preiner_11_53_RTP_fp.abs_fp.geq.yml unknown 0.00 0.00 tc05 FP/FP_2019-Preiner_11_53_RTP_fp.sqrt_fp.isZero.yml unknown 0.00 0.00 tc01 FP/FP_2019-Preiner_11_53_RTZ_fp.sqrt_fp.isZero.yml unknown 0.00 0.00 tc08 FP/FP_2019-Preiner_3_5_RNA_fp.fma_fp.isInfinite0.yml unknown 0.00 0.00 tc08 FP/FP_2019-Preiner_3_5_RNE_fp.sqrt_fp.geq.yml unknown 0.00 0.01 tc04 FP/FP_2019-Preiner_3_5_RTN_fp.sqrt_fp.lt.yml unknown 0.00 0.00 tc07 FP/FP_2019-Preiner_3_5_RTP_fp.div_fp.geq0.yml unknown 0.00 0.00 tc04 FP/FP_2019-Preiner_3_5_RTZ_fp.rem_fp.isPositive0.yml unknown 0.00 0.01 tc08 FP/FP_2019-Preiner_3_5_RTZ_fp.rem_fp.isZero1.yml unknown 0.00 0.00 tc01 FP/FP_2019-Preiner_8_24_RNA_fp.fma_fp.isNegative2.yml unknown 0.00 0.00 tc05 FP/FP_2019-Preiner_8_24_RNE_fp.mul_fp.isNormal.yml unknown 0.00 0.00 tc02 FP/FP_2019-Preiner_8_24_RNE_fp.roundToIntegral_fp.isSubnormal.yml unknown 0.00 0.00 tc06 FP/FP_2019-Preiner_8_24_RNE_fp.sqrt_fp.isInfinite.yml unknown 0.01 0.01 tc06 FP/FP_2019-Preiner_8_24_RTP_fp.neg_fp.geq.yml unknown 0.00 0.00 tc02 FP/FP_20200911-Pine_1599121901269744000.yml unknown 0.00 0.00 tc02 FP/FP_20200911-Pine_1599121977787050000.yml unknown 0.01 0.01 tc02 FP/FP_20200911-Pine_1599122166216193000.yml unknown 0.00 0.00 tc02 FPLRA/FPLRA_20170501-Heizmann-UltimateAutomizer_exp_loop_true-unreach-call.c_1294.yml unknown 0.00 0.00 tc01 FPLRA/FPLRA_20170501-Heizmann-UltimateAutomizer_exp_loop_true-unreach-call.c_1310.yml unknown 0.00 0.00 tc04 FPLRA/FPLRA_20170501-Heizmann-UltimateAutomizer_float-div1_true-unreach-call.i_574.yml unknown 0.00 0.00 tc06 FPLRA/FPLRA_20170501-Heizmann-UltimateAutomizer_inv_square_true-unreach-call.c_110.yml unknown 0.01 0.01 tc08 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0833_true-unreach-call.c_14.yml unknown 0.00 0.00 tc02 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0833_true-unreach-call.c_5.yml unknown 0.00 0.00 tc03 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_double_req_bl_0833_true-unreach-call.c_6.yml unknown 0.00 0.00 tc03 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_filter1_true-unreach-call.c.v+nlh-reducer.c_0.yml unknown 0.01 0.01 tc02 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_filter1_true-unreach-call_true-termination.c_2.yml unknown 0.01 0.01 tc03 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_filter1_true-unreach-call_true-termination.c_3.yml unknown 0.00 0.00 tc05 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0683a_true-unreach-call.c_3.yml unknown 0.00 0.00 tc08 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0683a_true-unreach-call.c_4.yml unknown 0.00 0.00 tc04 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0683a_true-unreach-call.c_5.yml unknown 0.00 0.00 tc07 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0683a_true-unreach-call.c_6.yml unknown 0.00 0.00 ws19 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0683a_true-unreach-call.c_7.yml unknown 0.00 0.00 tc08 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_0832a_true-unreach-call.c_2.yml unknown 0.00 0.00 tc05 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_float_req_bl_1122a_true-unreach-call.c_3.yml unknown 0.00 0.00 tc04 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_water_pid_true-unreach-call_true-termination.c_2.yml unknown 0.00 0.00 tc02 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_water_pid_true-unreach-call_true-termination.c_3.yml unknown 0.00 0.00 tc01 FPLRA/FPLRA_20190429-UltimateAutomizerSvcomp2019_water_pid_true-unreach-call_true-termination.c_5.yml unknown 0.00 0.00 tc03 --------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Run set 1 done None 6.04 - Statistics: 80 Files correct: 0 correct true: 0 correct false: 0 incorrect: 0 incorrect true: 0 incorrect false: 0 unknown: 80