reduction_results_smt2.md

Reduction Results (SMT-LIB 2)

Bug ID	Program	HDD*	CoarseHDD*	HDDr*	GTR*	Perses*	Pardis*	PardisHyb*
C83	unexpected_token_parentheses_13K	410 28.077	3638 16.362	410 9.903	23 24.003	14 12.209	3638 18.174	3638 19.557
	unexpected_token_parentheses_2K	59 6.318	516 3.053	59 3.492	23 4.406	14 1.862	516 2.443	516 2.52
	unexpected_token_parentheses_36K	9068 5420.587	14411 132.526	8877 267.701	44 245.358	70 28.805	14355 120.526	14355 135.272
	unexpected_token_parentheses_4K	113 12.328	1103 6.38	113 6.03	23 9.219	14 3.528	1267 8.294	1267 9.13
C84	theory_fp_theory_fp_rewriter_cpp_157_1K	42 3.503	75 1.101	42 2.42	32 1.419	32 1.078	75 1.476	75 1.271
	theory_fp_theory_fp_rewriter_cpp_157_40K	42 7.31	70 3.301	42 4.947	58 4.257	29 3.515	91 20.742	98 4.343
	theory_fp_theory_fp_rewriter_cpp_157_6K	37 3.994	63 1.26	37 2.709	34 1.559	31 1.55	47 2.09	63 1.39
C85	theory_bv_bv_subtheory_inequality_cpp_208_2K	793 130.742	1009 8.586	844 33.75	243 38.35	216 14.381	1009 7.91	1009 8.557
	theory_bv_bv_subtheory_inequality_cpp_208_3K	912 119.371	1088 8.738	926 35.463	256 40.206	220 19.324	1088 8.293	1088 8.962
	theory_bv_bv_subtheory_inequality_cpp_208_4K	1400 237.44	1499 14.115	1416 43.826	375 64.676	321 30.244	1499 13.076	1499 14.195
C86	theory_rewriter_cpp_291_15K	4521 1860.754	5869 57.181	4509 164.081	413 199.227	216 46.833	5869 54.916	5869 58.975
	theory_rewriter_cpp_291_4K	1628 237.176	1832 14.947	1559 50.013	226 54.854	163 21.76	1832 13.721	1832 14.234
	theory_rewriter_cpp_291_5K	1631 353.701	1976 16.832	1512 45.507	231 59.453	150 27.834	1976 15.831	1976 17.149
	theory_rewriter_cpp_291_7K	2150 706.5	2910 32.545	2119 72.145	306 88.328	189 32.029	2910 26.072	2910 32.254
C87	significand_bit_vector_in_fp_is_an_invalid_size_12K	29 1.482	39 1.236	29 1.353	17 1.455	17 0.999	39 4.278	39 2.424
	significand_bit_vector_in_fp_is_an_invalid_size_31K	28 1.821	39 0.964	28 1.556	13 1.425	13 1.384	39 11.605	39 2.662
	significand_bit_vector_in_fp_is_an_invalid_size_5K	29 1.108	29 0.553	29 0.991	17 0.684	17 0.617	29 2.38	29 1.149
C88	theory_fp_fp_converter_cpp_160_1K	32 3.116	32 2.242	32 2.804	29 2.555	29 2.519	32 4.114	32 2.216
	theory_fp_fp_converter_cpp_160_4K	46 4.052	46 2.4	46 3.28	29 2.453	29 2.412	46 8.561	46 4.824
	theory_fp_fp_converter_cpp_160_9K	32 2.703	32 1.855	32 2.388	29 2.127	29 2.098	32 11.641	32 5.68
C89	util_floatingpoint_cpp_445_2K	20 2.071	25 1.665	20 2.065	17 1.618	17 1.641	32 7.318	40 4.756
	util_floatingpoint_cpp_445_41K	29 2.463	46 2.722	29 2.383	17 2.424	17 1.929	60 93.23	60 18.336
	util_floatingpoint_cpp_445_5K	34 2.099	45 1.024	34 2.116	13 1.493	13 1.606	61 18.383	33 3.769
C90	util_floatingpoint_cpp_455_2K	19 3.215	19 2.795	19 3.107	19 2.997	19 3.035	19 7.09	19 2.983
	util_floatingpoint_cpp_455_3K	29 1.911	44 1.752	29 1.83	17 1.97	17 1.441	39 5.689	39 2.416
	util_floatingpoint_cpp_455_8K	28 1.926	28 1.233	28 1.86	22 1.421	13 1.454	28 18.28	28 4.139
C91	theory_strings_regexp_entail_cpp_319_13K	98 20.496	261 8.536	98 12.766	68 9.324	59 7.203	231 11.522	231 10.474
	theory_strings_regexp_entail_cpp_319_24K	124 9.567	124 3.105	124 5.781	70 5.693	70 5.205	124 11.072	124 5.975
	theory_strings_regexp_entail_cpp_319_46K	140 74.197	166 63.649	125 65.699	72 61.243	72 60.867	151 48.545	151 45.248
	theory_strings_regexp_entail_cpp_319_64K	271 40.858	339 11.329	271 24.458	71 8.978	75 7.698	334 31.445	334 19.861
C92	segfault_yices_2_2_0_20K	417 31.729	443 10.945	428 17.29	265 13.39	244 13.782	454 5.641	434 6.487
	segfault_yices_2_2_0_4K	114 6.796	111 2.098	111 3.813	52 2.179	84 2.143	100 1.618	100 1.393
	segfault_yices_2_2_0_59K	91 4.417	91 1.764	88 2.553	82 2.062	82 1.744	88 10.643	88 2.484
C93	parser_utils_term_stack2_c_2454_100K	84 4.778	74 1.861	84 3.646	27 1.706	31 1.458	74 23.408	74 4.438
	parser_utils_term_stack2_c_2454_13K	23 2.135	23 1.781	23 1.995	23 1.902	23 1.9	23 2.018	23 1.046
	parser_utils_term_stack2_c_2454_25K	25 7.63	25 7.279	25 7.525	19 7.613	19 7.339	25 7.101	25 4.313
	parser_utils_term_stack2_c_2454_2K	29 0.975	29 0.476	29 0.874	19 0.615	19 0.585	29 0.829	29 0.698
C94	invalid_index_in_rotate_23K	607 94.681	7240 27.764	650 12.022	63 23.669	53 7.462	7212 19.276	7212 20.665
	invalid_index_in_rotate_3K	151 12.114	889 3.196	151 4.157	37 4.048	28 1.771	889 2.475	889 2.698
	invalid_index_in_rotate_54K	209 21.721	16318 42.674	209 5.113	54 51.141	55 2.499	16318 32.931	16318 34.556
C95	invalid_index_in_rotate_5K	116 9.98	1493 4.559	116 2.39	35 4.759	26 1.715	1486 3.512	1486 3.998
C96	segfault_z3_4_4_0_18K	4426 2210.549	7104 75.881	4328 89.251	189 107.27	203 22.721	7062 45.848	7062 77.676
	segfault_z3_4_4_0_1K	194 25.082	369 2.907	194 4.29	29 2.779	34 1.654	354 2.383	340 2.166
	segfault_z3_4_4_0_22K	4546 469.577	7611 110.987	4546 120.543	74 75.78	36 17.891	7053 44.849	7053 53.253
	segfault_z3_4_4_0_6K	1427 198.68	2356 19.184	1427 31.473	20 16.479	34 4.834	2208 12.471	2208 14.614
C97	invalid_number_of_arguments_to_floating_point_relation_1K	15 0.724	29 0.465	15 0.715	12 0.304	12 0.298	29 0.435	27 0.373
	invalid_number_of_arguments_to_floating_point_relation_34K	24 0.698	29 0.344	24 0.725	21 0.279	12 0.305	37 11.803	35 2.245
	invalid_number_of_arguments_to_floating_point_relation_7K	15 0.889	47 0.882	15 0.927	12 0.447	12 0.458	49 2.006	49 0.951
W10	wrong_cvc4_1_4_16K	144 20.364	203 8.942	144 12.546	99 10.871	99 10.84	166 15.043	166 9.645
	wrong_cvc4_1_4_2K	155 16.196	205 5.438	155 8.454	112 6.989	103 5.266	184 2.359	184 2.544
	wrong_cvc4_1_4_35K	246 34.153	293 16.186	247 21.308	111 16.566	123 13.944	253 40.889	246 27.842
	wrong_cvc4_1_4_9K	217 21.158	213 8.015	216 25.344	148 11.682	121 13.3	145 10.025	145 8.422
W11	wrong_cvc4_1_5_11K	2793 1193.159	4540 35.632	3707 118.341	203 93.893	159 19.026	4541 34.943	4540 37.111
	wrong_cvc4_1_5_1K	429 50.683	473 4.195	429 10.318	151 12.127	66 4.055	473 3.695	473 3.915
	wrong_cvc4_1_5_21K	5996 3082.317	8654 93.737	6109 266.967	636 245.902	80 22.967	8654 91.711	8654 98.626
	wrong_cvc4_1_5_4K	880 305.324	1591 13.767	880 22.322	118 32.812	88 13.756	1591 12.612	1591 13.931
W12	wrong_cvc4_1_6_21K	82 12.404	82 6.476	82 8.048	64 6.628	64 6.127	73 19.914	73 12.505
	wrong_cvc4_1_6_37K	159 17.272	164 4.927	159 10.543	111 6.673	111 7.296	164 40.251	164 23.349
	wrong_cvc4_1_6_55K	79 10.087	97 7.486	79 8.663	67 7.061	67 6.746	92 55.314	92 24.384
	wrong_cvc4_1_6_9K	74 7.081	86 2.199	74 4.01	50 2.594	50 2.926	86 8.178	86 5.688
W13	wrong_yices_2_2_0_1K	480 62.015	570 4.433	507 14.175	89 10.251	44 4.805	571 3.789	570 4.193
	wrong_yices_2_2_0_2K	911 145.877	1048 8.088	812 25.915	109 18.822	64 7.047	1048 6.941	1048 7.7
	wrong_yices_2_2_0_3K	714 188.784	1262 8.335	810 18.21	134 20.067	71 5.326	1262 7.676	1262 8.584
W14	wrong_yices_2_3_0_12K	34 12.927	45 6.914	34 8.295	25 6.648	65 6.906	45 7.527	45 5.256
	wrong_yices_2_3_0_49K	144 20.917	136 7.011	133 9.988	67 9.062	67 8.452	108 33.083	66 18.896
	wrong_yices_2_3_0_5K	217 17.448	229 5.918	217 10.216	100 5.812	100 6.14	229 4.646	229 4.948
	wrong_yices_2_3_0_69K	227 26.398	238 8.911	227 14.303	138 10.735	138 9.799	225 53.488	225 36.686
W15	wrong_yices_2_4_0_13K	354 36.788	433 8.757	354 21.149	170 11.632	127 7.936	436 11.103	424 9.766
	wrong_yices_2_4_0_24K	79 5.698	79 2.451	79 3.674	61 4.148	61 3.712	79 14.992	79 9.182
	wrong_yices_2_4_0_42K	150 21.025	164 11.618	150 15.5	79 12.622	85 12.742	144 31.941	144 19.528
	wrong_yices_2_4_0_87K	67 9.556	86 4.703	42 5.892	62 5.069	62 5.036	95 59.894	36 34.375