Tool	BLAST 2.7.3				Cascade 0.1				CBMC 4.9				CPAchecker 1.3.10-svcomp15				ESBMC 1.24				Seahorn				SMACK				Ultimate Automizer r12950				Ultimate Kojak r12950
Limits	timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host	cayman[1-8]
OS	Linux 3.13.0
System	CPU: Intel Core i7-4770 @ 3.40 GHz with 8 cores, frequency: 3.4 GHz; RAM: 33 GB
Date of execution	14-11-25 03:45 [[ 14-12-21 23:31 ]]				14-12-18 12:10 [[ 14-12-19 11:22 ]]				14-11-19 20:34 [[ 14-12-21 23:35 ]]				14-11-15 15:53 [[ 14-12-21 23:23 ]]				14-12-13 18:39 [[ 14-12-19 11:24 ]]				14-12-20 18:50 [[ 14-12-21 21:13 ]]				14-11-26 16:05 [[ 14-12-22 07:46 ]]				14-11-12 22:41 [[ 14-12-21 23:12 ]]				14-11-16 20:08 [[ 14-12-21 23:18 ]]
Options	-alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/blast.14-11-25_0345.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/blast-2.7.3/bin/witness.graphml -setprop spec.singlePathMatching=true -setprop parser.transformTokensToLines=false -tokenize -useTokenizer ]]				-trace [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cascade.14-12-18_1210.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/Cascade-4113-patch/out/${sourcefile_name}/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]]				--32 [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cbmc.14-11-19_2034.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/cbmc-sv-comp-2015/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]]				-sv-comp15 -disable-java-assertions -heap 10000m [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cpachecker.14-11-15_1553.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/CPAchecker-1.3.10-svcomp15-unix/output/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=true ]]				[[ -witness-check -noout -timelimit 90 -spec ../../results-2015/esbmc.14-12-13_1839.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/esbmc-v1.24.1/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]]				--cex=witness.graphml [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/seahorn.14-12-20_1850.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/seahorn-svcomp15/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]]				--errorwitness witness.graphml [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/smack.14-11-26_1605.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/smack-corral/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=true -tokenize -deletePragmas ]]				32bit precise [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimateautomizer.14-11-12_2241.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/UltimateAutomizer/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]]				32bit precise [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimatekojak.14-11-16_2008.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/UltimateKojak/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]]
../../sv-benchmarks/c/product-lines/	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness
elevator_spec14_product20_false-unreach-call.cil.c	witness confirmed	450	430	3.8	unknown	1.3	98	-	witness confirmed	0.25	36	3.8	witness confirmed	5.3	420	4.2	witness confirmed	0.19	39	3.8	witness confirmed	9.2	70	3.7	witness confirmed	110	3800	4.2	timeout	920	9400	-	timeout	920	1900	-
elevator_spec14_product24_false-unreach-call.cil.c	exception (gremlins)	1.5	35	-	unknown	1.5	110	-	witness confirmed	0.26	36	4.1	witness confirmed	6.3	470	4.9	witness confirmed	0.19	40	4.1	witness confirmed	14	120	3.7	witness confirmed	110	3100	4.3	timeout	920	9000	-	timeout	920	1900	-
elevator_spec14_product28_false-unreach-call.cil.c	witness confirmed	490	380	3.7	unknown	1.6	110	-	witness confirmed	0.23	36	3.8	witness confirmed	6.2	420	4.0	witness confirmed	0.19	39	4.5	witness confirmed	9.9	73	3.6	witness confirmed	110	4300	3.9	timeout	920	13000	-	timeout	920	1900	-
elevator_spec14_product32_false-unreach-call.cil.c	exception (gremlins)	1.4	35	-	unknown	1.4	100	-	witness confirmed	0.24	36	4.0	witness confirmed	5.9	460	4.4	witness confirmed	0.19	40	4.0	witness confirmed	14	120	3.7	witness confirmed	110	3200	4.1	timeout	920	10000	-	timeout	920	1900	-
elevator_spec14_productSimulator_false-unreach-call.cil.c	exception (gremlins)	130	320	-	unknown	1.6	120	-	witness confirmed	13	180	5.8	witness confirmed	7.1	540	6.9	witness confirmed	30	1100	6.0	witness confirmed	48	300	6.0	witness confirmed	120	5300	6.0	timeout	920	11000	-	timeout	920	1900	-
elevator_spec1_product18_false-unreach-call.cil.c	timeout	920	600	-	unknown	1.5	100	-	witness confirmed	0.45	36	3.9	witness confirmed	5.5	460	4.8	witness confirmed	0.17	39	4.0	witness confirmed	7.6	79	3.7	witness confirmed	110	3100	4.2	timeout	920	9400	-	timeout	920	1900	-
elevator_spec1_product20_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.5	110	-	true	0.43	37	-	witness confirmed	6.0	490	4.3	witness confirmed	0.19	41	4.2	witness confirmed	8.0	79	3.7	witness confirmed	110	3000	3.9	timeout	920	9400	-	timeout	920	1900	-
elevator_spec1_product22_false-unreach-call.cil.c	exception (gremlins)	2.6	55	-	unknown	1.3	100	-	witness confirmed	0.46	37	3.9	witness confirmed	6.5	560	4.4	witness confirmed	0.20	40	4.2	witness confirmed	15	130	3.7	witness confirmed	110	4000	3.9	timeout	920	12000	-	timeout	920	1900	-
elevator_spec1_product24_false-unreach-call.cil.c	exception (gremlins)	2.5	49	-	unknown	1.2	100	-	witness confirmed	0.47	37	4.0	witness confirmed	6.6	530	4.5	witness confirmed	0.20	41	4.7	witness confirmed	16	130	3.8	witness confirmed	110	4700	4.1	timeout	920	12000	-	timeout	920	1900	-
elevator_spec1_product26_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.5	110	-	true	0.43	36	-	witness confirmed	5.8	470	4.3	witness confirmed	0.18	40	4.0	witness confirmed	7.6	80	3.7	witness confirmed	110	3200	4.1	timeout	920	8800	-	timeout	920	1900	-
elevator_spec1_product28_false-unreach-call.cil.c	timeout	920	670	-	unknown	1.6	110	-	witness confirmed	0.48	37	4.0	witness confirmed	6.8	490	4.4	witness confirmed	0.21	41	4.3	witness confirmed	8.7	81	3.7	witness confirmed	110	3200	3.9	timeout	920	13000	-	timeout	920	1900	-
elevator_spec1_product30_false-unreach-call.cil.c	exception (gremlins)	2.9	67	-	unknown	1.2	100	-	witness confirmed	0.45	37	4.0	witness confirmed	6.6	550	4.4	witness confirmed	0.18	41	4.1	witness confirmed	16	130	3.7	witness confirmed	110	4100	4.0	timeout	920	12000	-	timeout	920	1900	-
elevator_spec1_product32_false-unreach-call.cil.c	exception (gremlins)	2.9	56	-	unknown	1.6	110	-	witness confirmed	0.46	37	4.1	witness confirmed	8.2	540	4.6	witness confirmed	0.19	41	4.9	witness confirmed	16	130	4.1	witness confirmed	110	4400	4.5	timeout	920	8800	-	timeout	920	1900	-
elevator_spec1_productSimulator_false-unreach-call.cil.c	timeout	920	840	-	unknown	1.4	110	-	witness confirmed	100	440	6.7	witness confirmed	7.3	580	8.1	witness confirmed	46	1500	7.6	witness confirmed	120	390	6.9	witness confirmed	120	3900	7.3	timeout	920	13000	-	timeout	920	1900	-
elevator_spec2_product18_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.5	110	-	witness confirmed	0.46	36	3.9	witness confirmed	5.9	450	4.5	witness confirmed	0.19	39	4.1	witness confirmed	5.8	74	3.7	witness confirmed	110	3100	3.8	timeout	920	10000	-	timeout	920	1900	-
elevator_spec2_product20_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.5	110	-	witness confirmed	0.46	37	3.9	witness confirmed	6.0	470	4.5	witness confirmed	0.20	40	4.1	witness confirmed	6.9	74	3.6	witness confirmed	110	2900	4.0	timeout	920	9300	-	timeout	920	1900	-
elevator_spec2_product22_false-unreach-call.cil.c	exception (gremlins)	2.5	52	-	unknown	1.5	110	-	witness confirmed	0.46	37	3.9	witness confirmed	6.5	470	4.5	witness confirmed	0.19	40	4.0	witness confirmed	12	120	3.6	witness confirmed	110	4500	4.1	timeout	920	10000	-	timeout	920	1900	-
elevator_spec2_product24_false-unreach-call.cil.c	exception (gremlins)	2.6	47	-	unknown	1.6	110	-	witness confirmed	0.46	37	4.1	witness confirmed	6.5	500	4.5	witness confirmed	0.19	41	4.4	witness confirmed	13	120	3.9	witness confirmed	110	4600	4.1	timeout	920	10000	-	timeout	920	1900	-
elevator_spec2_product26_false-unreach-call.cil.c	timeout	920	630	-	unknown	1.6	110	-	witness confirmed	0.44	36	4.1	witness confirmed	5.9	450	4.4	witness confirmed	0.18	39	3.9	witness confirmed	6.4	74	3.7	witness confirmed	110	3000	4.0	timeout	920	13000	-	timeout	920	1900	-
elevator_spec2_product28_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.4	110	-	true	0.43	37	-	witness confirmed	7.0	470	5.2	witness confirmed	0.17	40	4.1	witness confirmed	6.6	74	4.1	witness confirmed	110	3200	4.0	timeout	920	9800	-	timeout	920	1900	-
elevator_spec2_product30_false-unreach-call.cil.c	exception (gremlins)	2.7	62	-	unknown	1.6	110	-	witness confirmed	0.46	37	3.9	witness confirmed	6.2	470	5.5	witness confirmed	0.18	40	4.0	witness confirmed	12	120	3.7	witness confirmed	110	4600	4.5	timeout	920	11000	-	timeout	920	1900	-
elevator_spec2_product32_false-unreach-call.cil.c	exception (gremlins)	2.9	54	-	unknown	1.5	110	-	witness confirmed	0.45	37	4.1	witness confirmed	6.5	490	4.5	witness confirmed	0.20	41	4.6	witness confirmed	13	120	3.9	witness confirmed	110	4300	4.4	timeout	920	11000	-	timeout	920	1900	-
elevator_spec2_productSimulator_false-unreach-call.cil.c	timeout	920	710	-	unknown	1.5	110	-	witness confirmed	63	340	6.9	witness confirmed	7.5	580	8.1	witness confirmed	46	1400	7.4	witness confirmed	89	350	6.6	witness confirmed	120	4000	6.8	timeout	920	13000	-	timeout	920	2300	-
elevator_spec3_product03_false-unreach-call.cil.c	witness confirmed	0.34	68	4.2	unknown	1.3	99	-	witness confirmed	0.31	37	5.0	witness confirmed	6.1	460	4.8	witness confirmed	0.24	42	4.5	witness confirmed	4.9	41	4.1	witness confirmed	75	2100	4.7	timeout	920	12000	-	timeout	920	1900	-
elevator_spec3_product11_false-unreach-call.cil.c	witness confirmed	0.33	67	4.2	unknown	1.3	96	-	witness confirmed	0.31	37	3.9	witness confirmed	6.8	470	4.8	witness confirmed	0.22	43	4.9	witness confirmed	5.1	42	4.0	witness confirmed	77	2200	4.6	timeout	920	13000	-	timeout	920	1900	-
elevator_spec3_product19_false-unreach-call.cil.c	witness confirmed	0.34	69	4.6	unknown	1.4	100	-	witness confirmed	0.31	37	4.4	witness confirmed	6.4	460	4.8	witness confirmed	0.23	43	4.7	witness confirmed	5.0	43	4.6	witness confirmed	81	2300	5.5	timeout	920	12000	-	timeout	920	1900	-
elevator_spec3_product20_false-unreach-call.cil.c	witness confirmed	0.38	74	4.3	unknown	1.5	110	-	witness confirmed	0.32	37	4.5	witness confirmed	7.0	470	5.0	witness confirmed	0.24	43	4.8	witness confirmed	9.4	72	4.9	witness confirmed	110	3900	5.1	timeout	920	9400	-	timeout	920	2500	-
elevator_spec3_product23_false-unreach-call.cil.c	exception (gremlins)	0.73	29	-	unknown	1.6	110	-	witness confirmed	0.31	38	4.2	witness confirmed	7.2	480	4.6	witness confirmed	0.26	44	4.8	witness confirmed	7.1	58	4.1	witness confirmed	110	3000	4.8	timeout	920	13000	-	timeout	920	2600	-
elevator_spec3_product24_false-unreach-call.cil.c	exception (gremlins)	0.75	30	-	unknown	1.6	110	-	witness confirmed	0.31	38	4.4	witness confirmed	8.1	530	4.8	witness confirmed	0.25	44	5.4	witness confirmed	14	120	4.5	witness confirmed	110	3200	4.9	timeout	920	9800	-	timeout	920	1900	-
elevator_spec3_product27_false-unreach-call.cil.c	witness confirmed	0.36	68	4.2	unknown	1.6	110	-	witness confirmed	0.30	37	4.2	witness confirmed	6.8	470	4.7	witness confirmed	0.25	43	4.7	witness confirmed	5.3	48	4.0	witness confirmed	89	2600	4.7	timeout	920	12000	-	timeout	920	2500	-
elevator_spec3_product28_false-unreach-call.cil.c	witness confirmed	0.37	75	4.2	unknown	1.5	110	-	witness confirmed	0.30	37	4.1	witness confirmed	6.6	480	4.5	witness confirmed	0.22	44	4.8	witness confirmed	10.0	80	4.0	witness confirmed	110	4000	4.7	timeout	920	8900	-	timeout	920	1900	-
elevator_spec3_product31_false-unreach-call.cil.c	exception (gremlins)	0.75	30	-	unknown	1.4	99	-	witness confirmed	0.29	38	4.8	witness confirmed	6.9	480	4.7	witness confirmed	0.24	44	4.7	witness confirmed	7.4	60	4.1	witness confirmed	110	3100	4.8	timeout	920	13000	-	timeout	920	1900	-
elevator_spec3_product32_false-unreach-call.cil.c	exception (gremlins)	0.76	30	-	unknown	1.4	100	-	witness confirmed	0.32	38	4.6	witness confirmed	7.4	540	4.7	witness confirmed	0.25	45	5.9	witness confirmed	14	120	4.1	witness confirmed	110	3300	5.8	timeout	920	9800	-	timeout	920	2600	-
elevator_spec3_productSimulator_false-unreach-call.cil.c	exception (gremlins)	460	280	-	unknown	1.4	110	-	witness confirmed	53	340	8.3	witness confirmed	7.9	550	11	witness confirmed	57	1900	9.2	witness confirmed	86	490	8.8	witness confirmed	120	5300	9.0	timeout	920	13000	-	timeout	920	2600	-
elevator_spec9_product26_false-unreach-call.cil.c	timeout	920	590	-	unknown	1.3	100	-	witness confirmed	0.44	36	3.9	witness confirmed	5.9	430	4.4	witness confirmed	0.18	39	4.1	witness confirmed	6.3	74	3.7	witness confirmed	110	3000	3.8	timeout	920	13000	-	timeout	920	1900	-
elevator_spec9_product28_false-unreach-call.cil.c	timeout	920	410	-	unknown	1.6	110	-	witness confirmed	0.46	37	3.9	witness confirmed	6.7	480	4.7	witness confirmed	0.19	41	4.2	witness confirmed	6.6	74	3.7	witness confirmed	110	3400	4.1	timeout	920	13000	-	timeout	920	1900	-
elevator_spec9_product30_false-unreach-call.cil.c	exception (gremlins)	67	150	-	unknown	1.3	100	-	witness confirmed	0.44	37	3.9	witness confirmed	6.9	500	4.5	witness confirmed	0.20	41	4.1	witness confirmed	13	120	3.6	witness confirmed	110	4600	4.0	timeout	920	12000	-	timeout	920	1900	-
elevator_spec9_product32_false-unreach-call.cil.c	exception (gremlins)	95	180	-	unknown	1.6	110	-	witness confirmed	0.45	37	4.1	witness confirmed	6.8	490	4.6	witness confirmed	0.20	42	4.4	witness confirmed	12	120	3.8	witness confirmed	110	4300	4.2	timeout	920	12000	-	timeout	920	1900	-
elevator_spec9_productSimulator_false-unreach-call.cil.c	timeout	920	1200	-	unknown	1.4	110	-	true	57	330	-	witness confirmed	7.7	570	8.3	witness confirmed	46	1400	7.0	witness confirmed	68	340	7.2	witness confirmed	120	4000	7.4	timeout	920	13000	-	timeout	920	1900	-
elevator_spec13_product21_true-unreach-call.cil.c	exception (gremlins)	1.4	40	-	unknown	1.6	110	-	true	2.8	36	-	true	2.6	190	-	true	0.19	38	-	true	29	140	-	true	120	3800	-	timeout	920	13000	-	timeout	920	1900	-
elevator_spec13_product22_true-unreach-call.cil.c	exception (gremlins)	1.5	39	-	unknown	1.3	96	-	true	2.9	36	-	true	2.7	200	-	true	0.18	38	-	true	92	200	-	true	120	2700	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec13_product23_true-unreach-call.cil.c	exception (gremlins)	1.5	38	-	unknown	1.7	110	-	true	2.8	36	-	true	2.7	190	-	true	0.18	39	-	true	280	410	-	true	120	3500	-	timeout	920	11000	-	timeout	920	1900	-
elevator_spec13_product24_true-unreach-call.cil.c	exception (gremlins)	1.6	39	-	unknown	1.2	100	-	true	2.9	38	-	true	2.8	200	-	true	0.20	39	-	timeout	920	420	-	true	120	3500	-	timeout	920	11000	-	timeout	920	1900	-
elevator_spec13_product29_true-unreach-call.cil.c	exception (gremlins)	1.7	42	-	unknown	1.6	110	-	true	2.9	36	-	true	2.6	170	-	true	0.19	38	-	true	30	150	-	true	120	3600	-	timeout	920	11000	-	timeout	920	1900	-
elevator_spec13_product30_true-unreach-call.cil.c	exception (gremlins)	1.8	43	-	unknown	1.6	110	-	true	2.9	36	-	true	2.6	200	-	true	0.19	38	-	true	91	210	-	true	120	3100	-	timeout	920	11000	-	timeout	920	2600	-
elevator_spec13_product31_true-unreach-call.cil.c	exception (gremlins)	1.7	41	-	unknown	1.3	100	-	true	2.8	38	-	true	2.7	200	-	true	0.18	39	-	true	710	550	-	true	120	3800	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec13_product32_true-unreach-call.cil.c	exception (gremlins)	1.8	42	-	unknown	1.5	110	-	true	2.9	38	-	true	2.7	200	-	true	0.17	39	-	timeout	920	560	-	true	120	3100	-	timeout	920	11000	-	timeout	920	1900	-
elevator_spec13_productSimulator_true-unreach-call.cil.c	exception (gremlins)	2.1	69	-	unknown	1.4	100	-	true	850	200	-	true	3.4	200	-	timeout	920	3800	-	timeout	920	740	-	true	260	5500	-	timeout	920	9700	-	timeout	920	1900	-
elevator_spec14_product03_true-unreach-call.cil.c	timeout	920	600	-	unknown	1.5	110	-	true	1.9	35	-	true	3.0	200	-	true	0.20	37	-	true	5.3	50	-	true	160	2800	-	timeout	920	9500	-	timeout	920	1900	-
elevator_spec14_product11_true-unreach-call.cil.c	timeout	920	620	-	unknown	1.4	100	-	true	2.0	35	-	true	3.0	200	-	true	0.21	38	-	true	5.5	51	-	true	170	2700	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec14_product19_true-unreach-call.cil.c	timeout	920	420	-	unknown	1.5	110	-	true	2.0	36	-	true	3.0	200	-	true	0.20	38	-	true	5.5	50	-	true	180	3000	-	timeout	920	9200	-	timeout	920	1900	-
elevator_spec14_product23_true-unreach-call.cil.c	exception (gremlins)	1.4	33	-	unknown	1.4	100	-	true	2.4	36	-	true	3.1	210	-	true	0.21	38	-	true	8.4	68	-	true	130	2800	-	timeout	920	9800	-	timeout	920	2600	-
elevator_spec14_product27_true-unreach-call.cil.c	timeout	920	530	-	unknown	1.5	110	-	true	2.1	36	-	true	3.1	200	-	true	0.23	38	-	true	5.8	51	-	true	190	3000	-	timeout	920	9800	-	timeout	920	2600	-
elevator_spec14_product31_true-unreach-call.cil.c	exception (gremlins)	1.4	34	-	unknown	1.3	100	-	true	2.3	36	-	true	3.1	210	-	true	0.21	39	-	true	8.8	68	-	true	130	2900	-	timeout	920	10000	-	timeout	920	1900	-
elevator_spec1_product01_true-unreach-call.cil.c	timeout	920	520	-	unknown	1.6	110	-	true	1.6	36	-	true	2.9	200	-	true	0.20	38	-	true	17	63	-	true	120	2200	-	timeout	920	11000	-	timeout	920	1900	-
elevator_spec1_product03_true-unreach-call.cil.c	timeout	920	1100	-	unknown	1.3	98	-	true	1.8	36	-	true	2.9	200	-	true	0.18	39	-	true	11	49	-	true	120	2200	-	timeout	920	13000	-	timeout	920	1900	-
elevator_spec1_product09_true-unreach-call.cil.c	timeout	920	540	-	unknown	1.4	99	-	true	1.6	37	-	true	2.9	200	-	true	0.19	38	-	true	14	64	-	true	130	2200	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec1_product11_true-unreach-call.cil.c	timeout	920	1100	-	unknown	1.5	110	-	true	1.9	37	-	true	3.0	210	-	true	0.20	39	-	true	16	64	-	true	130	2300	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec1_product17_true-unreach-call.cil.c	timeout	920	560	-	unknown	1.5	110	-	true	1.7	36	-	true	2.9	200	-	true	0.19	38	-	true	11	58	-	true	130	2400	-	timeout	920	10000	-	timeout	920	1900	-
elevator_spec1_product19_true-unreach-call.cil.c	timeout	920	420	-	unknown	1.6	110	-	true	1.9	37	-	true	2.9	200	-	true	0.22	39	-	true	16	63	-	true	140	2400	-	timeout	920	12000	-	timeout	920	2600	-
elevator_spec1_product21_true-unreach-call.cil.c	exception (gremlins)	3.4	80	-	unknown	1.5	110	-	true	1.8	37	-	true	2.9	200	-	true	0.22	39	-	true	99	96	-	true	200	3200	-	timeout	920	9700	-	timeout	920	1900	-
elevator_spec1_product23_true-unreach-call.cil.c	exception (gremlins)	26	160	-	unknown	1.4	100	-	true	2.0	38	-	true	3.0	210	-	true	0.21	39	-	true	150	110	-	true	220	3200	-	timeout	920	11000	-	timeout	920	1900	-
elevator_spec1_product25_true-unreach-call.cil.c	timeout	920	560	-	unknown	1.3	98	-	true	1.7	36	-	true	2.9	200	-	true	0.18	38	-	true	14	64	-	true	140	2300	-	timeout	920	11000	-	timeout	920	1900	-
elevator_spec1_product27_true-unreach-call.cil.c	timeout	920	590	-	unknown	1.5	110	-	true	1.9	37	-	true	2.8	200	-	true	0.20	39	-	true	16	65	-	true	140	2500	-	timeout	920	11000	-	timeout	920	2300	-
elevator_spec1_product29_true-unreach-call.cil.c	exception (gremlins)	3.5	83	-	unknown	1.6	120	-	true	1.9	37	-	true	2.9	200	-	true	0.21	39	-	true	120	98	-	true	210	3300	-	timeout	920	12000	-	timeout	920	2600	-
elevator_spec1_product31_true-unreach-call.cil.c	exception (gremlins)	26	160	-	unknown	1.2	100	-	true	2.0	37	-	true	3.0	210	-	true	0.23	39	-	true	140	110	-	true	240	3600	-	timeout	920	10000	-	timeout	920	1900	-
elevator_spec2_product01_true-unreach-call.cil.c	timeout	920	390	-	unknown	1.4	100	-	true	1.3	36	-	true	2.6	190	-	true	0.18	38	-	true	9.1	55	-	true	120	2100	-	timeout	920	9400	-	timeout	920	1900	-
elevator_spec2_product03_true-unreach-call.cil.c	timeout	920	720	-	unknown	1.5	110	-	true	1.5	36	-	true	2.7	200	-	true	0.19	38	-	true	6.1	44	-	true	120	2100	-	timeout	920	10000	-	timeout	920	1900	-
elevator_spec2_product09_true-unreach-call.cil.c	timeout	920	560	-	unknown	1.5	110	-	true	1.3	36	-	true	2.7	200	-	true	0.18	38	-	true	6.0	44	-	true	130	2300	-	timeout	920	9300	-	timeout	920	1900	-
elevator_spec2_product11_true-unreach-call.cil.c	timeout	920	540	-	unknown	1.4	100	-	true	1.5	37	-	true	2.7	200	-	true	0.17	39	-	true	5.7	44	-	true	130	2500	-	timeout	920	13000	-	timeout	920	1900	-
elevator_spec2_product17_true-unreach-call.cil.c	timeout	920	410	-	unknown	1.4	110	-	true	1.3	36	-	true	2.7	190	-	true	0.18	38	-	true	5.3	44	-	true	130	2300	-	timeout	920	9200	-	timeout	920	1900	-
elevator_spec2_product19_true-unreach-call.cil.c	timeout	920	560	-	unknown	1.6	110	-	true	1.5	38	-	true	2.7	190	-	true	0.18	38	-	true	7.7	44	-	true	140	2400	-	timeout	920	8900	-	timeout	920	1900	-
elevator_spec2_product21_true-unreach-call.cil.c	exception (gremlins)	3.4	72	-	unknown	1.3	98	-	true	1.4	36	-	true	2.7	200	-	true	0.17	39	-	true	41	79	-	true	210	3300	-	timeout	920	8900	-	timeout	920	1900	-
elevator_spec2_product23_true-unreach-call.cil.c	exception (gremlins)	37	230	-	unknown	1.5	110	-	true	1.5	37	-	true	2.7	200	-	true	0.18	39	-	true	31	77	-	true	210	3400	-	timeout	920	7500	-	timeout	920	1900	-
elevator_spec2_product25_true-unreach-call.cil.c	timeout	920	390	-	unknown	1.5	110	-	true	1.4	36	-	true	2.6	200	-	true	0.19	38	-	true	6.3	44	-	true	150	2600	-	timeout	920	11000	-	timeout	920	1900	-
elevator_spec2_product27_true-unreach-call.cil.c	timeout	920	570	-	unknown	1.3	100	-	true	1.5	37	-	true	2.7	200	-	true	0.17	39	-	true	9.2	57	-	true	150	2500	-	timeout	920	9300	-	timeout	920	1900	-
elevator_spec2_product29_true-unreach-call.cil.c	exception (gremlins)	3.5	75	-	unknown	1.6	110	-	true	1.5	37	-	true	2.7	200	-	true	0.19	39	-	true	25	58	-	true	220	3200	-	timeout	920	7900	-	timeout	920	1900	-
elevator_spec2_product31_true-unreach-call.cil.c	exception (gremlins)	39	280	-	unknown	1.6	110	-	true	1.5	37	-	true	2.8	200	-	true	0.19	39	-	true	35	79	-	true	220	3600	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec3_product01_true-unreach-call.cil.c	timeout	920	400	-	unknown	1.5	110	-	true	2.2	36	-	true	3.1	200	-	true	0.23	38	-	true	4.8	44	-	true	180	2700	-	timeout	920	10000	-	timeout	920	1900	-
elevator_spec3_product09_true-unreach-call.cil.c	timeout	920	410	-	unknown	1.6	110	-	true	2.1	37	-	true	3.0	200	-	true	0.23	38	-	true	5.1	44	-	true	180	2900	-	timeout	920	8800	-	timeout	920	1900	-
elevator_spec3_product17_true-unreach-call.cil.c	timeout	920	400	-	unknown	1.5	100	-	true	2.1	36	-	true	3.2	200	-	true	0.23	38	-	true	5.1	44	-	true	180	2900	-	timeout	920	10000	-	timeout	920	1900	-
elevator_spec3_product18_true-unreach-call.cil.c	timeout	920	530	-	unknown	1.3	98	-	true	2.2	36	-	true	3.2	200	-	true	0.23	38	-	true	9.5	69	-	true	120	3500	-	timeout	920	6900	-	timeout	920	1900	-
elevator_spec3_product21_true-unreach-call.cil.c	exception (gremlins)	2.4	46	-	unknown	1.4	110	-	true	2.5	36	-	true	3.1	200	-	true	0.23	39	-	true	7.7	56	-	true	120	2900	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec3_product22_true-unreach-call.cil.c	exception (gremlins)	2.5	48	-	unknown	1.4	100	-	true	2.5	38	-	true	3.1	200	-	true	0.24	39	-	true	15	110	-	true	130	3100	-	timeout	920	7600	-	timeout	920	1900	-
elevator_spec3_product25_true-unreach-call.cil.c	timeout	920	530	-	unknown	1.3	99	-	true	2.1	36	-	true	3.2	200	-	true	0.21	38	-	true	5.4	44	-	true	200	3100	-	timeout	920	9300	-	timeout	920	1900	-
elevator_spec3_product26_true-unreach-call.cil.c	timeout	920	530	-	unknown	1.5	110	-	true	2.2	38	-	true	3.1	200	-	true	0.22	39	-	true	10	72	-	true	120	4400	-	timeout	920	7500	-	timeout	920	1900	-
elevator_spec3_product29_true-unreach-call.cil.c	exception (gremlins)	2.3	48	-	unknown	1.5	110	-	true	2.5	36	-	true	3.1	200	-	true	0.22	39	-	true	8.0	58	-	true	120	3000	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec3_product30_true-unreach-call.cil.c	exception (gremlins)	2.4	48	-	unknown	1.6	110	-	true	2.6	36	-	true	3.1	200	-	true	0.23	39	-	true	16	120	-	true	130	3200	-	timeout	920	7300	-	timeout	920	1900	-
elevator_spec9_product09_true-unreach-call.cil.c	timeout	920	560	-	unknown	1.6	110	-	true	1.3	36	-	true	2.6	200	-	true	0.17	38	-	true	6.3	44	-	true	130	2200	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec9_product11_true-unreach-call.cil.c	timeout	920	420	-	unknown	1.4	100	-	true	1.5	37	-	true	2.7	200	-	true	0.19	39	-	true	5.9	44	-	true	140	2300	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec9_product25_true-unreach-call.cil.c	timeout	920	440	-	unknown	1.4	100	-	true	1.4	36	-	true	2.7	190	-	true	0.19	38	-	true	6.6	44	-	true	140	2400	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec9_product27_true-unreach-call.cil.c	timeout	920	580	-	unknown	1.3	100	-	true	1.5	37	-	true	2.8	200	-	true	0.20	39	-	true	5.8	44	-	true	150	2600	-	timeout	920	13000	-	timeout	920	3200	-
elevator_spec9_product29_true-unreach-call.cil.c	exception (gremlins)	19	110	-	unknown	1.5	110	-	true	1.4	37	-	true	2.7	200	-	true	0.19	39	-	true	29	76	-	true	220	3400	-	timeout	920	12000	-	timeout	920	1900	-
elevator_spec9_product31_true-unreach-call.cil.c	exception (gremlins)	32	280	-	unknown	1.6	110	-	true	1.6	37	-	true	3.3	200	-	true	0.18	39	-	true	28	76	-	true	220	3600	-	timeout	920	13000	-	timeout	920	1900	-
email_spec0_product16_false-unreach-call.cil.c	witness confirmed	400	340	23	unknown	1.2	99	-	true	1.2	45	-	witness confirmed	16	820	23	witness confirmed	0.82	79	19	witness confirmed	1.6	50	20	witness confirmed	6.9	370	20	unknown	5.3	240	-	unknown	5.7	240	-
email_spec0_product21_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.4	100	-	true	2.2	48	-	witness confirmed	17	850	33	witness confirmed	1.1	91	21	witness confirmed	5.5	75	20	witness confirmed	11	510	21	unknown	5.7	240	-	unknown	5.3	240	-
email_spec0_product22_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.3	96	-	true	1.3	45	-	witness confirmed	18	860	32	witness confirmed	0.86	82	22	witness confirmed	2.4	57	21	witness confirmed	7.7	400	21	unknown	5.6	240	-	unknown	5.8	240	-
email_spec0_product26_false-unreach-call.cil.c	timeout	920	490	-	unknown	1.4	110	-	true	2.4	49	-	witness confirmed	19	870	33	witness confirmed	1.2	110	22	witness confirmed	5.5	80	21	witness confirmed	11	540	22	unknown	5.8	240	-	unknown	5.7	240	-
email_spec0_product31_false-unreach-call.cil.c	timeout	920	410	-	unknown	1.3	98	-	witness confirmed	1.5	46	22	witness confirmed	20	870	36	witness confirmed	1.1	110	22	witness confirmed	3.3	67	21	witness confirmed	8.2	420	22	unknown	5.9	240	-	unknown	5.5	240	-
email_spec0_product33_false-unreach-call.cil.c	timeout	920	510	-	unknown	1.5	110	-	true	1.5	46	-	witness confirmed	18	880	37	witness confirmed	1.2	110	24	witness confirmed	2.6	60	24	witness confirmed	8.4	400	24	unknown	5.5	240	-	unknown	5.7	240	-
email_spec0_product34_false-unreach-call.cil.c	timeout	920	560	-	unknown	1.3	110	-	witness confirmed	3.2	55	22	witness confirmed	18	930	35	witness confirmed	1.5	120	22	witness confirmed	6.2	90	22	witness confirmed	12	590	22	unknown	5.7	240	-	unknown	6.0	240	-
email_spec0_product35_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.3	100	-	witness confirmed	3.4	56	24	witness confirmed	19	950	35	witness confirmed	1.6	130	30	witness confirmed	7.7	93	24	witness confirmed	13	610	30	unknown	5.3	240	-	unknown	5.3	240	-
email_spec0_productSimulator_false-unreach-call.cil.c	timeout	920	5900	-	unknown	1.5	110	-	true	850	900	-	witness timeout	24	1300	93	witness timeout	13	740	93	witness timeout	140	650	93	witness timeout	380	3100	93	unknown	5.9	240	-	unknown	5.3	240	-
email_spec11_product15_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.4	110	-	witness confirmed	1.2	44	20	witness confirmed	17	850	21	witness confirmed	0.47	62	20	witness confirmed	1.8	59	19	witness confirmed	7.1	330	19	unknown	5.5	240	-	unknown	5.4	240	-
email_spec11_product20_false-unreach-call.cil.c	timeout	920	390	-	unknown	1.2	100	-	witness confirmed	2.1	49	20	witness confirmed	17	850	22	witness confirmed	0.72	77	20	witness confirmed	3.5	71	19	witness confirmed	9.8	480	19	unknown	5.7	240	-	unknown	5.4	240	-
email_spec11_product22_false-unreach-call.cil.c	timeout	920	530	-	unknown	1.4	110	-	witness confirmed	1.4	44	19	witness confirmed	17	830	22	witness confirmed	0.85	82	19	witness confirmed	3.3	69	19	witness confirmed	7.5	390	19	unknown	5.5	240	-	unknown	5.4	240	-
email_spec11_product26_false-unreach-call.cil.c	timeout	920	560	-	unknown	1.3	99	-	witness confirmed	2.5	50	20	witness confirmed	17	870	22	witness confirmed	1.2	110	20	witness confirmed	5.9	79	20	witness confirmed	11	500	20	unknown	5.8	240	-	unknown	5.3	240	-
email_spec11_product30_false-unreach-call.cil.c	timeout	920	590	-	unknown	1.5	110	-	witness confirmed	1.4	45	23	witness confirmed	18	850	33	witness confirmed	0.52	65	23	witness confirmed	2.0	53	22	witness confirmed	7.7	390	23	unknown	5.5	240	-	unknown	5.6	240	-
email_spec11_product32_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.2	110	-	witness confirmed	2.8	52	22	witness confirmed	19	1000	34	witness confirmed	0.78	82	23	witness confirmed	5.7	82	23	witness confirmed	12	540	23	unknown	5.5	240	-	unknown	5.5	240	-
email_spec11_product33_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.4	110	-	true	1.5	47	-	witness confirmed	19	870	33	witness confirmed	1.2	110	23	witness confirmed	2.9	60	23	witness confirmed	8.5	380	23	unknown	5.7	240	-	unknown	6.0	240	-
email_spec11_product35_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.5	110	-	witness confirmed	3.3	57	24	witness confirmed	19	940	34	witness confirmed	1.7	130	23	witness confirmed	7.0	93	23	witness confirmed	13	570	23	unknown	5.7	240	-	unknown	6.7	240	-
email_spec11_productSimulator_false-unreach-call.cil.c	timeout	920	5300	-	unknown	1.4	110	-	true	850	1000	-	witness timeout	28	1400	93	witness timeout	14	820	93	witness timeout	190	690	94	timeout	920	3200	-	unknown	5.6	250	-	unknown	5.4	240	-
email_spec1_product14_false-unreach-call.cil.c	timeout	920	900	-	unknown	1.4	100	-	witness confirmed	1.2	45	24	witness confirmed	19	840	52	witness confirmed	0.55	65	25	witness confirmed	1.6	53	23	witness confirmed	9.9	420	23	unknown	5.8	240	-	unknown	5.3	240	-
email_spec1_product15_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.6	110	-	true	1.1	45	-	witness confirmed	18	850	36	witness confirmed	0.47	63	24	witness confirmed	1.1	45	23	witness confirmed	7.5	360	23	unknown	5.3	240	-	unknown	5.6	240	-
email_spec1_product16_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.4	110	-	witness confirmed	1.3	45	31	witness confirmed	20	850	54	witness confirmed	0.82	80	31	witness confirmed	1.5	46	24	witness confirmed	8.0	340	31	unknown	5.2	240	-	unknown	5.3	240	-
email_spec1_product20_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.4	110	-	witness confirmed	2.0	49	24	witness confirmed	19	870	38	witness confirmed	0.66	76	30	witness confirmed	2.9	64	23	witness confirmed	9.7	480	24	unknown	5.5	240	-	unknown	5.9	240	-
email_spec1_product21_false-unreach-call.cil.c	timeout	920	530	-	unknown	1.4	100	-	witness confirmed	2.2	48	24	witness confirmed	19	970	53	witness confirmed	1.2	92	31	witness confirmed	3.3	71	32	witness confirmed	11	500	31	unknown	6.6	240	-	unknown	5.8	240	-
email_spec1_product22_false-unreach-call.cil.c	timeout	920	410	-	unknown	1.3	100	-	witness confirmed	1.3	46	24	witness confirmed	17	850	37	witness confirmed	0.90	83	23	witness confirmed	2.3	51	23	witness confirmed	8.2	370	23	unknown	5.7	240	-	unknown	5.2	240	-
email_spec1_product26_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.4	110	-	witness confirmed	2.5	48	32	witness confirmed	18	930	40	witness confirmed	1.3	110	30	witness confirmed	3.6	74	32	witness confirmed	11	510	31	unknown	5.7	240	-	unknown	5.6	240	-
email_spec1_product29_false-unreach-call.cil.c	timeout	920	780	-	unknown	1.3	97	-	witness confirmed	1.4	45	33	witness confirmed	21	870	62	witness confirmed	0.57	68	34	witness confirmed	2.0	52	35	witness confirmed	11	470	33	unknown	5.5	240	-	unknown	5.9	240	-
email_spec1_product30_false-unreach-call.cil.c	timeout	920	660	-	unknown	1.3	100	-	witness confirmed	1.4	45	35	witness confirmed	19	920	52	witness confirmed	0.50	66	33	witness confirmed	2.1	50	34	witness confirmed	8.5	380	33	unknown	5.8	240	-	unknown	5.5	240	-
email_spec1_product31_false-unreach-call.cil.c	timeout	920	410	-	unknown	1.3	100	-	witness confirmed	1.5	46	36	witness confirmed	21	1000	65	witness confirmed	1.1	110	35	witness confirmed	1.9	50	36	witness confirmed	9.1	420	36	unknown	5.8	240	-	unknown	5.5	240	-
email_spec1_product32_false-unreach-call.cil.c	timeout	920	800	-	unknown	1.4	100	-	witness confirmed	2.5	49	35	witness confirmed	19	1100	54	witness confirmed	0.72	81	36	witness confirmed	4.6	75	37	witness confirmed	12	500	35	unknown	5.4	240	-	unknown	5.6	240	-
email_spec1_product33_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.3	100	-	witness confirmed	1.5	46	35	witness confirmed	20	900	53	witness confirmed	1.3	110	35	witness confirmed	2.1	54	36	witness confirmed	9.1	410	34	unknown	5.5	240	-	unknown	5.7	240	-
email_spec1_product34_false-unreach-call.cil.c	timeout	920	660	-	unknown	1.3	98	-	witness confirmed	3.1	54	35	witness confirmed	20	1100	61	witness confirmed	1.5	120	35	witness confirmed	4.2	81	36	witness confirmed	13	590	34	unknown	5.4	240	-	unknown	5.8	240	-
email_spec1_product35_false-unreach-call.cil.c	timeout	920	810	-	unknown	1.4	100	-	witness confirmed	3.4	55	36	witness confirmed	20	960	58	witness confirmed	1.7	130	36	witness confirmed	5.5	85	37	witness confirmed	13	590	37	unknown	5.3	240	-	unknown	5.3	240	-
email_spec1_productSimulator_false-unreach-call.cil.c	timeout	920	2200	-	unknown	1.8	120	-	witness timeout	120	340	93	witness timeout	28	1400	92	witness timeout	5.6	360	93	witness timeout	47	290	93	witness timeout	150	3200	93	unknown	5.8	240	-	unknown	5.6	240	-
email_spec27_product17_false-unreach-call.cil.c	witness confirmed	60	140	60	unknown	1.3	100	-	witness confirmed	1.4	45	32	witness timeout	16	830	110	witness confirmed	0.53	67	31	witness confirmed	1.9	55	33	witness confirmed	10.0	470	31	unknown	5.4	240	-	unknown	5.4	240	-
email_spec27_product18_false-unreach-call.cil.c	witness confirmed	6.5	110	59	unknown	1.3	98	-	witness confirmed	1.3	46	31	witness confirmed	21	820	55	witness confirmed	0.49	64	32	witness confirmed	1.8	58	33	witness confirmed	8.1	340	32	unknown	5.5	240	-	unknown	5.7	240	-
email_spec27_product19_false-unreach-call.cil.c	witness confirmed	61	150	61	unknown	1.1	97	-	witness confirmed	1.2	46	33	witness confirmed	20	870	83	witness confirmed	0.86	83	33	witness confirmed	1.9	53	33	witness confirmed	8.2	340	33	unknown	5.3	240	-	unknown	5.3	240	-
email_spec27_product23_false-unreach-call.cil.c	witness confirmed	7.3	110	65	unknown	1.4	110	-	witness confirmed	2.3	49	34	witness timeout	18	840	110	witness confirmed	0.68	78	34	witness confirmed	3.7	71	34	witness confirmed	11	460	34	unknown	5.6	240	-	unknown	5.7	240	-
email_spec27_product24_false-unreach-call.cil.c	witness timeout	6.7	110	110	unknown	1.4	110	-	witness confirmed	1.4	45	33	witness confirmed	18	870	59	witness confirmed	0.98	86	34	witness confirmed	2.2	53	34	witness confirmed	8.6	390	33	unknown	5.4	240	-	unknown	5.4	240	-
email_spec27_product25_false-unreach-call.cil.c	witness confirmed	65	140	68	unknown	1.4	110	-	witness confirmed	2.5	48	35	witness timeout	18	930	110	witness confirmed	1.2	110	34	witness confirmed	4.3	73	34	witness confirmed	11	510	34	unknown	5.6	240	-	unknown	5.5	240	-
email_spec27_product27_false-unreach-call.cil.c	witness timeout	6.9	120	110	unknown	1.1	98	-	witness confirmed	2.7	50	37	witness timeout	17	890	110	witness confirmed	1.4	120	35	witness confirmed	5.3	78	37	witness confirmed	13	520	35	unknown	5.5	240	-	unknown	5.8	240	-
email_spec27_product29_false-unreach-call.cil.c	witness timeout	130	290	110	unknown	1.3	97	-	witness confirmed	1.5	47	38	witness timeout	18	860	110	witness confirmed	0.56	70	37	witness confirmed	2.7	64	37	witness confirmed	12	530	36	unknown	5.5	240	-	unknown	6.0	240	-
email_spec27_product30_false-unreach-call.cil.c	witness timeout	390	280	110	unknown	1.4	110	-	witness confirmed	1.5	45	36	witness timeout	21	920	110	witness confirmed	0.56	68	37	witness confirmed	1.9	52	37	witness confirmed	8.8	390	36	unknown	5.9	240	-	unknown	5.5	240	-
email_spec27_product31_false-unreach-call.cil.c	witness timeout	590	430	110	unknown	1.4	110	-	witness confirmed	1.6	47	38	witness timeout	21	970	110	witness confirmed	1.2	110	38	witness confirmed	2.3	53	37	witness confirmed	9.4	360	37	unknown	5.5	240	-	unknown	5.7	240	-
email_spec27_product32_false-unreach-call.cil.c	witness timeout	410	280	110	unknown	1.3	110	-	witness confirmed	3.1	52	41	witness timeout	19	940	110	witness confirmed	0.76	85	41	witness confirmed	4.7	87	41	witness confirmed	13	520	40	unknown	5.6	240	-	unknown	5.5	240	-
email_spec27_product33_false-unreach-call.cil.c	witness timeout	270	220	110	unknown	1.1	98	-	witness confirmed	1.6	46	38	witness timeout	18	890	110	witness confirmed	1.2	110	40	witness confirmed	2.4	59	40	witness confirmed	9.5	380	38	unknown	5.8	240	-	unknown	5.3	240	-
email_spec27_product34_false-unreach-call.cil.c	witness timeout	660	470	110	unknown	1.5	110	-	true	3.5	56	-	witness timeout	21	930	110	witness confirmed	1.6	120	40	witness confirmed	5.7	93	40	witness confirmed	14	540	40	unknown	5.6	240	-	unknown	5.3	240	-
email_spec27_product35_false-unreach-call.cil.c	witness timeout	280	240	110	unknown	1.4	110	-	witness confirmed	3.8	57	48	witness timeout	22	980	110	witness confirmed	1.7	130	47	witness confirmed	6.3	96	48	witness confirmed	15	600	49	unknown	5.9	240	-	unknown	5.6	240	-
email_spec27_productSimulator_false-unreach-call.cil.c	witness timeout	48	410	92	unknown	1.3	100	-	witness timeout	300	520	92	witness timeout	29	1400	92	witness timeout	8.4	490	93	witness timeout	130	520	92	witness timeout	290	3100	93	unknown	6.0	240	-	unknown	5.9	240	-
email_spec3_product13_false-unreach-call.cil.c	witness confirmed	77	140	13	unknown	1.4	100	-	witness confirmed	0.45	39	10	witness confirmed	18	780	16	witness confirmed	0.46	63	10	witness confirmed	0.86	37	9.7	witness confirmed	6.8	330	9.6	unknown	5.5	240	-	unknown	5.5	240	-
email_spec3_product17_false-unreach-call.cil.c	witness confirmed	82	140	14	unknown	1.3	97	-	witness confirmed	0.60	43	10	witness confirmed	18	830	14	witness confirmed	0.61	72	11	witness confirmed	1.1	41	10.0	witness confirmed	10	450	10	unknown	5.8	240	-	unknown	5.5	240	-
email_spec3_product18_false-unreach-call.cil.c	witness confirmed	4.6	95	12	unknown	1.4	100	-	unknown	0.51	40	-	witness confirmed	18	780	16	witness confirmed	0.56	68	9.5	witness confirmed	0.98	43	9.1	witness confirmed	7.4	360	9.5	unknown	5.4	240	-	unknown	5.3	240	-
email_spec3_product19_false-unreach-call.cil.c	witness confirmed	76	140	12	unknown	1.3	110	-	unknown	0.55	42	-	witness confirmed	19	780	12	witness confirmed	1.1	100	10	witness confirmed	1.1	43	8.8	witness confirmed	7.5	390	9.4	unknown	5.5	240	-	unknown	5.2	240	-
email_spec3_product23_false-unreach-call.cil.c	witness confirmed	5.5	94	12	unknown	1.3	100	-	unknown	0.96	46	-	witness confirmed	19	830	13	witness confirmed	0.81	81	10.0	witness confirmed	2.1	60	9.4	witness confirmed	11	500	10	unknown	5.5	240	-	unknown	5.5	240	-
email_spec3_product24_false-unreach-call.cil.c	witness confirmed	4.9	92	11	unknown	1.3	110	-	unknown	0.58	40	-	witness confirmed	17	770	12	witness confirmed	1.2	110	9.5	witness confirmed	1.2	45	8.7	witness confirmed	8.4	420	8.8	unknown	5.4	240	-	unknown	5.5	240	-
email_spec3_product25_false-unreach-call.cil.c	witness confirmed	81	140	13	unknown	1.3	98	-	witness confirmed	1.1	45	11	witness confirmed	17	820	13	witness confirmed	1.4	120	10	witness confirmed	2.6	62	9.7	witness confirmed	11	490	9.9	unknown	5.8	240	-	unknown	5.3	240	-
email_spec3_product27_false-unreach-call.cil.c	witness confirmed	5.5	95	13	unknown	1.3	97	-	witness confirmed	1.2	47	9.9	witness confirmed	16	830	17	witness confirmed	1.8	120	10	witness confirmed	2.6	66	9.5	witness confirmed	13	530	10	unknown	5.3	240	-	unknown	5.5	240	-
email_spec3_product28_false-unreach-call.cil.c	witness confirmed	120	140	19	unknown	1.3	99	-	witness confirmed	0.47	40	14	witness confirmed	18	810	34	witness confirmed	0.45	62	14	witness confirmed	0.94	39	14	witness confirmed	7.2	380	14	unknown	5.6	240	-	unknown	5.9	240	-
email_spec3_product29_false-unreach-call.cil.c	witness confirmed	130	150	20	unknown	1.3	98	-	witness confirmed	0.65	44	15	witness confirmed	19	830	31	witness confirmed	0.64	75	15	witness confirmed	1.5	45	14	witness confirmed	12	530	14	unknown	5.8	240	-	unknown	5.6	240	-
email_spec3_product30_false-unreach-call.cil.c	witness confirmed	5.7	110	20	unknown	1.3	100	-	witness confirmed	0.59	41	14	witness confirmed	17	810	21	witness confirmed	0.60	71	15	witness confirmed	1.2	46	14	witness confirmed	8.3	370	14	unknown	5.7	240	-	unknown	5.4	240	-
email_spec3_product31_false-unreach-call.cil.c	witness confirmed	130	150	19	unknown	1.4	110	-	witness confirmed	0.66	42	14	witness confirmed	20	820	21	witness confirmed	1.3	110	14	witness confirmed	1.4	47	14	witness confirmed	8.1	430	14	unknown	5.3	240	-	unknown	5.3	230	-
email_spec3_product32_false-unreach-call.cil.c	witness confirmed	6.4	110	19	unknown	1.5	110	-	unknown	1.3	48	-	witness confirmed	18	860	38	witness confirmed	0.89	87	15	witness confirmed	3.4	78	14	witness confirmed	13	600	15	unknown	5.5	240	-	unknown	5.6	240	-
email_spec3_product33_false-unreach-call.cil.c	witness confirmed	5.9	110	19	unknown	1.4	110	-	witness confirmed	0.69	41	14	witness confirmed	18	810	31	witness confirmed	1.6	110	14	witness confirmed	1.6	53	14	witness confirmed	9.1	410	14	unknown	6.6	240	-	unknown	5.3	240	-
email_spec3_product34_false-unreach-call.cil.c	witness confirmed	140	140	20	unknown	1.5	110	-	witness confirmed	1.5	47	14	witness confirmed	16	850	37	witness confirmed	1.8	130	15	witness confirmed	3.6	83	14	witness confirmed	13	560	14	unknown	5.3	240	-	unknown	5.4	240	-
email_spec3_product35_false-unreach-call.cil.c	witness confirmed	6.4	110	20	unknown	1.4	110	-	unknown	1.6	51	-	witness confirmed	17	870	28	witness confirmed	1.9	130	16	witness confirmed	3.7	86	14	witness confirmed	15	620	14	unknown	5.3	240	-	unknown	5.6	240	-
email_spec3_productSimulator_false-unreach-call.cil.c	witness timeout	17	160	92	unknown	1.4	110	-	witness timeout	66	380	93	witness timeout	25	1200	93	witness timeout	6.2	370	93	witness timeout	52	300	92	witness timeout	110	3500	92	unknown	5.5	240	-	unknown	5.2	240	-
email_spec4_product18_false-unreach-call.cil.c	timeout	920	550	-	unknown	1.6	110	-	witness confirmed	1.2	45	23	witness confirmed	18	840	37	witness confirmed	0.47	63	23	witness confirmed	1.2	45	22	witness confirmed	6.9	360	23	unknown	5.5	240	-	unknown	5.6	240	-
email_spec4_product19_false-unreach-call.cil.c	timeout	920	560	-	unknown	1.3	97	-	witness confirmed	1.3	45	31	witness confirmed	19	890	53	witness confirmed	0.89	82	31	witness confirmed	1.3	45	24	witness confirmed	7.9	370	31	unknown	5.7	240	-	unknown	5.5	240	-
email_spec4_product23_false-unreach-call.cil.c	timeout	920	440	-	unknown	1.4	100	-	witness confirmed	2.0	47	24	witness confirmed	18	980	40	witness confirmed	0.66	75	24	witness confirmed	2.0	56	23	witness confirmed	11	460	24	unknown	5.6	240	-	unknown	5.4	240	-
email_spec4_product24_false-unreach-call.cil.c	timeout	920	570	-	unknown	1.5	100	-	true	1.3	46	-	witness confirmed	18	860	38	witness confirmed	1.0	84	23	witness confirmed	1.7	50	24	witness confirmed	7.7	360	23	unknown	5.5	240	-	unknown	5.8	240	-
email_spec4_product25_false-unreach-call.cil.c	timeout	920	460	-	unknown	1.3	98	-	witness confirmed	2.3	48	32	witness confirmed	18	940	57	witness confirmed	1.2	110	31	witness confirmed	2.5	58	33	witness confirmed	11	470	33	unknown	5.8	240	-	unknown	5.6	240	-
email_spec4_product27_false-unreach-call.cil.c	timeout	920	1000	-	unknown	1.4	110	-	true	2.4	48	-	witness confirmed	17	930	46	witness confirmed	1.5	110	30	witness confirmed	2.6	60	23	witness confirmed	12	500	30	unknown	5.4	240	-	unknown	5.8	240	-
email_spec4_product30_false-unreach-call.cil.c	timeout	920	400	-	unknown	1.4	110	-	witness confirmed	1.4	45	33	witness confirmed	18	810	51	witness confirmed	0.50	65	33	witness confirmed	1.4	48	32	witness confirmed	7.9	360	32	unknown	5.8	240	-	unknown	5.5	240	-
email_spec4_product31_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.4	100	-	true	1.5	47	-	witness timeout	23	990	110	witness confirmed	1.2	110	36	witness confirmed	1.9	50	37	witness confirmed	8.4	420	35	unknown	5.5	240	-	unknown	5.4	240	-
email_spec4_product32_false-unreach-call.cil.c	timeout	920	530	-	unknown	1.5	110	-	witness confirmed	2.5	49	34	witness confirmed	18	930	54	witness confirmed	0.74	82	34	witness confirmed	3.1	65	35	witness confirmed	12	540	34	unknown	5.5	240	-	unknown	6.7	240	-
email_spec4_product33_false-unreach-call.cil.c	timeout	920	560	-	unknown	1.3	98	-	true	1.5	46	-	witness timeout	18	870	100	witness confirmed	1.2	110	33	witness confirmed	2.0	54	33	witness confirmed	8.5	390	33	unknown	5.5	240	-	unknown	5.4	240	-
email_spec4_product34_false-unreach-call.cil.c	timeout	920	530	-	unknown	1.5	110	-	witness confirmed	3.2	53	38	witness timeout	17	980	110	witness confirmed	1.6	120	37	witness confirmed	4.0	71	37	witness confirmed	13	590	37	unknown	5.7	240	-	unknown	5.7	240	-
email_spec4_product35_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.5	120	-	true	3.3	55	-	witness confirmed	18	960	57	witness confirmed	1.8	130	35	witness confirmed	4.1	73	35	witness confirmed	13	580	34	unknown	5.7	240	-	unknown	5.5	240	-
email_spec4_productSimulator_false-unreach-call.cil.c	timeout	920	1700	-	unknown	1.6	110	-	witness timeout	120	350	93	witness timeout	28	1700	93	witness timeout	5.6	350	92	witness timeout	42	290	93	witness timeout	160	3200	92	unknown	5.5	240	-	unknown	5.8	240	-
email_spec6_product12_false-unreach-call.cil.c	timeout	920	610	-	unknown	1.4	97	-	witness confirmed	1.0	44	18	witness confirmed	19	810	22	witness confirmed	0.42	60	19	witness confirmed	1.1	52	18	witness confirmed	6.4	300	19	unknown	5.5	240	-	unknown	5.9	240	-
email_spec6_product14_false-unreach-call.cil.c	timeout	920	610	-	unknown	1.4	110	-	witness confirmed	1.3	45	19	witness confirmed	16	830	22	witness confirmed	0.65	73	20	witness confirmed	1.7	46	18	witness confirmed	9.7	420	19	unknown	5.6	240	-	unknown	5.4	240	-
email_spec6_product15_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.3	110	-	witness confirmed	1.2	44	19	witness confirmed	19	870	22	witness confirmed	0.56	69	19	witness confirmed	1.6	47	20	witness confirmed	7.3	340	18	unknown	5.5	240	-	unknown	5.5	240	-
email_spec6_product16_false-unreach-call.cil.c	timeout	920	590	-	unknown	1.4	100	-	true	1.3	46	-	witness confirmed	19	850	22	witness confirmed	0.99	85	19	witness confirmed	1.8	50	19	witness confirmed	7.7	330	19	unknown	5.4	240	-	unknown	5.4	240	-
email_spec6_product20_false-unreach-call.cil.c	timeout	920	450	-	unknown	1.5	100	-	true	2.1	48	-	witness confirmed	18	870	22	witness confirmed	0.80	81	19	witness confirmed	4.0	71	19	witness confirmed	11	490	19	unknown	5.4	240	-	unknown	5.4	240	-
email_spec6_product21_false-unreach-call.cil.c	timeout	920	730	-	unknown	1.4	110	-	true	2.4	49	-	witness confirmed	18	870	23	witness confirmed	1.3	120	19	witness confirmed	5.4	75	19	witness confirmed	11	490	19	unknown	5.3	240	-	unknown	5.2	240	-
email_spec6_product22_false-unreach-call.cil.c	timeout	920	590	-	unknown	1.3	98	-	witness confirmed	1.4	46	20	witness confirmed	18	860	23	witness confirmed	1.1	110	19	witness confirmed	2.2	53	19	witness confirmed	7.8	400	19	unknown	5.4	240	-	unknown	5.3	240	-
email_spec6_product26_false-unreach-call.cil.c	witness confirmed	690	420	34	unknown	1.3	98	-	true	2.5	50	-	witness confirmed	17	860	22	witness confirmed	1.5	120	19	witness confirmed	4.7	77	19	witness confirmed	13	510	19	unknown	5.9	240	-	unknown	5.5	240	-
email_spec6_product28_false-unreach-call.cil.c	timeout	920	430	-	unknown	1.1	100	-	witness confirmed	1.1	44	21	witness confirmed	19	830	24	witness confirmed	0.44	62	21	witness confirmed	1.3	56	21	witness confirmed	7.3	370	21	unknown	5.3	240	-	unknown	5.5	240	-
email_spec6_product29_false-unreach-call.cil.c	timeout	920	350	-	unknown	1.3	99	-	witness confirmed	1.5	48	20	witness confirmed	17	930	32	witness confirmed	0.72	76	20	witness confirmed	2.3	51	20	witness confirmed	11	540	20	unknown	5.4	240	-	unknown	5.4	240	-
email_spec6_product30_false-unreach-call.cil.c	witness confirmed	600	320	23	unknown	1.5	110	-	witness confirmed	1.5	46	20	witness confirmed	17	830	23	witness confirmed	0.60	71	22	witness confirmed	2.5	62	20	witness confirmed	7.9	400	20	unknown	5.7	240	-	unknown	5.9	240	-
email_spec6_product31_false-unreach-call.cil.c	timeout	920	520	-	unknown	1.4	110	-	true	1.5	46	-	witness confirmed	19	870	20	witness confirmed	1.3	110	21	witness confirmed	2.1	52	20	witness confirmed	8.4	420	20	unknown	5.3	240	-	unknown	5.5	240	-
email_spec6_product32_false-unreach-call.cil.c	witness confirmed	640	330	24	unknown	1.5	110	-	witness confirmed	2.9	52	19	witness confirmed	18	910	32	witness confirmed	0.88	86	21	witness confirmed	4.1	79	20	witness confirmed	12	520	21	unknown	5.6	240	-	unknown	5.6	240	-
email_spec6_product33_false-unreach-call.cil.c	timeout	920	480	-	unknown	1.6	120	-	witness confirmed	1.7	46	21	witness confirmed	19	840	24	witness confirmed	1.4	110	21	witness confirmed	2.6	56	21	witness confirmed	8.8	400	20	unknown	5.5	240	-	unknown	5.4	240	-
email_spec6_product34_false-unreach-call.cil.c	timeout	920	550	-	unknown	1.3	100	-	witness confirmed	3.4	56	21	witness confirmed	19	930	33	witness confirmed	1.9	130	21	witness confirmed	5.0	85	21	witness confirmed	13	540	21	unknown	5.6	240	-	unknown	5.4	240	-
email_spec6_product35_false-unreach-call.cil.c	witness confirmed	700	440	33	unknown	1.4	110	-	true	3.6	58	-	witness confirmed	18	930	32	witness confirmed	1.9	130	21	witness confirmed	6.1	88	20	witness confirmed	14	610	20	unknown	5.9	240	-	unknown	5.8	240	-
email_spec6_productSimulator_false-unreach-call.cil.c	timeout	920	1400	-	unknown	1.2	100	-	witness timeout	130	350	92	witness timeout	26	1300	93	witness timeout	6.0	370	93	witness timeout	53	290	93	witness timeout	160	3200	93	unknown	6.8	240	-	unknown	5.4	240	-
email_spec7_product28_false-unreach-call.cil.c	timeout	920	550	-	unknown	1.3	99	-	witness confirmed	1.1	45	21	witness confirmed	20	840	23	witness confirmed	0.38	55	20	witness confirmed	1.2	50	20	witness confirmed	7.2	360	20	unknown	5.5	240	-	unknown	5.9	240	-
email_spec7_product29_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.3	98	-	witness confirmed	1.5	48	19	witness confirmed	18	920	22	witness confirmed	0.52	67	20	witness confirmed	2.1	58	19	witness confirmed	11	520	19	unknown	5.3	240	-	unknown	5.7	240	-
email_spec7_product30_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.3	98	-	witness confirmed	1.4	45	20	witness confirmed	17	830	24	witness confirmed	0.47	63	20	witness confirmed	1.9	50	20	witness confirmed	7.4	390	21	unknown	5.5	240	-	unknown	5.5	240	-
email_spec7_product31_false-unreach-call.cil.c	timeout	920	520	-	unknown	1.3	100	-	true	1.5	45	-	witness confirmed	19	850	23	witness confirmed	1.1	86	20	witness confirmed	2.1	51	19	witness confirmed	8.1	370	19	unknown	5.4	240	-	unknown	5.4	240	-
email_spec7_product32_false-unreach-call.cil.c	timeout	920	410	-	unknown	1.4	100	-	true	2.5	50	-	witness confirmed	18	920	31	witness confirmed	0.70	76	22	witness confirmed	4.5	77	21	witness confirmed	11	540	20	unknown	5.6	240	-	unknown	5.8	240	-
email_spec7_product33_false-unreach-call.cil.c	timeout	920	410	-	unknown	1.3	96	-	true	1.5	45	-	witness confirmed	17	830	22	witness confirmed	1.1	110	19	witness confirmed	2.3	56	19	witness confirmed	8.1	390	19	unknown	5.4	240	-	unknown	5.3	240	-
email_spec7_product34_false-unreach-call.cil.c	timeout	920	410	-	unknown	1.3	100	-	witness confirmed	3.1	53	20	witness confirmed	18	920	31	witness confirmed	1.4	120	21	witness confirmed	4.7	84	19	witness confirmed	12	590	20	unknown	5.5	240	-	unknown	5.4	240	-
email_spec7_product35_false-unreach-call.cil.c	timeout	920	420	-	unknown	1.4	100	-	true	3.3	55	-	witness confirmed	18	930	30	witness confirmed	1.7	120	20	witness confirmed	9.5	88	19	witness confirmed	13	590	20	unknown	5.4	240	-	unknown	5.3	240	-
email_spec7_productSimulator_false-unreach-call.cil.c	timeout	920	2700	-	unknown	1.3	110	-	witness timeout	160	410	93	witness timeout	26	1200	93	witness timeout	6.0	380	93	witness timeout	49	300	93	witness timeout	180	3200	92	unknown	5.3	240	-	unknown	5.7	240	-
email_spec8_product15_false-unreach-call.cil.c	timeout	920	550	-	unknown	1.4	110	-	witness confirmed	1.2	45	24	witness confirmed	20	840	39	witness confirmed	0.58	68	25	witness confirmed	1.4	45	24	witness confirmed	7.5	350	24	unknown	5.4	240	-	unknown	5.4	240	-
email_spec8_product16_false-unreach-call.cil.c	timeout	920	710	-	unknown	1.4	100	-	witness confirmed	1.3	44	33	witness confirmed	19	900	54	witness confirmed	0.95	84	32	witness confirmed	1.3	46	25	witness confirmed	7.8	340	32	unknown	5.5	240	-	unknown	5.4	240	-
email_spec8_product20_false-unreach-call.cil.c	timeout	920	660	-	unknown	1.1	99	-	witness confirmed	2.0	48	33	witness confirmed	19	870	43	witness confirmed	0.80	79	32	witness confirmed	2.3	63	34	witness confirmed	10	450	33	unknown	5.3	240	-	unknown	5.9	240	-
email_spec8_product21_false-unreach-call.cil.c	timeout	920	530	-	unknown	1.3	100	-	true	2.2	48	-	witness confirmed	19	1000	57	witness confirmed	1.3	110	33	witness confirmed	3.6	68	35	witness confirmed	11	500	33	unknown	5.3	240	-	unknown	5.8	240	-
email_spec8_product22_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.4	100	-	witness confirmed	1.4	45	31	witness confirmed	20	840	25	witness confirmed	1.1	100	31	witness confirmed	2.3	51	24	witness confirmed	8.2	360	31	unknown	5.5	240	-	unknown	5.4	240	-
email_spec8_product26_false-unreach-call.cil.c	timeout	920	660	-	unknown	1.3	100	-	witness confirmed	2.5	49	33	witness confirmed	17	960	48	witness confirmed	1.5	120	32	witness confirmed	3.3	74	34	witness confirmed	12	540	32	unknown	5.4	240	-	unknown	5.8	240	-
email_spec8_product30_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.3	100	-	true	1.4	46	-	witness confirmed	19	850	53	witness confirmed	0.60	72	33	witness confirmed	1.5	48	34	witness confirmed	8.3	350	34	unknown	5.8	240	-	unknown	5.7	240	-
email_spec8_product31_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.4	100	-	witness confirmed	1.5	46	37	witness timeout	23	1000	94	witness confirmed	1.4	110	37	witness confirmed	1.7	50	37	witness confirmed	8.7	410	36	unknown	5.4	240	-	unknown	5.9	240	-
email_spec8_product32_false-unreach-call.cil.c	timeout	920	800	-	unknown	1.4	100	-	witness confirmed	2.7	50	39	witness confirmed	18	980	58	witness confirmed	0.89	85	38	witness confirmed	3.4	75	38	witness confirmed	12	510	36	unknown	5.6	240	-	unknown	5.7	240	-
email_spec8_product33_false-unreach-call.cil.c	timeout	920	660	-	unknown	1.3	98	-	witness confirmed	1.6	45	37	witness confirmed	22	910	57	witness confirmed	1.7	110	37	witness confirmed	1.9	54	37	witness confirmed	9.3	410	37	unknown	5.7	240	-	unknown	5.8	240	-
email_spec8_product34_false-unreach-call.cil.c	timeout	920	900	-	unknown	1.4	110	-	witness confirmed	3.0	54	41	witness timeout	19	1100	110	witness confirmed	1.7	130	40	witness confirmed	3.9	81	42	witness confirmed	13	590	40	unknown	5.7	240	-	unknown	5.4	240	-
email_spec8_product35_false-unreach-call.cil.c	timeout	920	930	-	unknown	1.4	110	-	witness confirmed	3.3	56	41	witness confirmed	17	970	62	witness confirmed	1.9	130	39	witness confirmed	5.0	84	40	witness confirmed	14	560	39	unknown	5.6	240	-	unknown	5.5	240	-
email_spec8_productSimulator_false-unreach-call.cil.c	timeout	920	1400	-	unknown	1.4	110	-	witness timeout	130	350	93	witness timeout	27	1400	92	witness timeout	5.9	360	92	witness timeout	47	290	92	witness timeout	150	3200	93	unknown	5.9	240	-	unknown	5.5	240	-
email_spec9_product15_false-unreach-call.cil.c	timeout	920	550	-	unknown	1.3	99	-	witness confirmed	1.3	44	25	witness confirmed	20	840	39	witness confirmed	0.55	68	25	witness confirmed	1.4	45	24	witness confirmed	7.5	340	24	unknown	5.4	240	-	unknown	5.4	240	-
email_spec9_product16_false-unreach-call.cil.c	timeout	920	710	-	unknown	1.3	96	-	witness confirmed	1.3	45	31	witness confirmed	21	900	52	witness confirmed	0.93	84	32	witness confirmed	1.2	46	24	witness confirmed	7.8	340	32	unknown	5.3	240	-	unknown	5.4	240	-
email_spec9_product20_false-unreach-call.cil.c	timeout	920	660	-	unknown	1.5	110	-	witness confirmed	2.1	49	32	witness confirmed	19	870	42	witness confirmed	0.82	79	32	witness confirmed	2.5	63	33	witness confirmed	10	530	31	unknown	5.5	240	-	unknown	5.4	240	-
email_spec9_product21_false-unreach-call.cil.c	timeout	920	530	-	unknown	1.5	110	-	true	2.1	49	-	witness confirmed	19	1000	60	witness confirmed	1.3	110	34	witness confirmed	3.5	68	34	witness confirmed	11	480	33	unknown	5.5	240	-	unknown	5.5	240	-
email_spec9_product22_false-unreach-call.cil.c	timeout	920	540	-	unknown	1.5	110	-	witness confirmed	1.4	44	31	witness confirmed	19	840	25	witness confirmed	1.1	100	31	witness confirmed	2.0	51	24	witness confirmed	8.1	360	32	unknown	5.3	240	-	unknown	5.8	240	-
email_spec9_product26_false-unreach-call.cil.c	timeout	920	660	-	unknown	1.3	98	-	witness confirmed	2.5	50	33	witness confirmed	17	950	48	witness confirmed	1.5	120	33	witness confirmed	3.2	74	33	witness confirmed	12	550	32	unknown	5.8	240	-	unknown	5.9	240	-
email_spec9_product30_false-unreach-call.cil.c	timeout	920	630	-	unknown	1.4	110	-	true	1.3	45	-	witness confirmed	19	850	54	witness confirmed	0.57	72	36	witness confirmed	1.5	48	35	witness confirmed	8.1	350	34	unknown	5.2	240	-	unknown	5.2	240	-
email_spec9_product31_false-unreach-call.cil.c	timeout	920	500	-	unknown	1.4	100	-	witness confirmed	1.5	46	37	witness timeout	22	1000	95	witness confirmed	1.5	110	37	witness confirmed	1.8	50	38	witness confirmed	9.0	420	36	unknown	5.5	240	-	unknown	5.5	240	-
email_spec9_product32_false-unreach-call.cil.c	timeout	920	920	-	unknown	1.5	110	-	witness confirmed	2.7	51	38	witness confirmed	19	980	57	witness confirmed	0.89	87	36	witness confirmed	3.7	75	38	witness confirmed	12	500	37	unknown	5.3	240	-	unknown	6.3	240	-
email_spec9_product33_false-unreach-call.cil.c	timeout	920	650	-	unknown	1.4	110	-	witness confirmed	1.6	45	36	witness confirmed	22	900	58	witness confirmed	1.7	110	37	witness confirmed	2.0	54	37	witness confirmed	9.4	410	36	unknown	5.4	240	-	unknown	5.7	240	-
email_spec9_product34_false-unreach-call.cil.c	timeout	920	900	-	unknown	1.5	100	-	witness confirmed	3.0	54	40	witness timeout	22	1100	110	witness confirmed	1.7	130	40	witness confirmed	4.2	81	41	witness confirmed	13	590	40	unknown	5.4	240	-	unknown	5.8	240	-
email_spec9_product35_false-unreach-call.cil.c	timeout	920	810	-	unknown	1.5	110	-	witness confirmed	3.5	56	38	witness confirmed	16	970	61	witness confirmed	1.9	130	38	witness confirmed	4.4	84	39	witness confirmed	14	560	39	unknown	5.4	240	-	unknown	5.8	240	-
email_spec9_productSimulator_false-unreach-call.cil.c	timeout	920	1400	-	unknown	1.5	110	-	witness timeout	130	350	92	witness timeout	29	1400	92	witness timeout	5.9	360	93	witness timeout	51	290	93	witness timeout	150	3200	92	unknown	5.4	240	-	unknown	5.6	250	-
email_spec0_product05_true-unreach-call.cil.c	true	0.40	34	-	unknown	1.4	96	-	true	2.4	35	-	true	23	460	-	true	0.18	34	-	true	0.45	30	-	true	4.0	130	-	unknown	5.8	240	-	unknown	5.7	240	-
email_spec0_product09_true-unreach-call.cil.c	true	0.66	49	-	unknown	1.4	99	-	true	3.5	35	-	true	18	530	-	true	0.22	34	-	true	0.81	33	-	true	7.4	250	-	unknown	5.8	240	-	unknown	5.5	240	-
email_spec0_product10_true-unreach-call.cil.c	true	0.52	39	-	unknown	1.2	96	-	true	2.5	35	-	true	21	470	-	true	0.19	34	-	true	0.51	31	-	true	4.6	140	-	unknown	5.4	240	-	unknown	5.7	240	-
email_spec0_product11_true-unreach-call.cil.c	true	0.73	52	-	unknown	1.3	98	-	true	3.2	36	-	true	16	800	-	true	0.25	35	-	true	0.63	31	-	true	13	440	-	unknown	5.6	240	-	unknown	5.3	240	-
email_spec0_product19_true-unreach-call.cil.c	true	1.00	66	-	unknown	1.4	110	-	true	3.7	36	-	true	17	920	-	true	0.27	37	-	true	0.83	32	-	true	16	510	-	unknown	5.9	240	-	unknown	5.8	240	-
email_spec0_product24_true-unreach-call.cil.c	true	1.2	75	-	unknown	1.4	99	-	true	3.8	37	-	true	17	930	-	true	0.27	37	-	true	1.0	34	-	true	16	490	-	unknown	5.5	240	-	unknown	5.5	240	-
email_spec0_product25_true-unreach-call.cil.c	true	1.8	110	-	unknown	1.4	110	-	true	6.2	38	-	true	16	930	-	true	0.35	41	-	true	1.5	40	-	true	25	680	-	unknown	5.5	240	-	unknown	5.4	240	-
email_spec0_product27_true-unreach-call.cil.c	true	2.3	140	-	unknown	1.4	98	-	true	6.7	38	-	true	28	1600	-	true	0.37	42	-	true	1.7	42	-	true	26	700	-	unknown	5.8	240	-	unknown	5.6	240	-
email_spec0_product36_true-unreach-call.cil.c	true	0.89	62	-	unknown	1.3	94	-	true	4.0	36	-	true	18	550	-	true	0.27	36	-	true	1.0	36	-	true	8.7	270	-	unknown	5.7	240	-	unknown	5.5	240	-
email_spec0_product37_true-unreach-call.cil.c	true	1.0	67	-	unknown	1.4	100	-	true	3.3	36	-	true	16	800	-	true	0.26	36	-	true	0.69	32	-	true	14	470	-	unknown	5.4	240	-	unknown	5.4	240	-
email_spec0_product38_true-unreach-call.cil.c	true	1.1	70	-	unknown	1.3	98	-	true	4.5	36	-	true	15	790	-	true	0.30	40	-	true	0.94	34	-	true	19	620	-	unknown	5.8	240	-	unknown	5.4	240	-
email_spec0_product40_true-unreach-call.cil.c	true	1.7	110	-	unknown	1.4	110	-	true	4.9	36	-	true	16	920	-	true	0.32	39	-	true	1.1	36	-	true	21	620	-	unknown	5.3	240	-	unknown	5.4	240	-
email_spec11_product03_true-unreach-call.cil.c	true	0.37	30	-	unknown	1.3	98	-	true	2.2	35	-	true	22	340	-	true	0.16	34	-	true	0.44	30	-	true	4.0	140	-	unknown	5.5	240	-	unknown	5.6	240	-
email_spec11_product07_true-unreach-call.cil.c	true	0.58	44	-	unknown	1.3	100	-	true	3.3	35	-	true	17	460	-	true	0.24	34	-	true	0.72	32	-	true	7.0	240	-	unknown	5.3	240	-	unknown	5.4	240	-
email_spec11_product08_true-unreach-call.cil.c	true	0.83	54	-	unknown	1.4	100	-	true	3.1	36	-	true	15	780	-	true	0.24	35	-	true	0.69	30	-	true	14	400	-	unknown	5.2	240	-	unknown	5.3	240	-
email_spec11_product10_true-unreach-call.cil.c	true	0.47	37	-	unknown	1.3	100	-	true	2.6	35	-	true	21	470	-	true	0.19	34	-	true	0.53	31	-	true	4.6	140	-	unknown	5.7	240	-	unknown	5.6	240	-
email_spec11_product18_true-unreach-call.cil.c	true	1.0	65	-	unknown	1.4	110	-	true	3.5	36	-	true	17	910	-	true	0.24	37	-	true	0.77	32	-	true	15	450	-	unknown	5.4	240	-	unknown	5.9	240	-
email_spec11_product23_true-unreach-call.cil.c	true	1.7	110	-	unknown	1.2	98	-	true	5.5	38	-	true	16	930	-	true	0.34	40	-	true	1.4	38	-	true	23	680	-	unknown	5.7	240	-	unknown	5.5	240	-
email_spec11_product24_true-unreach-call.cil.c	true	1.2	76	-	unknown	1.1	95	-	true	3.8	37	-	true	17	940	-	true	0.28	38	-	true	0.93	34	-	true	19	500	-	unknown	5.6	240	-	unknown	5.7	240	-
email_spec11_product27_true-unreach-call.cil.c	true	2.3	140	-	unknown	1.5	110	-	true	6.7	37	-	true	18	1100	-	true	0.38	42	-	true	1.8	42	-	true	35	670	-	unknown	5.6	240	-	unknown	5.6	240	-
email_spec11_product36_true-unreach-call.cil.c	true	0.82	58	-	unknown	1.3	96	-	true	4.0	35	-	true	17	550	-	true	0.25	35	-	true	1.1	36	-	true	8.8	270	-	unknown	5.5	240	-	unknown	5.6	240	-
email_spec11_product37_true-unreach-call.cil.c	true	0.99	66	-	unknown	1.4	100	-	true	3.2	37	-	true	16	790	-	true	0.26	36	-	true	0.69	31	-	true	15	460	-	unknown	5.5	240	-	unknown	5.8	240	-
email_spec11_product39_true-unreach-call.cil.c	true	1.2	76	-	unknown	1.3	98	-	true	4.2	36	-	true	15	790	-	true	0.28	37	-	true	0.93	33	-	true	19	510	-	unknown	5.5	240	-	unknown	5.5	240	-
email_spec11_product40_true-unreach-call.cil.c	true	1.7	100	-	unknown	1.4	99	-	true	5.0	36	-	true	15	840	-	true	0.33	39	-	true	1.1	36	-	true	21	630	-	unknown	5.6	240	-	unknown	5.5	240	-
email_spec1_product12_true-unreach-call.cil.c	true	0.73	50	-	unknown	1.3	110	-	true	2.8	36	-	true	15	800	-	true	0.24	36	-	true	0.60	30	-	true	15	450	-	unknown	5.8	240	-	unknown	5.6	240	-
email_spec1_product28_true-unreach-call.cil.c	true	0.89	58	-	unknown	1.4	100	-	true	3.1	37	-	true	17	920	-	true	0.26	37	-	true	0.72	30	-	true	16	460	-	unknown	5.3	240	-	unknown	5.8	240	-
email_spec27_product13_true-unreach-call.cil.c	false(reach)	59	140	-	unknown	1.2	97	-	true	3.2	44	-	true	16	790	-	true	0.26	42	-	true	0.65	30	-	true	15	470	-	unknown	5.4	240	-	unknown	5.8	240	-
email_spec27_product28_true-unreach-call.cil.c	false(reach)	120	290	-	unknown	1.3	100	-	true	3.4	44	-	true	17	920	-	true	0.27	43	-	true	0.82	35	-	true	16	470	-	unknown	6.5	240	-	unknown	5.3	240	-
email_spec4_product13_true-unreach-call.cil.c	true	20	120	-	unknown	1.3	98	-	true	3.2	43	-	true	16	790	-	true	0.27	41	-	true	0.62	30	-	true	14	450	-	unknown	5.4	240	-	unknown	5.5	240	-
email_spec4_product17_true-unreach-call.cil.c	true	110	170	-	unknown	1.5	110	-	true	4.0	45	-	true	16	920	-	true	0.28	45	-	true	1.0	31	-	true	22	650	-	unknown	5.7	240	-	unknown	5.5	240	-
email_spec4_product28_true-unreach-call.cil.c	true	140	140	-	unknown	1.4	110	-	true	3.3	44	-	true	16	840	-	true	0.26	42	-	true	0.72	30	-	true	15	460	-	unknown	5.7	240	-	unknown	5.6	240	-
email_spec4_product29_true-unreach-call.cil.c	true	660	380	-	unknown	1.3	98	-	true	4.5	45	-	true	16	930	-	true	0.33	48	-	true	1.2	33	-	true	24	720	-	unknown	5.4	240	-	unknown	5.9	240	-
email_spec7_product13_true-unreach-call.cil.c	true	0.75	50	-	unknown	1.3	98	-	true	2.8	36	-	true	16	790	-	true	0.24	36	-	true	0.63	30	-	true	14	440	-	unknown	5.8	240	-	unknown	5.6	240	-
email_spec7_product17_true-unreach-call.cil.c	true	0.91	61	-	unknown	1.3	98	-	true	3.6	36	-	true	16	910	-	true	0.26	37	-	true	0.87	31	-	true	20	630	-	unknown	5.5	240	-	unknown	5.6	240	-
email_spec7_product18_true-unreach-call.cil.c	true	0.98	66	-	unknown	1.3	98	-	true	3.5	37	-	true	17	920	-	true	0.26	36	-	true	0.77	32	-	true	14	440	-	unknown	5.5	240	-	unknown	5.5	240	-
email_spec7_product19_true-unreach-call.cil.c	true	0.98	66	-	unknown	1.3	98	-	true	3.6	37	-	true	17	930	-	true	0.26	37	-	true	0.91	32	-	true	16	520	-	unknown	5.4	240	-	unknown	5.5	240	-
email_spec7_product23_true-unreach-call.cil.c	true	1.7	110	-	unknown	1.4	110	-	true	5.4	38	-	true	16	930	-	true	0.31	40	-	true	1.3	38	-	true	23	690	-	unknown	5.8	240	-	unknown	5.5	240	-
email_spec7_product24_true-unreach-call.cil.c	true	1.2	75	-	unknown	1.4	100	-	true	3.9	37	-	true	18	930	-	true	0.27	37	-	true	0.96	34	-	true	17	530	-	unknown	5.5	240	-	unknown	5.8	240	-
email_spec7_product25_true-unreach-call.cil.c	true	1.8	110	-	unknown	1.4	110	-	true	6.1	37	-	true	16	930	-	true	0.36	41	-	true	1.5	39	-	true	23	680	-	unknown	5.8	240	-	unknown	5.5	240	-
email_spec7_product27_true-unreach-call.cil.c	true	2.3	140	-	unknown	1.5	110	-	true	6.6	38	-	true	18	1200	-	true	0.38	42	-	true	1.7	42	-	true	26	670	-	unknown	5.5	240	-	unknown	5.8	240	-
email_spec8_product12_true-unreach-call.cil.c	true	0.74	52	-	unknown	1.1	98	-	true	2.9	37	-	true	16	790	-	true	0.23	36	-	true	0.61	30	-	true	14	440	-	unknown	5.5	240	-	unknown	5.7	240	-
email_spec8_product14_true-unreach-call.cil.c	timeout	920	910	-	unknown	1.3	100	-	true	4.2	46	-	true	16	910	-	true	0.37	70	-	true	1.1	38	-	true	22	610	-	unknown	5.5	240	-	unknown	5.8	240	-
email_spec8_product28_true-unreach-call.cil.c	true	0.90	60	-	unknown	1.4	99	-	true	3.1	37	-	true	18	840	-	true	0.25	37	-	true	0.73	31	-	true	16	510	-	unknown	5.5	240	-	unknown	5.8	240	-
email_spec8_product29_true-unreach-call.cil.c	timeout	920	780	-	unknown	1.3	100	-	true	4.8	46	-	true	17	930	-	true	0.39	72	-	true	1.7	41	-	true	24	720	-	unknown	5.7	240	-	unknown	5.5	240	-
email_spec9_product12_true-unreach-call.cil.c	true	0.75	52	-	unknown	1.3	100	-	true	2.9	36	-	true	16	790	-	true	0.25	36	-	true	0.60	30	-	true	14	440	-	unknown	5.9	240	-	unknown	5.4	240	-
email_spec9_product14_true-unreach-call.cil.c	timeout	920	910	-	unknown	1.4	100	-	true	4.1	46	-	true	16	910	-	true	0.38	70	-	true	1.1	38	-	true	23	610	-	unknown	5.4	240	-	unknown	5.9	240	-
email_spec9_product28_true-unreach-call.cil.c	true	0.91	58	-	unknown	1.4	110	-	true	3.1	37	-	true	17	920	-	true	0.27	37	-	true	0.82	31	-	true	15	510	-	unknown	5.7	240	-	unknown	5.6	240	-
email_spec9_product29_true-unreach-call.cil.c	timeout	920	780	-	unknown	1.3	99	-	true	4.8	46	-	true	17	920	-	true	0.40	72	-	true	1.7	41	-	true	24	720	-	unknown	5.5	240	-	unknown	5.7	240	-
minepump_spec1_product33_false-unreach-call.cil.c	witness confirmed	0.98	18	2.4	unknown	0.94	80	-	unknown	0.12	27	-	witness confirmed	2.3	200	2.5	witness confirmed	0.12	21	3.2	witness confirmed	0.28	33	2.4	witness confirmed	1.8	110	2.5	witness confirmed	8.7	290	2.7	witness confirmed	15	670	2.6
minepump_spec1_product34_false-unreach-call.cil.c	witness confirmed	1.0	18	2.5	unknown	0.96	81	-	witness confirmed	0.17	29	2.5	witness confirmed	2.4	210	2.5	witness confirmed	0.15	21	3.1	witness confirmed	0.29	33	2.4	witness confirmed	1.9	120	2.5	witness confirmed	10	290	2.7	witness confirmed	21	1200	3.1
minepump_spec1_product35_false-unreach-call.cil.c	witness confirmed	1.2	18	2.7	unknown	0.85	80	-	witness confirmed	0.18	28	2.5	witness confirmed	2.3	210	2.7	witness confirmed	0.14	21	3.1	witness confirmed	0.42	34	2.4	witness confirmed	1.9	110	2.6	witness confirmed	8.9	270	2.8	witness confirmed	31	1200	2.7
minepump_spec1_product36_false-unreach-call.cil.c	witness confirmed	1.3	20	2.8	unknown	0.86	79	-	witness confirmed	0.17	28	2.6	witness confirmed	2.4	200	2.8	witness confirmed	0.14	21	3.0	witness confirmed	0.31	34	2.4	witness confirmed	1.9	110	2.5	witness confirmed	8.8	280	2.8	witness confirmed	61	1200	2.8
minepump_spec1_product37_false-unreach-call.cil.c	witness confirmed	1.0	17	2.5	unknown	0.94	80	-	unknown	0.15	30	-	witness confirmed	2.4	210	2.5	witness confirmed	0.14	22	2.9	witness confirmed	0.39	33	2.4	witness confirmed	2.2	150	2.5	witness confirmed	9.1	300	2.7	witness confirmed	23	1200	2.7
minepump_spec1_product38_false-unreach-call.cil.c	witness confirmed	0.96	18	2.9	unknown	0.96	81	-	witness confirmed	0.15	28	2.6	witness confirmed	2.4	210	2.6	witness confirmed	0.17	23	2.9	witness confirmed	0.29	33	2.4	witness confirmed	2.2	150	2.6	witness confirmed	11	310	2.8	witness confirmed	41	1200	2.7
minepump_spec1_product39_false-unreach-call.cil.c	witness confirmed	1.3	19	3.0	unknown	0.95	80	-	witness confirmed	0.17	28	2.6	witness confirmed	2.4	200	2.8	witness confirmed	0.17	24	3.0	witness confirmed	0.29	34	2.5	witness confirmed	2.2	130	2.7	witness confirmed	12	330	2.7	witness confirmed	58	1200	2.8
minepump_spec1_product40_false-unreach-call.cil.c	witness confirmed	1.3	19	2.9	unknown	1.00	79	-	witness confirmed	0.19	28	2.6	witness confirmed	2.4	210	2.9	witness confirmed	0.14	24	3.4	witness confirmed	0.34	34	2.6	witness confirmed	2.3	130	2.8	witness confirmed	12	340	2.8	witness confirmed	68	1200	2.8
minepump_spec1_product41_false-unreach-call.cil.c	witness confirmed	11	26	3.2	unknown	0.96	80	-	witness confirmed	0.15	28	3.1	witness confirmed	3.0	210	3.2	witness confirmed	0.14	21	3.7	witness confirmed	0.44	37	3.0	witness confirmed	2.1	110	3.2	witness confirmed	9.6	290	3.4	timeout	920	1200	-
minepump_spec1_product42_false-unreach-call.cil.c	witness confirmed	11	28	3.4	unknown	0.84	79	-	witness confirmed	0.15	28	3.5	witness confirmed	3.0	210	3.5	witness confirmed	0.13	22	4.0	witness confirmed	0.41	36	3.1	witness confirmed	2.1	110	3.3	witness confirmed	11	400	3.3	timeout	920	1200	-
minepump_spec1_product43_false-unreach-call.cil.c	witness confirmed	23	35	3.2	unknown	0.97	80	-	unknown	0.14	28	-	witness confirmed	3.0	210	3.3	witness confirmed	0.12	21	3.4	witness confirmed	0.35	39	2.9	witness confirmed	2.1	120	3.3	witness confirmed	13	410	3.2	timeout	920	1600	-
minepump_spec1_product44_false-unreach-call.cil.c	witness confirmed	24	38	3.6	unknown	0.97	80	-	witness confirmed	0.16	28	3.1	witness confirmed	3.0	210	3.4	witness confirmed	0.15	22	3.5	witness confirmed	0.35	38	3.0	witness confirmed	2.2	120	3.3	witness confirmed	13	410	3.2	timeout	920	1200	-
minepump_spec1_product49_false-unreach-call.cil.c	witness confirmed	1.0	17	2.7	unknown	0.97	81	-	unknown	0.17	28	-	witness confirmed	2.4	200	2.6	witness confirmed	0.16	23	3.0	witness confirmed	0.30	34	2.4	witness confirmed	2.3	130	2.5	witness confirmed	9.4	290	2.7	witness confirmed	33	1200	2.7
minepump_spec1_product50_false-unreach-call.cil.c	witness confirmed	1.0	19	2.7	unknown	0.90	81	-	witness confirmed	0.17	28	2.6	witness confirmed	2.4	200	2.6	witness confirmed	0.15	24	3.0	witness confirmed	0.33	35	2.4	witness confirmed	2.3	130	2.6	witness confirmed	9.9	310	2.8	witness confirmed	28	1200	2.8
minepump_spec1_product51_false-unreach-call.cil.c	witness confirmed	1.1	18	2.8	unknown	0.98	83	-	unknown	0.16	29	-	witness confirmed	2.4	200	2.9	witness confirmed	0.17	24	2.9	witness confirmed	0.40	34	2.5	witness confirmed	2.2	140	2.7	witness confirmed	9.4	270	2.8	witness confirmed	66	1200	2.8
minepump_spec1_product52_false-unreach-call.cil.c	witness confirmed	1.3	19	2.8	unknown	0.99	78	-	witness confirmed	0.15	29	2.7	witness confirmed	2.4	210	2.9	witness confirmed	0.16	25	3.1	witness confirmed	0.36	34	2.6	witness confirmed	2.4	130	2.8	witness confirmed	9.3	280	2.9	witness confirmed	58	1200	2.8
minepump_spec1_product53_false-unreach-call.cil.c	witness confirmed	1.0	18	2.6	unknown	0.95	81	-	unknown	0.18	29	-	witness confirmed	2.4	200	2.6	witness confirmed	0.20	29	3.0	witness confirmed	0.33	33	2.5	witness confirmed	3.1	190	2.5	witness confirmed	9.5	290	2.8	witness confirmed	39	1200	2.8
minepump_spec1_product54_false-unreach-call.cil.c	witness confirmed	1.1	18	2.7	unknown	0.90	79	-	witness confirmed	0.17	29	2.7	witness confirmed	2.4	210	2.9	witness confirmed	0.20	30	3.0	witness confirmed	0.34	33	2.6	witness confirmed	3.3	190	2.7	witness confirmed	9.4	290	2.8	witness confirmed	56	1200	2.8
minepump_spec1_product55_false-unreach-call.cil.c	witness confirmed	1.3	18	2.8	unknown	0.99	80	-	witness confirmed	0.22	30	2.7	witness confirmed	2.4	210	2.9	witness confirmed	0.21	31	3.0	witness confirmed	0.34	34	2.6	witness confirmed	3.3	190	2.7	witness confirmed	9.2	300	2.8	witness confirmed	110	1200	2.8
minepump_spec1_product56_false-unreach-call.cil.c	witness confirmed	1.2	21	3.0	unknown	0.98	82	-	witness confirmed	0.21	30	2.8	witness confirmed	2.4	210	3.0	witness confirmed	0.22	31	3.1	witness confirmed	0.36	34	2.7	witness confirmed	3.0	190	2.8	witness confirmed	9.6	300	3.0	witness confirmed	240	1200	3.0
minepump_spec1_productSimulator_false-unreach-call.cil.c	witness confirmed	2.0	27	5.0	unknown	1.0	80	-	witness confirmed	0.36	36	4.3	witness confirmed	2.8	210	4.7	witness confirmed	0.43	53	4.6	witness confirmed	0.67	39	4.2	witness confirmed	10	480	4.4	witness confirmed	11	330	3.1	timeout	920	1600	-
minepump_spec2_product33_false-unreach-call.cil.c	witness confirmed	9.1	28	3.2	unknown	0.99	80	-	witness confirmed	0.13	27	3.2	witness confirmed	2.8	210	3.3	witness confirmed	0.12	21	4.0	witness confirmed	0.29	39	3.1	witness confirmed	2.5	110	3.6	witness confirmed	11	350	3.5	timeout	920	1200	-
minepump_spec2_product34_false-unreach-call.cil.c	witness confirmed	9.5	31	3.4	unknown	0.97	81	-	witness confirmed	0.16	27	3.4	witness confirmed	2.8	210	3.6	witness confirmed	0.13	21	4.2	witness confirmed	0.31	38	3.2	witness confirmed	2.5	110	4.2	witness confirmed	10	300	3.5	timeout	920	1200	-
minepump_spec2_product35_false-unreach-call.cil.c	witness confirmed	26	39	3.3	unknown	0.88	79	-	witness confirmed	0.18	28	3.2	witness confirmed	2.7	210	3.4	witness confirmed	0.12	21	3.4	witness confirmed	0.32	38	3.5	witness confirmed	2.6	110	3.5	witness confirmed	10	300	3.5	timeout	920	1200	-
minepump_spec2_product36_false-unreach-call.cil.c	witness confirmed	25	43	3.6	unknown	0.97	80	-	witness confirmed	0.17	28	3.3	witness confirmed	2.8	210	4.1	witness confirmed	0.15	21	3.6	witness confirmed	0.35	38	3.2	witness confirmed	2.5	110	4.1	witness confirmed	11	310	3.4	timeout	920	1200	-
minepump_spec2_product41_false-unreach-call.cil.c	witness confirmed	28	40	3.7	unknown	0.95	78	-	witness confirmed	0.31	29	3.5	witness confirmed	3.8	220	3.8	witness confirmed	0.15	21	3.8	witness confirmed	0.43	41	3.3	witness confirmed	2.6	120	3.7	witness confirmed	14	420	3.6	timeout	920	1200	-
minepump_spec2_product42_false-unreach-call.cil.c	witness confirmed	29	51	5.4	unknown	0.95	79	-	witness confirmed	0.33	31	3.5	witness confirmed	3.8	210	4.3	witness confirmed	0.16	22	3.9	witness confirmed	0.34	41	3.5	witness confirmed	2.6	120	4.2	witness confirmed	15	420	3.8	timeout	920	1200	-
minepump_spec2_product43_false-unreach-call.cil.c	witness confirmed	85	71	3.7	unknown	0.97	80	-	witness confirmed	0.31	30	3.4	witness confirmed	3.5	210	3.8	witness confirmed	0.14	22	3.9	witness confirmed	0.41	43	3.2	witness confirmed	2.7	110	4.1	witness confirmed	16	430	3.5	timeout	920	1200	-
minepump_spec2_product44_false-unreach-call.cil.c	witness confirmed	74	63	4.7	unknown	0.86	79	-	witness confirmed	0.34	32	3.5	witness confirmed	4.1	220	4.4	witness confirmed	0.13	22	3.7	witness confirmed	0.39	42	3.3	witness confirmed	2.7	120	3.8	witness confirmed	17	680	3.7	timeout	920	1200	-
minepump_spec2_productSimulator_false-unreach-call.cil.c	witness confirmed	640	230	8.7	unknown	1.0	83	-	unknown	0.35	35	-	witness confirmed	5.5	260	8.3	witness confirmed	0.40	52	7.1	witness confirmed	0.90	42	6.4	witness confirmed	17	500	7.7	witness confirmed	17	460	4.0	timeout	920	1600	-
minepump_spec3_product01_false-unreach-call.cil.c	witness confirmed	0.095	17	2.1	unknown	0.97	81	-	unknown	0.13	27	-	witness confirmed	2.3	210	2.2	witness confirmed	0.10	19	2.6	witness confirmed	0.23	34	2.0	witness confirmed	1.7	97	2.2	witness confirmed	6.8	270	2.3	witness confirmed	10	300	2.1
minepump_spec3_product02_false-unreach-call.cil.c	witness confirmed	0.11	18	2.1	unknown	0.95	78	-	witness confirmed	0.17	27	2.2	witness confirmed	2.3	200	2.2	witness confirmed	0.13	19	2.6	witness confirmed	0.23	34	2.1	witness confirmed	1.7	95	2.4	witness confirmed	6.9	270	2.3	witness confirmed	9.0	300	2.2
minepump_spec3_product03_false-unreach-call.cil.c	witness confirmed	0.078	15	2.1	unknown	0.96	80	-	witness confirmed	0.16	27	2.2	witness confirmed	2.2	200	2.1	witness confirmed	0.13	19	3.0	witness confirmed	0.26	34	2.1	witness confirmed	1.7	95	2.3	witness confirmed	7.0	270	2.2	witness confirmed	9.0	300	2.1
minepump_spec3_product04_false-unreach-call.cil.c	witness confirmed	1.3	17	2.2	unknown	0.95	81	-	unknown	0.12	27	-	witness confirmed	2.3	200	2.2	witness confirmed	0.12	19	2.7	witness confirmed	0.25	34	2.1	witness confirmed	1.7	96	2.3	witness confirmed	7.0	270	2.3	witness confirmed	13	420	2.2
minepump_spec3_product05_false-unreach-call.cil.c	witness confirmed	0.10	17	2.2	unknown	0.98	82	-	witness confirmed	0.16	27	2.2	witness confirmed	2.3	200	2.2	witness confirmed	0.12	19	2.6	witness confirmed	0.24	36	2.1	witness confirmed	1.8	110	2.3	witness confirmed	6.9	270	2.4	witness confirmed	8.7	280	2.3
minepump_spec3_product06_false-unreach-call.cil.c	witness confirmed	0.11	14	2.2	unknown	1.00	80	-	witness confirmed	0.13	27	2.7	witness confirmed	2.2	210	2.3	witness confirmed	0.12	19	2.7	witness confirmed	0.25	33	2.1	witness confirmed	1.9	100	2.3	witness confirmed	7.1	270	2.4	witness confirmed	10	400	2.2
minepump_spec3_product07_false-unreach-call.cil.c	witness confirmed	1.2	17	2.2	unknown	0.98	79	-	witness confirmed	0.13	27	2.3	witness confirmed	2.3	210	2.4	witness confirmed	0.11	19	2.7	witness confirmed	0.26	34	2.1	witness confirmed	1.9	110	2.2	witness confirmed	7.0	270	2.3	witness confirmed	8.9	300	2.4
minepump_spec3_product08_false-unreach-call.cil.c	witness confirmed	1.4	17	2.2	unknown	0.95	80	-	witness confirmed	0.15	27	2.3	witness confirmed	2.3	200	2.3	witness confirmed	0.13	19	2.7	witness confirmed	0.25	35	2.1	witness confirmed	1.9	110	2.3	witness confirmed	7.3	280	2.3	witness confirmed	9.1	290	2.3
minepump_spec3_product09_false-unreach-call.cil.c	witness confirmed	0.093	14	2.2	unknown	0.99	83	-	unknown	0.15	27	-	witness confirmed	2.2	210	2.2	witness confirmed	0.10	19	2.6	witness confirmed	0.25	34	2.4	witness confirmed	1.6	100	2.3	witness confirmed	6.9	270	2.2	witness confirmed	11	400	2.2
minepump_spec3_product10_false-unreach-call.cil.c	witness confirmed	0.089	18	2.2	unknown	0.95	81	-	witness confirmed	0.16	27	2.2	witness confirmed	2.3	210	2.2	witness confirmed	0.12	19	2.8	witness confirmed	0.24	34	2.2	witness confirmed	1.7	95	2.2	witness confirmed	7.2	270	2.5	witness confirmed	11	400	2.3
minepump_spec3_product11_false-unreach-call.cil.c	witness confirmed	0.097	17	2.2	unknown	0.98	81	-	witness confirmed	0.16	27	2.2	witness confirmed	2.2	210	2.2	witness confirmed	0.13	19	2.6	witness confirmed	0.34	34	2.1	witness confirmed	1.7	94	2.2	witness confirmed	8.4	270	2.3	witness confirmed	9.4	360	2.2
minepump_spec3_product12_false-unreach-call.cil.c	witness confirmed	1.3	17	2.2	unknown	1.00	80	-	unknown	0.15	27	-	witness confirmed	2.3	200	2.3	witness confirmed	0.12	19	2.7	witness confirmed	0.26	34	2.1	witness confirmed	1.8	97	2.3	witness confirmed	7.2	270	2.3	witness confirmed	12	420	2.2
minepump_spec3_product13_false-unreach-call.cil.c	witness confirmed	0.088	14	2.2	unknown	0.87	79	-	witness confirmed	0.16	27	2.3	witness confirmed	2.3	210	2.2	witness confirmed	0.10	19	2.7	witness confirmed	0.27	32	2.1	witness confirmed	1.9	100	2.3	witness confirmed	6.9	280	2.4	witness confirmed	9.3	270	2.3
minepump_spec3_product14_false-unreach-call.cil.c	witness confirmed	0.091	14	2.3	unknown	0.97	80	-	unknown	0.14	27	-	witness confirmed	2.3	200	2.3	witness confirmed	0.13	19	3.0	witness confirmed	0.25	34	2.2	witness confirmed	1.9	110	2.3	witness confirmed	7.4	270	2.4	witness confirmed	8.0	270	2.4
minepump_spec3_product15_false-unreach-call.cil.c	witness confirmed	1.3	19	2.2	unknown	0.88	80	-	witness confirmed	0.15	27	2.3	witness confirmed	2.3	210	2.5	witness confirmed	0.11	19	2.6	witness confirmed	0.26	34	2.3	witness confirmed	1.9	110	2.3	witness confirmed	7.3	270	2.4	witness confirmed	9.4	300	2.3
minepump_spec3_product16_false-unreach-call.cil.c	witness confirmed	1.3	18	2.2	unknown	0.97	84	-	unknown	0.15	27	-	witness confirmed	2.3	210	2.2	witness confirmed	0.12	19	2.7	witness confirmed	0.24	35	2.1	witness confirmed	2.0	110	2.3	witness confirmed	7.4	280	2.4	witness confirmed	11	400	2.2
minepump_spec3_product17_false-unreach-call.cil.c	witness confirmed	0.11	16	2.2	unknown	0.94	84	-	witness confirmed	0.15	27	2.3	witness confirmed	2.3	200	2.3	witness confirmed	0.11	19	2.7	witness confirmed	0.27	33	2.2	witness confirmed	1.8	110	2.6	witness confirmed	7.3	270	2.5	witness confirmed	13	470	2.3
minepump_spec3_product18_false-unreach-call.cil.c	witness confirmed	0.084	15	2.3	unknown	0.96	79	-	witness confirmed	0.16	27	2.3	witness confirmed	2.3	200	2.4	witness confirmed	0.12	19	2.9	witness confirmed	0.27	34	2.2	witness confirmed	1.9	130	2.4	witness confirmed	7.1	270	2.4	witness confirmed	8.3	270	2.5
minepump_spec3_product19_false-unreach-call.cil.c	witness confirmed	1.4	19	2.2	unknown	0.96	81	-	witness confirmed	0.17	27	2.3	witness confirmed	2.3	210	2.6	witness confirmed	0.13	19	2.8	witness confirmed	0.29	34	2.1	witness confirmed	1.9	110	2.3	witness confirmed	7.1	270	2.4	witness confirmed	8.1	270	2.3
minepump_spec3_product20_false-unreach-call.cil.c	witness confirmed	1.3	16	2.2	unknown	0.95	81	-	witness confirmed	0.16	27	2.3	witness confirmed	2.3	200	2.5	witness confirmed	0.13	19	2.6	witness confirmed	0.25	34	2.1	witness confirmed	2.0	110	2.3	witness confirmed	7.1	270	2.3	witness confirmed	9.0	300	2.2
minepump_spec3_product21_false-unreach-call.cil.c	witness confirmed	0.090	17	2.3	unknown	0.98	80	-	unknown	0.12	27	-	witness confirmed	2.3	200	2.4	witness confirmed	0.11	19	2.7	witness confirmed	0.26	34	2.2	witness confirmed	2.3	130	2.4	witness confirmed	7.3	270	2.4	witness confirmed	12	420	2.4
minepump_spec3_product22_false-unreach-call.cil.c	witness confirmed	0.11	15	2.4	unknown	1.00	80	-	witness confirmed	0.15	27	2.5	witness confirmed	2.3	210	2.7	witness confirmed	0.11	19	2.8	witness confirmed	0.25	34	2.3	witness confirmed	2.2	130	2.4	witness confirmed	7.3	280	2.5	witness confirmed	13	430	2.7
minepump_spec3_product23_false-unreach-call.cil.c	witness confirmed	1.4	17	2.2	unknown	0.86	82	-	witness confirmed	0.15	27	2.7	witness confirmed	2.3	200	2.3	witness confirmed	0.12	19	2.7	witness confirmed	0.38	34	2.1	witness confirmed	2.3	130	2.3	witness confirmed	7.4	270	2.4	witness confirmed	11	370	2.6
minepump_spec3_product24_false-unreach-call.cil.c	witness confirmed	1.3	17	2.3	unknown	0.97	79	-	unknown	0.16	27	-	witness confirmed	2.3	200	2.2	witness confirmed	0.13	20	2.7	witness confirmed	0.39	34	2.2	witness confirmed	2.3	130	2.3	witness confirmed	7.2	270	2.4	witness confirmed	11	400	2.2
minepump_spec3_product25_false-unreach-call.cil.c	witness confirmed	0.090	14	2.2	unknown	0.96	79	-	witness confirmed	0.15	27	2.3	witness confirmed	2.3	210	2.3	witness confirmed	0.12	19	2.6	witness confirmed	0.25	34	2.1	witness confirmed	1.8	100	2.2	witness confirmed	7.2	270	2.3	witness confirmed	9.7	310	2.6
minepump_spec3_product26_false-unreach-call.cil.c	witness confirmed	0.096	14	2.2	unknown	0.87	78	-	witness confirmed	0.17	27	2.3	witness confirmed	2.4	200	2.4	witness confirmed	0.12	19	2.7	witness confirmed	0.36	34	2.2	witness confirmed	2.0	110	2.3	witness confirmed	7.1	270	2.4	witness confirmed	9.6	340	2.3
minepump_spec3_product27_false-unreach-call.cil.c	witness confirmed	1.3	17	2.2	unknown	0.86	82	-	witness confirmed	0.16	27	2.4	witness confirmed	2.3	200	2.3	witness confirmed	0.13	19	2.7	witness confirmed	0.51	34	2.2	witness confirmed	2.0	110	2.3	witness confirmed	7.3	270	2.8	witness confirmed	9.0	290	2.4
minepump_spec3_product28_false-unreach-call.cil.c	witness confirmed	1.3	18	2.2	unknown	1.0	80	-	unknown	0.15	27	-	witness confirmed	2.3	210	2.3	witness confirmed	0.10	19	2.7	witness confirmed	0.40	34	2.1	witness confirmed	1.9	110	2.3	witness confirmed	7.3	270	2.3	witness confirmed	9.9	310	2.4
minepump_spec3_product29_false-unreach-call.cil.c	witness confirmed	0.087	14	2.4	unknown	0.97	80	-	witness confirmed	0.15	28	2.3	witness confirmed	2.4	210	2.3	witness confirmed	0.12	19	2.8	witness confirmed	0.39	34	2.2	witness confirmed	2.1	130	2.3	witness confirmed	7.3	270	2.6	witness confirmed	14	670	2.4
minepump_spec3_product30_false-unreach-call.cil.c	witness confirmed	0.11	15	2.4	unknown	0.97	81	-	witness confirmed	0.16	27	2.5	witness confirmed	2.3	210	2.6	witness confirmed	0.13	19	2.8	witness confirmed	0.28	34	2.3	witness confirmed	2.3	130	2.6	witness confirmed	7.5	270	2.6	witness confirmed	14	600	2.4
minepump_spec3_product31_false-unreach-call.cil.c	witness confirmed	1.3	17	2.2	unknown	0.96	80	-	witness confirmed	0.17	28	2.3	witness confirmed	2.4	200	2.3	witness confirmed	0.11	19	3.1	witness confirmed	0.28	35	2.1	witness confirmed	2.4	130	2.3	witness confirmed	7.6	270	2.4	witness confirmed	11	410	2.2
minepump_spec3_product32_false-unreach-call.cil.c	witness confirmed	1.4	17	2.3	unknown	0.95	81	-	unknown	0.13	27	-	witness confirmed	2.4	210	2.3	witness confirmed	0.13	19	2.6	witness confirmed	0.27	34	2.2	witness confirmed	2.3	140	2.3	witness confirmed	7.1	280	2.3	witness confirmed	11	400	2.2
minepump_spec3_product35_false-unreach-call.cil.c	witness confirmed	1.5	19	2.2	unknown	0.98	79	-	witness confirmed	0.18	30	2.3	witness confirmed	2.4	200	2.4	witness confirmed	0.13	21	2.5	witness confirmed	0.29	34	2.1	witness confirmed	2.4	110	2.7	witness confirmed	8.6	270	2.3	witness confirmed	12	420	2.2
minepump_spec3_product36_false-unreach-call.cil.c	witness confirmed	1.6	18	2.2	unknown	0.96	80	-	unknown	0.16	28	-	witness confirmed	2.4	210	2.2	witness confirmed	0.15	21	2.6	witness confirmed	0.31	34	2.5	witness confirmed	2.5	140	2.8	witness confirmed	7.4	270	2.3	witness confirmed	9.2	300	2.6
minepump_spec3_product39_false-unreach-call.cil.c	witness confirmed	1.5	20	2.2	unknown	0.99	78	-	witness confirmed	0.18	29	2.3	witness confirmed	2.4	210	2.3	witness confirmed	0.14	24	2.6	witness confirmed	0.31	34	2.1	witness confirmed	3.0	140	2.8	witness confirmed	7.4	280	2.4	witness confirmed	11	410	2.5
minepump_spec3_product40_false-unreach-call.cil.c	witness confirmed	1.5	18	2.2	unknown	0.99	79	-	witness confirmed	0.16	31	2.3	witness confirmed	2.4	200	2.4	witness confirmed	0.15	24	2.6	witness confirmed	0.32	34	2.5	witness confirmed	2.9	130	2.7	witness confirmed	7.4	280	2.4	witness confirmed	11	300	2.2
minepump_spec3_product43_false-unreach-call.cil.c	witness confirmed	1.6	18	2.2	unknown	0.96	81	-	witness confirmed	0.18	28	2.3	witness confirmed	2.4	200	2.3	witness confirmed	0.16	22	2.6	witness confirmed	0.33	34	2.2	witness confirmed	2.6	110	2.7	witness confirmed	7.6	270	2.4	witness confirmed	13	420	2.2
minepump_spec3_product44_false-unreach-call.cil.c	witness confirmed	1.5	17	2.2	unknown	0.98	80	-	witness confirmed	0.17	28	2.3	witness confirmed	2.4	210	2.3	witness confirmed	0.15	22	2.8	witness confirmed	0.41	34	2.2	witness confirmed	2.6	130	2.7	witness confirmed	7.5	270	2.4	witness confirmed	9.8	310	2.3
minepump_spec3_product47_false-unreach-call.cil.c	witness confirmed	1.5	17	2.2	unknown	0.96	80	-	unknown	0.17	29	-	witness confirmed	2.4	210	2.3	witness confirmed	0.16	25	2.6	witness confirmed	0.33	34	2.1	witness confirmed	3.1	160	2.8	witness confirmed	7.7	280	2.4	witness confirmed	11	400	2.2
minepump_spec3_product48_false-unreach-call.cil.c	witness confirmed	1.5	18	2.2	unknown	0.88	79	-	witness confirmed	0.19	29	2.6	witness confirmed	2.4	200	2.3	witness confirmed	0.17	26	2.8	witness confirmed	0.34	34	2.2	witness confirmed	3.3	150	2.9	witness confirmed	7.4	270	2.4	witness confirmed	11	400	2.3
minepump_spec3_product51_false-unreach-call.cil.c	witness confirmed	1.3	19	2.5	unknown	1.0	80	-	unknown	0.16	29	-	witness confirmed	2.4	200	2.5	witness confirmed	0.17	25	2.6	witness confirmed	0.32	34	2.2	witness confirmed	3.0	140	2.7	witness confirmed	7.7	280	2.3	witness confirmed	8.5	280	2.6
minepump_spec3_product52_false-unreach-call.cil.c	witness confirmed	1.5	17	2.2	unknown	0.85	83	-	witness confirmed	0.17	29	2.3	witness confirmed	2.4	210	2.3	witness confirmed	0.17	25	2.5	witness confirmed	0.32	34	2.1	witness confirmed	3.1	130	2.8	witness confirmed	7.5	270	2.3	witness confirmed	11	400	2.2
minepump_spec3_product55_false-unreach-call.cil.c	witness confirmed	1.5	19	2.2	unknown	0.86	80	-	witness confirmed	0.22	30	2.4	witness confirmed	2.4	210	2.4	witness confirmed	0.22	31	2.6	witness confirmed	0.44	34	2.1	witness confirmed	3.8	190	2.7	witness confirmed	7.5	270	2.4	witness confirmed	11	400	2.3
minepump_spec3_product56_false-unreach-call.cil.c	witness confirmed	1.5	18	2.2	unknown	0.94	80	-	witness confirmed	0.21	30	2.3	witness confirmed	2.4	200	2.3	witness confirmed	0.20	31	2.6	witness confirmed	0.39	34	2.2	witness confirmed	3.9	190	2.8	witness confirmed	7.5	270	2.4	witness confirmed	11	300	2.2
minepump_spec3_product59_false-unreach-call.cil.c	witness confirmed	1.5	19	2.2	unknown	0.85	80	-	witness confirmed	0.18	31	2.3	witness confirmed	2.5	210	2.3	witness confirmed	0.15	26	2.6	witness confirmed	0.41	34	2.2	witness confirmed	3.4	160	2.8	witness confirmed	7.4	280	2.4	witness confirmed	10	400	2.3
minepump_spec3_product60_false-unreach-call.cil.c	witness confirmed	1.5	18	2.3	unknown	0.89	80	-	unknown	0.18	29	-	witness confirmed	2.4	210	2.3	witness confirmed	0.18	26	2.6	witness confirmed	0.36	34	2.2	witness confirmed	3.4	160	2.8	witness confirmed	7.4	270	2.4	witness confirmed	9.4	300	2.3
minepump_spec3_product63_false-unreach-call.cil.c	witness confirmed	1.5	17	2.3	unknown	0.98	79	-	witness confirmed	0.22	33	2.4	witness confirmed	2.4	200	2.4	witness confirmed	0.22	33	2.6	witness confirmed	0.46	34	2.2	witness confirmed	4.5	220	2.8	witness confirmed	7.9	280	2.4	witness confirmed	10	410	2.3
minepump_spec3_product64_false-unreach-call.cil.c	witness confirmed	1.5	22	2.2	unknown	1.0	79	-	unknown	0.19	31	-	witness confirmed	2.5	210	2.4	witness confirmed	0.21	33	2.6	witness confirmed	0.38	35	2.2	witness confirmed	4.6	220	2.7	witness confirmed	7.8	270	2.4	witness confirmed	10.0	290	2.2
minepump_spec3_productSimulator_false-unreach-call.cil.c	witness confirmed	2.1	22	3.4	unknown	0.86	80	-	witness confirmed	0.37	37	3.3	witness confirmed	3.1	210	3.4	witness confirmed	0.44	54	3.6	witness confirmed	0.69	39	3.2	witness confirmed	9.4	480	3.8	witness confirmed	8.6	280	3.2	witness confirmed	15	670	2.7
minepump_spec4_product33_false-unreach-call.cil.c	witness confirmed	30	36	3.4	unknown	0.94	80	-	witness confirmed	0.32	29	3.4	witness confirmed	3.4	210	3.7	witness confirmed	0.13	19	4.2	witness confirmed	0.31	37	3.2	witness confirmed	2.3	110	3.4	witness confirmed	10.0	300	3.5	timeout	920	1200	-
minepump_spec4_product34_false-unreach-call.cil.c	witness confirmed	26	37	4.1	unknown	0.97	80	-	witness confirmed	0.31	29	3.3	witness confirmed	3.5	210	4.1	witness confirmed	0.14	20	3.7	witness confirmed	0.43	39	3.3	witness confirmed	2.4	130	3.7	witness confirmed	12	400	3.6	timeout	920	1200	-
minepump_spec4_product35_false-unreach-call.cil.c	witness confirmed	50	66	3.6	unknown	0.98	80	-	witness confirmed	0.33	31	3.1	witness confirmed	3.5	220	3.7	witness confirmed	0.12	20	3.4	witness confirmed	0.39	41	3.1	witness confirmed	2.5	120	3.4	witness confirmed	11	390	3.4	timeout	920	1200	-
minepump_spec4_product36_false-unreach-call.cil.c	witness confirmed	40	62	4.2	unknown	1.0	80	-	true	0.29	29	-	witness confirmed	3.5	220	4.3	witness confirmed	0.14	20	3.5	witness confirmed	0.47	42	3.2	witness confirmed	2.5	110	3.6	witness confirmed	11	400	3.5	timeout	920	1200	-
minepump_spec4_product37_false-unreach-call.cil.c	witness confirmed	51	41	4.2	unknown	0.98	79	-	witness confirmed	0.32	31	3.4	witness confirmed	3.8	220	4.0	witness confirmed	0.15	22	3.6	witness confirmed	0.39	40	3.4	witness confirmed	2.9	130	4.0	witness confirmed	15	420	3.7	timeout	920	1600	-
minepump_spec4_product38_false-unreach-call.cil.c	witness confirmed	52	46	4.5	unknown	1.0	80	-	witness confirmed	0.33	30	3.5	witness confirmed	3.9	220	4.4	witness confirmed	0.16	23	3.9	witness confirmed	0.35	41	3.4	witness confirmed	2.8	130	3.8	witness confirmed	14	420	3.8	timeout	920	1200	-
minepump_spec4_product39_false-unreach-call.cil.c	witness confirmed	100	80	3.7	unknown	0.93	80	-	witness confirmed	0.37	30	3.2	witness confirmed	3.6	220	4.9	witness confirmed	0.17	23	3.5	witness confirmed	0.40	41	3.9	witness confirmed	3.0	130	3.6	witness confirmed	15	420	3.5	timeout	920	1200	-
minepump_spec4_product40_false-unreach-call.cil.c	witness confirmed	44	68	4.5	unknown	1.00	80	-	witness confirmed	0.35	30	3.4	witness confirmed	4.2	220	4.7	witness confirmed	0.17	23	3.5	witness confirmed	0.50	43	3.3	witness confirmed	2.9	130	3.8	witness confirmed	13	400	3.8	timeout	920	1600	-
minepump_spec4_product41_false-unreach-call.cil.c	witness confirmed	35	41	3.6	unknown	0.97	80	-	witness confirmed	0.34	29	3.4	witness confirmed	3.5	210	3.7	witness confirmed	0.13	20	3.5	witness confirmed	0.36	40	3.2	witness confirmed	2.5	130	3.9	witness confirmed	10	340	3.5	timeout	920	1200	-
minepump_spec4_product42_false-unreach-call.cil.c	witness confirmed	43	53	4.1	unknown	0.96	80	-	true	0.31	29	-	witness confirmed	3.8	220	4.1	witness confirmed	0.14	21	3.6	witness confirmed	0.34	40	3.3	witness confirmed	2.5	110	3.6	witness confirmed	10	350	3.6	timeout	920	2000	-
minepump_spec4_product43_false-unreach-call.cil.c	witness confirmed	120	78	3.7	unknown	1.0	80	-	witness confirmed	0.34	30	3.2	witness confirmed	3.5	220	3.8	witness confirmed	0.13	21	3.4	witness confirmed	0.38	42	3.1	witness confirmed	2.4	120	4.0	witness confirmed	11	400	3.7	timeout	920	1200	-
minepump_spec4_product44_false-unreach-call.cil.c	witness confirmed	150	110	4.8	unknown	0.97	79	-	true	0.32	30	-	witness confirmed	3.6	210	4.1	witness confirmed	0.15	21	3.4	witness confirmed	0.47	40	3.2	witness confirmed	2.6	120	3.8	witness confirmed	13	420	3.5	timeout	920	1200	-
minepump_spec4_product45_false-unreach-call.cil.c	witness confirmed	63	46	3.9	unknown	0.89	80	-	witness confirmed	0.36	30	3.3	witness confirmed	3.9	220	4.3	witness confirmed	0.17	23	3.6	witness confirmed	0.38	41	3.2	witness confirmed	3.2	160	3.7	witness confirmed	14	420	3.6	timeout	920	1200	-
minepump_spec4_product46_false-unreach-call.cil.c	witness confirmed	73	57	4.5	unknown	0.85	81	-	witness confirmed	0.35	30	3.5	witness confirmed	4.1	230	4.5	witness confirmed	0.16	24	3.7	witness confirmed	0.37	41	3.3	witness confirmed	3.2	160	3.8	witness confirmed	14	410	4.4	timeout	920	1200	-
minepump_spec4_product47_false-unreach-call.cil.c	witness confirmed	61	55	3.9	unknown	1.0	81	-	witness confirmed	0.37	32	3.3	witness confirmed	3.8	220	4.0	witness confirmed	0.15	24	3.8	witness confirmed	0.44	42	3.1	witness confirmed	3.1	150	3.7	witness confirmed	15	440	3.5	timeout	920	1200	-
minepump_spec4_product48_false-unreach-call.cil.c	witness confirmed	240	120	4.5	unknown	0.95	82	-	true	0.33	33	-	witness confirmed	3.9	220	4.6	witness confirmed	0.18	24	3.5	witness confirmed	0.44	40	3.3	witness confirmed	3.0	150	3.7	witness confirmed	13	410	4.1	timeout	920	1200	-
minepump_spec4_productSimulator_false-unreach-call.cil.c	timeout	920	460	-	unknown	0.98	79	-	true	1.1	58	-	witness confirmed	10.0	580	14	witness confirmed	0.43	53	8.4	witness confirmed	0.97	43	8.7	witness confirmed	13	490	8.6	witness confirmed	17	680	3.8	timeout	920	1200	-
minepump_spec1_product01_true-unreach-call.cil.c	true	0.058	12	-	unknown	0.88	81	-	true	0.74	27	-	true	2.3	160	-	true	0.10	19	-	true	0.21	27	-	true	2.8	110	-	true	6.7	270	-	true	170	1600	-
minepump_spec1_product02_true-unreach-call.cil.c	true	0.051	13	-	unknown	0.96	79	-	true	0.77	27	-	true	2.4	170	-	true	0.078	19	-	true	0.22	27	-	true	2.8	110	-	true	6.9	280	-	timeout	920	1200	-
minepump_spec1_product03_true-unreach-call.cil.c	true	0.050	13	-	unknown	1.0	79	-	true	0.80	27	-	true	2.6	190	-	true	0.11	19	-	true	0.22	27	-	true	3.1	110	-	true	6.8	270	-	true	150	1200	-
minepump_spec1_product04_true-unreach-call.cil.c	true	0.037	13	-	unknown	0.96	80	-	true	0.78	27	-	true	2.5	170	-	true	0.11	19	-	true	0.21	28	-	true	3.3	120	-	true	7.3	270	-	timeout	920	1600	-
minepump_spec1_product05_true-unreach-call.cil.c	true	0.073	14	-	unknown	0.98	80	-	true	0.79	27	-	true	2.4	170	-	true	0.097	19	-	true	0.21	27	-	true	3.1	120	-	true	6.7	270	-	timeout	920	1200	-
minepump_spec1_product06_true-unreach-call.cil.c	true	0.067	13	-	unknown	0.96	78	-	true	0.75	27	-	true	2.4	170	-	true	0.11	19	-	true	0.21	27	-	true	3.3	130	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec1_product07_true-unreach-call.cil.c	true	0.052	12	-	unknown	0.98	78	-	true	0.84	27	-	true	2.5	170	-	true	0.088	19	-	true	0.22	27	-	true	3.8	130	-	true	7.0	280	-	timeout	920	1200	-
minepump_spec1_product08_true-unreach-call.cil.c	true	0.069	12	-	unknown	0.97	81	-	true	0.84	27	-	true	2.5	170	-	true	0.10	19	-	true	0.37	27	-	true	240	140	-	true	6.8	270	-	timeout	920	1200	-
minepump_spec1_product09_true-unreach-call.cil.c	true	0.050	12	-	unknown	0.85	78	-	true	0.78	27	-	true	2.3	170	-	true	0.079	19	-	true	0.21	23	-	true	2.7	110	-	true	7.1	280	-	true	230	1600	-
minepump_spec1_product10_true-unreach-call.cil.c	true	0.055	13	-	unknown	0.86	81	-	true	0.79	27	-	true	2.4	160	-	true	0.097	19	-	true	0.22	27	-	true	2.8	110	-	true	7.1	280	-	timeout	920	1200	-
minepump_spec1_product11_true-unreach-call.cil.c	true	0.063	13	-	unknown	0.99	79	-	true	0.80	27	-	true	2.5	170	-	true	0.099	19	-	true	0.22	27	-	true	3.1	110	-	true	7.3	270	-	true	460	1600	-
minepump_spec1_product12_true-unreach-call.cil.c	true	0.047	12	-	unknown	0.97	80	-	true	0.80	27	-	true	2.5	170	-	true	0.11	19	-	true	0.21	28	-	true	3.2	120	-	true	7.1	280	-	true	850	1600	-
minepump_spec1_product13_true-unreach-call.cil.c	true	0.035	13	-	unknown	0.84	78	-	true	0.80	27	-	true	2.4	160	-	true	0.076	19	-	true	0.34	27	-	true	3.3	120	-	true	7.0	270	-	timeout	920	1200	-
minepump_spec1_product14_true-unreach-call.cil.c	true	0.052	13	-	unknown	0.95	80	-	true	0.81	27	-	true	2.4	170	-	true	0.11	19	-	true	0.37	27	-	true	3.1	130	-	true	7.4	280	-	timeout	920	1200	-
minepump_spec1_product15_true-unreach-call.cil.c	true	0.089	14	-	unknown	0.98	80	-	true	0.81	27	-	true	2.6	190	-	true	0.092	19	-	true	0.36	27	-	true	3.6	130	-	true	6.7	270	-	timeout	920	1200	-
minepump_spec1_product16_true-unreach-call.cil.c	true	0.068	13	-	unknown	0.98	82	-	true	0.81	29	-	true	2.6	170	-	true	0.093	19	-	true	0.23	28	-	true	250	140	-	true	7.1	270	-	timeout	920	1200	-
minepump_spec1_product17_true-unreach-call.cil.c	true	0.040	12	-	unknown	0.94	80	-	true	0.77	29	-	true	2.4	160	-	true	0.078	19	-	true	0.20	27	-	true	3.2	130	-	true	7.5	280	-	timeout	920	1200	-
minepump_spec1_product18_true-unreach-call.cil.c	true	0.048	13	-	unknown	1.0	83	-	true	0.81	27	-	true	2.4	170	-	true	0.081	19	-	true	0.22	27	-	true	3.2	130	-	true	7.4	280	-	timeout	920	1600	-
minepump_spec1_product19_true-unreach-call.cil.c	true	0.044	13	-	unknown	0.95	79	-	true	0.81	27	-	true	2.6	200	-	true	0.100	19	-	true	0.23	27	-	true	3.9	140	-	true	7.0	270	-	timeout	920	1600	-
minepump_spec1_product20_true-unreach-call.cil.c	true	0.069	13	-	unknown	0.99	80	-	true	0.83	27	-	true	2.6	190	-	true	0.081	19	-	true	0.22	27	-	true	240	150	-	true	7.1	270	-	timeout	920	1200	-
minepump_spec1_product21_true-unreach-call.cil.c	true	0.054	14	-	unknown	0.94	80	-	true	0.83	27	-	true	2.5	170	-	true	0.086	19	-	true	0.24	27	-	true	4.2	160	-	true	7.1	270	-	timeout	920	1200	-
minepump_spec1_product22_true-unreach-call.cil.c	true	0.070	12	-	unknown	0.84	80	-	true	0.81	27	-	true	2.5	170	-	true	0.10	19	-	true	0.23	27	-	true	4.3	180	-	true	7.7	270	-	timeout	920	1200	-
minepump_spec1_product23_true-unreach-call.cil.c	true	0.068	14	-	unknown	0.97	80	-	true	0.85	27	-	true	2.6	200	-	true	0.11	19	-	true	0.25	27	-	true	4.9	180	-	true	7.4	270	-	timeout	920	1200	-
minepump_spec1_product24_true-unreach-call.cil.c	true	0.049	13	-	unknown	0.94	80	-	true	0.83	27	-	true	2.6	190	-	true	0.11	19	-	true	0.23	27	-	true	300	180	-	true	7.1	270	-	timeout	920	1200	-
minepump_spec1_product25_true-unreach-call.cil.c	true	0.035	12	-	unknown	0.99	79	-	true	0.82	27	-	true	2.4	170	-	true	0.10	19	-	true	0.32	27	-	true	3.3	130	-	true	7.0	270	-	timeout	920	1200	-
minepump_spec1_product26_true-unreach-call.cil.c	true	0.073	12	-	unknown	0.99	80	-	true	0.78	27	-	true	2.4	170	-	true	0.091	19	-	true	0.22	27	-	true	3.4	130	-	true	7.3	270	-	timeout	920	1600	-
minepump_spec1_product27_true-unreach-call.cil.c	true	0.065	12	-	unknown	0.99	80	-	true	0.83	27	-	true	2.6	200	-	true	0.11	19	-	true	0.22	28	-	true	3.8	130	-	true	7.1	280	-	timeout	920	1200	-
minepump_spec1_product28_true-unreach-call.cil.c	true	0.042	13	-	unknown	0.98	80	-	true	0.81	27	-	true	2.5	170	-	true	0.10	19	-	true	0.22	27	-	true	240	140	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec1_product29_true-unreach-call.cil.c	true	0.063	13	-	unknown	0.87	79	-	true	0.80	27	-	true	2.5	170	-	true	0.093	19	-	true	0.24	27	-	true	4.1	160	-	true	8.4	270	-	true	630	1200	-
minepump_spec1_product30_true-unreach-call.cil.c	true	0.051	13	-	unknown	0.95	80	-	true	0.81	27	-	true	2.5	170	-	true	0.11	19	-	true	0.24	27	-	true	4.3	180	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec1_product31_true-unreach-call.cil.c	true	0.058	13	-	unknown	0.99	80	-	true	0.80	27	-	true	2.6	190	-	true	0.094	19	-	true	0.37	27	-	true	4.9	180	-	true	7.0	270	-	timeout	920	1200	-
minepump_spec1_product32_true-unreach-call.cil.c	true	0.070	13	-	unknown	0.96	80	-	true	0.84	27	-	true	2.6	200	-	true	0.11	20	-	true	0.24	27	-	true	300	180	-	true	7.6	270	-	timeout	920	1200	-
minepump_spec1_product45_true-unreach-call.cil.c	true	2.4	19	-	unknown	0.96	81	-	true	1.9	45	-	true	3.5	210	-	true	0.14	21	-	true	0.31	30	-	true	7.4	170	-	true	11	390	-	true	240	1200	-
minepump_spec1_product46_true-unreach-call.cil.c	true	2.5	19	-	unknown	0.98	78	-	true	1.9	44	-	true	3.6	200	-	true	0.15	22	-	true	0.31	30	-	true	12	200	-	true	11	400	-	timeout	920	1200	-
minepump_spec1_product47_true-unreach-call.cil.c	true	73	59	-	unknown	1.0	80	-	true	2.1	52	-	true	3.4	200	-	true	0.14	23	-	true	0.41	33	-	true	89	220	-	true	12	410	-	timeout	920	1200	-
minepump_spec1_product48_true-unreach-call.cil.c	true	78	67	-	unknown	0.98	80	-	true	2.0	54	-	true	3.7	200	-	true	0.14	23	-	true	0.31	33	-	true	340	230	-	true	9.0	300	-	timeout	920	1600	-
minepump_spec1_product57_true-unreach-call.cil.c	true	11	28	-	unknown	0.95	78	-	true	2.2	48	-	true	2.8	200	-	true	0.16	22	-	true	0.32	32	-	true	5.5	180	-	true	11	400	-	timeout	920	1200	-
minepump_spec1_product58_true-unreach-call.cil.c	true	11	30	-	unknown	0.98	79	-	true	2.2	48	-	true	2.9	200	-	true	0.17	23	-	true	0.34	32	-	true	6.7	200	-	true	14	420	-	timeout	920	1200	-
minepump_spec1_product59_true-unreach-call.cil.c	true	72	68	-	unknown	0.98	79	-	true	2.3	58	-	true	2.8	200	-	true	0.17	23	-	true	0.38	36	-	true	28	210	-	true	11	410	-	timeout	920	1200	-
minepump_spec1_product60_true-unreach-call.cil.c	true	120	96	-	unknown	1.0	81	-	true	2.3	58	-	true	3.0	200	-	true	0.18	24	-	true	0.47	36	-	true	330	190	-	true	15	430	-	timeout	920	1200	-
minepump_spec1_product61_true-unreach-call.cil.c	true	2.7	19	-	unknown	0.99	79	-	true	4.0	80	-	true	3.0	200	-	true	0.21	29	-	true	0.35	30	-	true	8.3	290	-	true	9.3	300	-	timeout	920	1200	-
minepump_spec1_product62_true-unreach-call.cil.c	true	2.7	20	-	unknown	0.98	80	-	true	4.0	79	-	true	3.0	200	-	true	0.20	30	-	true	0.34	31	-	true	10	310	-	true	11	390	-	timeout	920	1600	-
minepump_spec1_product63_true-unreach-call.cil.c	true	54	60	-	unknown	0.99	81	-	true	4.4	99	-	true	2.8	200	-	true	0.21	31	-	true	0.45	32	-	true	29	320	-	true	13	410	-	timeout	920	1200	-
minepump_spec1_product64_true-unreach-call.cil.c	true	89	80	-	unknown	0.97	80	-	true	4.4	99	-	true	3.0	200	-	true	0.23	31	-	true	0.48	32	-	true	360	300	-	true	13	410	-	timeout	920	1200	-
minepump_spec2_product01_true-unreach-call.cil.c	true	0.061	13	-	unknown	0.97	81	-	true	0.79	27	-	true	2.4	160	-	true	0.094	19	-	true	0.20	26	-	true	3.0	110	-	true	7.4	280	-	timeout	920	1200	-
minepump_spec2_product02_true-unreach-call.cil.c	true	0.065	14	-	unknown	0.98	83	-	true	0.81	27	-	true	2.4	170	-	true	0.098	19	-	true	0.22	27	-	true	2.8	110	-	true	7.6	270	-	timeout	920	1200	-
minepump_spec2_product03_true-unreach-call.cil.c	true	0.061	14	-	unknown	0.99	81	-	true	0.80	27	-	true	2.5	170	-	true	0.094	19	-	true	0.22	27	-	true	3.4	120	-	true	7.9	270	-	timeout	920	1200	-
minepump_spec2_product04_true-unreach-call.cil.c	true	0.063	13	-	unknown	0.93	82	-	true	0.85	27	-	true	2.5	170	-	true	0.099	19	-	true	0.21	27	-	true	3.3	120	-	true	7.5	270	-	timeout	920	1200	-
minepump_spec2_product05_true-unreach-call.cil.c	true	0.066	14	-	unknown	0.96	79	-	true	0.81	27	-	true	2.4	170	-	true	0.090	19	-	true	0.21	27	-	true	3.3	130	-	true	7.3	270	-	timeout	920	1600	-
minepump_spec2_product06_true-unreach-call.cil.c	true	0.061	13	-	unknown	0.98	81	-	true	0.85	27	-	true	2.4	170	-	true	0.11	19	-	true	0.21	27	-	true	3.4	130	-	true	7.6	280	-	timeout	920	1200	-
minepump_spec2_product07_true-unreach-call.cil.c	true	0.036	13	-	unknown	0.86	80	-	true	0.80	27	-	true	2.6	190	-	true	0.095	19	-	true	0.35	27	-	true	3.9	130	-	true	7.7	270	-	timeout	920	1200	-
minepump_spec2_product08_true-unreach-call.cil.c	true	0.061	13	-	unknown	0.87	80	-	true	0.83	27	-	true	3.0	180	-	true	0.11	19	-	true	0.24	27	-	true	210	140	-	true	7.7	270	-	timeout	920	1200	-
minepump_spec2_product09_true-unreach-call.cil.c	true	0.047	12	-	unknown	0.95	78	-	true	0.78	27	-	true	2.4	170	-	true	0.10	19	-	true	0.21	27	-	true	2.9	110	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec2_product10_true-unreach-call.cil.c	true	0.046	13	-	unknown	0.84	80	-	true	0.80	27	-	true	2.4	170	-	true	0.094	19	-	true	0.34	27	-	true	3.0	120	-	true	7.2	280	-	timeout	920	1600	-
minepump_spec2_product11_true-unreach-call.cil.c	true	0.045	12	-	unknown	0.93	80	-	true	0.80	27	-	true	2.5	170	-	true	0.11	19	-	true	0.23	27	-	true	3.4	120	-	true	7.6	280	-	timeout	920	1200	-
minepump_spec2_product12_true-unreach-call.cil.c	true	0.038	14	-	unknown	0.98	78	-	true	0.83	27	-	true	2.4	170	-	true	0.11	19	-	true	0.22	27	-	true	3.4	120	-	true	7.4	280	-	timeout	920	1200	-
minepump_spec2_product13_true-unreach-call.cil.c	true	0.053	13	-	unknown	0.95	80	-	true	0.81	27	-	true	2.4	170	-	true	0.089	19	-	true	0.21	27	-	true	3.3	130	-	true	7.4	270	-	timeout	920	1200	-
minepump_spec2_product14_true-unreach-call.cil.c	true	0.057	13	-	unknown	0.97	81	-	true	0.85	27	-	true	2.4	170	-	true	0.098	19	-	true	0.22	27	-	true	3.2	130	-	true	7.5	270	-	timeout	920	1200	-
minepump_spec2_product15_true-unreach-call.cil.c	true	0.046	12	-	unknown	0.98	82	-	true	0.85	27	-	true	2.6	190	-	true	0.098	19	-	true	0.23	27	-	true	3.9	130	-	true	7.6	280	-	timeout	920	1200	-
minepump_spec2_product16_true-unreach-call.cil.c	true	0.054	12	-	unknown	0.96	80	-	true	0.85	27	-	true	2.6	190	-	true	0.12	19	-	true	0.35	27	-	true	210	150	-	true	7.7	270	-	timeout	920	1200	-
minepump_spec2_product17_true-unreach-call.cil.c	true	0.064	12	-	unknown	0.86	79	-	true	0.77	27	-	true	2.4	170	-	true	0.11	19	-	true	0.20	27	-	true	3.6	140	-	true	7.8	270	-	timeout	920	1200	-
minepump_spec2_product18_true-unreach-call.cil.c	true	0.072	12	-	unknown	1.00	80	-	true	0.83	27	-	true	2.5	170	-	true	0.11	19	-	true	0.22	27	-	true	3.4	140	-	true	7.6	270	-	timeout	920	1600	-
minepump_spec2_product19_true-unreach-call.cil.c	true	0.045	14	-	unknown	0.93	81	-	true	0.84	27	-	true	2.7	200	-	true	0.084	19	-	true	0.23	29	-	true	3.9	150	-	true	8.0	270	-	timeout	920	1200	-
minepump_spec2_product20_true-unreach-call.cil.c	true	0.047	13	-	unknown	0.99	81	-	true	0.83	27	-	true	2.6	190	-	true	0.11	19	-	true	0.35	28	-	true	210	160	-	true	7.8	280	-	timeout	920	1600	-
minepump_spec2_product21_true-unreach-call.cil.c	true	0.067	13	-	unknown	0.84	80	-	true	0.79	27	-	true	2.5	170	-	true	0.11	20	-	true	0.24	27	-	true	4.4	170	-	true	8.3	280	-	timeout	920	1200	-
minepump_spec2_product22_true-unreach-call.cil.c	true	0.069	14	-	unknown	0.89	80	-	true	0.84	27	-	true	2.5	170	-	true	0.11	19	-	true	0.39	27	-	true	4.3	170	-	true	7.9	270	-	timeout	920	1200	-
minepump_spec2_product23_true-unreach-call.cil.c	true	0.053	13	-	unknown	0.97	80	-	true	0.85	27	-	true	2.7	190	-	true	0.098	20	-	true	0.38	27	-	true	5.2	180	-	true	7.9	270	-	timeout	920	1200	-
minepump_spec2_product24_true-unreach-call.cil.c	true	0.054	13	-	unknown	1.00	81	-	true	0.85	27	-	true	2.8	190	-	true	0.11	19	-	true	0.40	27	-	true	260	190	-	true	7.9	270	-	timeout	920	1200	-
minepump_spec2_product25_true-unreach-call.cil.c	true	0.067	12	-	unknown	0.98	80	-	true	0.81	27	-	true	2.4	170	-	true	0.091	19	-	true	0.22	27	-	true	3.3	130	-	true	7.3	280	-	timeout	920	1200	-
minepump_spec2_product26_true-unreach-call.cil.c	true	0.038	13	-	unknown	0.96	80	-	true	0.83	27	-	true	2.4	170	-	true	0.091	19	-	true	0.23	27	-	true	3.5	140	-	true	7.8	270	-	timeout	920	1600	-
minepump_spec2_product27_true-unreach-call.cil.c	true	0.050	13	-	unknown	0.96	81	-	true	0.79	27	-	true	2.6	200	-	true	0.11	19	-	true	0.23	27	-	true	3.9	140	-	true	8.1	270	-	timeout	920	1200	-
minepump_spec2_product28_true-unreach-call.cil.c	true	0.060	13	-	unknown	0.99	79	-	true	0.85	27	-	true	2.6	190	-	true	0.093	19	-	true	0.36	27	-	true	210	150	-	true	7.8	270	-	timeout	920	1200	-
minepump_spec2_product29_true-unreach-call.cil.c	true	0.064	14	-	unknown	1.0	79	-	true	0.79	27	-	true	2.5	170	-	true	0.097	20	-	true	0.24	27	-	true	4.2	180	-	true	8.0	270	-	timeout	920	1200	-
minepump_spec2_product30_true-unreach-call.cil.c	true	0.052	13	-	unknown	0.94	80	-	true	0.82	27	-	true	2.6	170	-	true	0.093	20	-	true	0.24	27	-	true	4.4	180	-	true	8.2	280	-	timeout	920	1200	-
minepump_spec2_product31_true-unreach-call.cil.c	true	0.039	13	-	unknown	1.0	80	-	true	0.83	27	-	true	2.7	200	-	true	0.093	19	-	true	0.26	27	-	true	5.0	180	-	true	8.0	270	-	timeout	920	1200	-
minepump_spec2_product32_true-unreach-call.cil.c	true	0.064	13	-	unknown	1.0	79	-	true	0.81	27	-	true	2.7	200	-	true	0.12	20	-	true	0.24	28	-	true	270	190	-	true	8.2	270	-	timeout	920	1600	-
minepump_spec2_product37_true-unreach-call.cil.c	true	32	40	-	unknown	0.99	79	-	true	1.7	39	-	true	3.5	200	-	true	0.15	20	-	true	0.32	33	-	true	5.9	180	-	true	14	430	-	timeout	920	1200	-
minepump_spec2_product38_true-unreach-call.cil.c	true	35	50	-	unknown	0.96	78	-	true	1.7	41	-	true	3.7	200	-	true	0.16	21	-	true	0.32	32	-	true	9.4	180	-	true	15	420	-	timeout	920	1200	-
minepump_spec2_product39_true-unreach-call.cil.c	true	140	110	-	unknown	0.98	77	-	true	1.8	46	-	true	3.4	200	-	true	0.16	22	-	true	0.33	35	-	true	56	200	-	true	13	400	-	timeout	920	1200	-
minepump_spec2_product40_true-unreach-call.cil.c	true	180	150	-	unknown	0.89	80	-	true	1.9	47	-	true	3.7	200	-	true	0.16	22	-	true	0.35	35	-	true	310	210	-	true	9.4	290	-	timeout	920	1600	-
minepump_spec2_product45_true-unreach-call.cil.c	true	6.8	20	-	unknown	0.95	80	-	true	1.9	45	-	true	3.5	210	-	true	0.15	21	-	true	0.29	30	-	true	6.9	200	-	true	10	330	-	timeout	920	1200	-
minepump_spec2_product46_true-unreach-call.cil.c	true	7.1	22	-	unknown	0.96	80	-	true	1.9	45	-	true	3.9	200	-	true	0.15	22	-	true	0.31	30	-	true	10	180	-	true	15	430	-	timeout	920	1200	-
minepump_spec2_product47_true-unreach-call.cil.c	true	110	89	-	unknown	0.94	80	-	true	2.2	54	-	true	3.5	200	-	true	0.14	23	-	true	0.35	34	-	true	46	210	-	true	9.7	300	-	timeout	920	1200	-
minepump_spec2_product48_true-unreach-call.cil.c	true	130	93	-	unknown	0.97	79	-	true	2.2	54	-	true	3.5	200	-	true	0.17	23	-	true	0.39	37	-	true	320	210	-	true	10	290	-	timeout	920	1600	-
minepump_spec2_product49_true-unreach-call.cil.c	true	86	82	-	unknown	0.97	79	-	true	1.8	41	-	true	2.9	200	-	true	0.15	21	-	true	0.33	34	-	true	4.9	190	-	true	16	410	-	timeout	920	1200	-
minepump_spec2_product50_true-unreach-call.cil.c	true	91	150	-	unknown	0.97	79	-	true	1.8	42	-	true	3.4	200	-	true	0.15	22	-	true	0.31	34	-	true	6.6	190	-	true	15	490	-	timeout	920	1200	-
minepump_spec2_product51_true-unreach-call.cil.c	true	130	110	-	unknown	1.0	80	-	true	2.1	49	-	true	2.9	200	-	true	0.52	24	-	true	0.43	37	-	true	13	170	-	true	13	400	-	timeout	920	1200	-
minepump_spec2_product52_true-unreach-call.cil.c	true	250	160	-	unknown	0.98	80	-	true	2.0	49	-	true	3.1	210	-	true	0.50	23	-	true	0.38	37	-	true	310	200	-	true	16	470	-	timeout	920	1200	-
minepump_spec2_product53_true-unreach-call.cil.c	true	80	75	-	unknown	0.95	80	-	true	3.1	65	-	true	3.0	200	-	true	0.18	26	-	true	0.34	32	-	true	7.6	270	-	true	15	420	-	timeout	920	1200	-
minepump_spec2_product54_true-unreach-call.cil.c	true	84	88	-	unknown	0.97	80	-	true	3.2	65	-	true	3.0	200	-	true	0.20	28	-	true	0.34	32	-	true	9.1	250	-	true	14	420	-	timeout	920	1200	-
minepump_spec2_product55_true-unreach-call.cil.c	true	160	140	-	unknown	0.99	79	-	true	3.6	83	-	true	3.0	200	-	true	0.57	30	-	true	0.41	35	-	true	20	280	-	true	13	430	-	timeout	920	1600	-
minepump_spec2_product56_true-unreach-call.cil.c	true	170	150	-	unknown	0.96	80	-	true	3.6	83	-	true	3.1	200	-	true	0.51	29	-	true	0.37	34	-	true	320	280	-	true	12	410	-	timeout	920	1200	-
minepump_spec2_product57_true-unreach-call.cil.c	true	55	67	-	unknown	0.99	80	-	true	2.4	49	-	true	2.8	200	-	true	0.14	22	-	true	0.37	35	-	true	5.4	210	-	true	16	540	-	timeout	920	1600	-
minepump_spec2_product58_true-unreach-call.cil.c	true	82	99	-	unknown	0.96	80	-	true	2.3	50	-	true	2.9	200	-	true	0.16	23	-	true	0.33	35	-	true	6.4	210	-	true	17	670	-	timeout	920	1200	-
minepump_spec2_product59_true-unreach-call.cil.c	true	72	63	-	unknown	0.98	81	-	true	2.4	60	-	true	2.9	200	-	true	0.17	24	-	true	0.42	37	-	true	15	210	-	true	18	670	-	timeout	920	1200	-
minepump_spec2_product60_true-unreach-call.cil.c	true	190	130	-	unknown	0.99	83	-	true	2.4	59	-	true	3.0	200	-	true	0.16	24	-	true	0.36	35	-	true	320	230	-	true	18	680	-	timeout	920	1600	-
minepump_spec2_product61_true-unreach-call.cil.c	true	6.9	22	-	unknown	0.96	83	-	true	4.2	80	-	true	3.0	200	-	true	0.21	28	-	true	0.37	31	-	true	8.8	300	-	true	14	430	-	timeout	920	1200	-
minepump_spec2_product62_true-unreach-call.cil.c	true	7.0	22	-	unknown	0.95	81	-	true	4.1	81	-	true	3.0	200	-	true	0.19	30	-	true	0.33	31	-	true	9.8	310	-	true	12	410	-	timeout	920	1200	-
minepump_spec2_product63_true-unreach-call.cil.c	true	72	63	-	unknown	0.98	81	-	true	4.5	99	-	true	3.0	200	-	true	0.21	31	-	true	0.42	33	-	true	26	290	-	true	15	420	-	timeout	920	1200	-
minepump_spec2_product64_true-unreach-call.cil.c	true	140	110	-	unknown	0.89	82	-	true	4.5	100	-	true	3.0	200	-	true	0.22	31	-	true	0.53	33	-	true	320	300	-	true	13	410	-	timeout	920	1600	-
minepump_spec3_product33_true-unreach-call.cil.c	true	8.4	23	-	unknown	0.97	81	-	true	1.3	39	-	true	3.2	200	-	true	0.12	20	-	true	0.25	30	-	true	5.7	130	-	true	7.9	270	-	timeout	920	1200	-
minepump_spec3_product34_true-unreach-call.cil.c	true	8.8	24	-	unknown	1.00	81	-	true	1.3	39	-	true	3.3	200	-	true	0.11	20	-	true	0.40	30	-	true	13	140	-	true	8.6	270	-	timeout	920	1600	-
minepump_spec3_product37_true-unreach-call.cil.c	true	93	49	-	unknown	0.97	80	-	true	1.8	42	-	true	3.5	210	-	true	0.15	21	-	true	0.42	30	-	true	7.7	180	-	true	9.5	300	-	timeout	920	1200	-
minepump_spec3_product38_true-unreach-call.cil.c	true	93	54	-	unknown	0.98	81	-	true	1.8	43	-	true	3.5	200	-	true	0.15	22	-	true	0.39	30	-	true	16	180	-	true	9.7	310	-	timeout	920	1600	-
minepump_spec3_product41_true-unreach-call.cil.c	true	50	36	-	unknown	0.88	81	-	true	1.5	41	-	true	3.3	200	-	true	0.13	19	-	true	0.27	30	-	true	6.8	150	-	true	9.5	300	-	timeout	920	1200	-
minepump_spec3_product42_true-unreach-call.cil.c	true	43	35	-	unknown	1.0	79	-	true	1.5	41	-	true	3.6	200	-	true	0.12	20	-	true	0.29	30	-	true	14	160	-	true	9.6	300	-	timeout	920	1200	-
minepump_spec3_product45_true-unreach-call.cil.c	true	160	66	-	unknown	0.98	80	-	true	2.1	48	-	true	3.5	200	-	true	0.14	22	-	true	0.28	30	-	true	9.8	210	-	true	11	410	-	timeout	920	1600	-
minepump_spec3_product46_true-unreach-call.cil.c	true	97	59	-	unknown	0.95	80	-	true	2.1	49	-	true	3.5	200	-	true	0.16	23	-	true	0.32	30	-	true	15	210	-	true	11	400	-	timeout	920	1200	-
minepump_spec3_product49_true-unreach-call.cil.c	true	78	46	-	unknown	0.98	79	-	true	2.0	43	-	true	3.0	200	-	true	0.15	21	-	true	0.29	32	-	true	5.0	180	-	true	10	330	-	timeout	920	1200	-
minepump_spec3_product50_true-unreach-call.cil.c	true	76	51	-	unknown	0.97	80	-	true	2.0	44	-	true	3.0	200	-	true	0.16	22	-	true	0.32	32	-	true	6.2	190	-	true	10	310	-	timeout	920	1200	-
minepump_spec3_product53_true-unreach-call.cil.c	exception (gremlins)	87	57	-	unknown	0.88	79	-	true	3.3	67	-	true	3.0	200	-	true	0.20	27	-	true	0.34	32	-	true	7.6	240	-	true	10	320	-	timeout	920	1600	-
minepump_spec3_product54_true-unreach-call.cil.c	true	430	160	-	unknown	1.00	81	-	true	3.5	68	-	true	3.0	200	-	true	0.19	28	-	true	0.35	32	-	true	9.0	280	-	true	10	340	-	timeout	920	1200	-
minepump_spec3_product57_true-unreach-call.cil.c	exception (gremlins)	47	41	-	unknown	0.94	80	-	true	2.5	53	-	true	3.0	200	-	true	0.17	22	-	true	0.34	31	-	true	5.5	200	-	true	12	400	-	timeout	920	1600	-
minepump_spec3_product58_true-unreach-call.cil.c	exception (gremlins)	50	47	-	unknown	0.96	81	-	true	2.5	53	-	true	2.9	200	-	true	0.17	23	-	true	0.32	31	-	true	6.7	200	-	true	11	410	-	timeout	920	1200	-
minepump_spec3_product61_true-unreach-call.cil.c	true	260	100	-	unknown	0.99	79	-	true	4.5	84	-	true	3.0	200	-	true	0.22	29	-	true	0.36	31	-	true	8.6	330	-	true	12	410	-	timeout	920	1200	-
minepump_spec3_product62_true-unreach-call.cil.c	exception (gremlins)	47	48	-	unknown	0.99	82	-	true	4.6	85	-	true	3.0	200	-	true	0.22	31	-	true	0.36	32	-	true	10.0	320	-	true	14	420	-	timeout	920	1600	-
minepump_spec4_product01_true-unreach-call.cil.c	true	0.036	14	-	unknown	0.86	80	-	true	0.77	27	-	true	2.3	160	-	true	0.096	19	-	true	0.20	27	-	true	2.6	110	-	true	8.2	270	-	true	120	1200	-
minepump_spec4_product02_true-unreach-call.cil.c	true	0.052	13	-	unknown	1.0	81	-	true	0.77	27	-	true	2.3	160	-	true	0.10	19	-	true	0.21	27	-	true	5.5	110	-	true	7.2	280	-	timeout	920	1200	-
minepump_spec4_product03_true-unreach-call.cil.c	true	0.051	12	-	unknown	0.95	77	-	true	0.80	27	-	true	2.5	170	-	true	0.082	19	-	true	0.23	27	-	true	16	120	-	true	6.8	270	-	timeout	920	1200	-
minepump_spec4_product04_true-unreach-call.cil.c	true	0.055	13	-	unknown	1.0	81	-	true	0.81	27	-	true	2.4	170	-	true	0.096	19	-	true	0.35	27	-	true	30	130	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec4_product05_true-unreach-call.cil.c	true	0.063	14	-	unknown	0.95	80	-	true	0.80	27	-	true	2.4	160	-	true	0.077	19	-	true	0.32	27	-	true	4.5	120	-	true	6.8	270	-	timeout	920	1200	-
minepump_spec4_product06_true-unreach-call.cil.c	true	0.052	12	-	unknown	0.88	79	-	true	0.84	27	-	true	2.4	170	-	true	0.10	19	-	true	0.23	27	-	true	7.1	130	-	true	7.0	270	-	timeout	920	1200	-
minepump_spec4_product07_true-unreach-call.cil.c	true	0.067	13	-	unknown	0.97	80	-	true	0.80	27	-	true	2.5	170	-	true	0.093	19	-	true	0.25	27	-	true	59	140	-	true	7.0	270	-	timeout	920	1200	-
minepump_spec4_product08_true-unreach-call.cil.c	true	0.051	12	-	unknown	0.99	80	-	true	0.81	27	-	true	2.5	170	-	true	0.100	19	-	true	0.21	27	-	true	840	130	-	true	7.1	280	-	timeout	920	1600	-
minepump_spec4_product09_true-unreach-call.cil.c	true	0.035	14	-	unknown	0.92	78	-	true	0.79	27	-	true	2.3	160	-	true	0.078	19	-	true	0.21	27	-	true	2.7	110	-	true	7.1	270	-	true	100	1200	-
minepump_spec4_product10_true-unreach-call.cil.c	true	0.052	12	-	unknown	0.98	79	-	true	0.76	27	-	true	2.3	160	-	true	0.11	19	-	true	0.21	27	-	true	5.5	120	-	true	6.7	270	-	timeout	920	1200	-
minepump_spec4_product11_true-unreach-call.cil.c	true	0.060	14	-	unknown	1.0	80	-	true	0.80	27	-	true	2.5	170	-	true	0.10	19	-	true	0.20	27	-	true	16	120	-	true	6.9	280	-	true	330	1200	-
minepump_spec4_product12_true-unreach-call.cil.c	true	0.069	12	-	unknown	0.85	79	-	true	0.83	29	-	true	2.4	170	-	true	0.089	19	-	true	0.22	27	-	true	31	130	-	true	6.9	280	-	timeout	920	1600	-
minepump_spec4_product13_true-unreach-call.cil.c	true	0.061	12	-	unknown	0.84	80	-	true	0.80	27	-	true	2.4	160	-	true	0.081	19	-	true	0.22	27	-	true	4.6	130	-	true	7.4	280	-	timeout	920	1200	-
minepump_spec4_product14_true-unreach-call.cil.c	true	0.071	12	-	unknown	0.97	80	-	true	0.80	27	-	true	2.4	160	-	true	0.089	19	-	true	0.22	27	-	true	7.1	130	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec4_product15_true-unreach-call.cil.c	true	0.066	12	-	unknown	0.96	79	-	true	0.83	27	-	true	2.5	170	-	true	0.096	19	-	true	0.22	27	-	true	61	130	-	true	6.9	270	-	timeout	920	1200	-
minepump_spec4_product16_true-unreach-call.cil.c	true	0.070	12	-	unknown	0.93	80	-	true	0.84	27	-	true	2.5	170	-	true	0.081	19	-	true	0.36	27	-	true	840	130	-	true	7.5	270	-	timeout	920	1200	-
minepump_spec4_product17_true-unreach-call.cil.c	true	0.036	13	-	unknown	0.98	79	-	true	0.79	27	-	true	2.4	160	-	true	0.099	19	-	true	0.22	27	-	true	5.1	130	-	true	6.8	270	-	timeout	920	1600	-
minepump_spec4_product18_true-unreach-call.cil.c	true	0.051	13	-	unknown	0.98	80	-	true	0.82	27	-	true	2.4	170	-	true	0.11	19	-	true	0.38	27	-	true	7.2	130	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec4_product19_true-unreach-call.cil.c	true	0.045	14	-	unknown	0.96	81	-	true	0.82	27	-	true	2.5	170	-	true	0.094	19	-	true	0.56	27	-	true	59	140	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec4_product20_true-unreach-call.cil.c	true	0.061	12	-	unknown	0.98	80	-	true	0.82	27	-	true	2.5	170	-	true	0.095	19	-	true	0.23	27	-	true	630	110	-	true	7.3	270	-	timeout	920	1200	-
minepump_spec4_product21_true-unreach-call.cil.c	true	0.052	13	-	unknown	0.98	80	-	true	0.81	27	-	true	2.5	170	-	true	0.097	19	-	true	0.23	27	-	true	6.2	170	-	true	7.7	280	-	timeout	920	1200	-
minepump_spec4_product22_true-unreach-call.cil.c	true	0.063	13	-	unknown	1.00	79	-	true	0.82	27	-	true	2.5	170	-	true	0.081	19	-	true	0.24	27	-	true	9.7	170	-	true	7.1	280	-	timeout	920	1200	-
minepump_spec4_product23_true-unreach-call.cil.c	true	0.051	13	-	unknown	0.95	80	-	true	0.82	27	-	true	2.6	170	-	true	0.11	19	-	true	0.24	27	-	true	61	180	-	true	7.3	270	-	timeout	920	1600	-
minepump_spec4_product24_true-unreach-call.cil.c	true	0.050	13	-	unknown	0.88	79	-	true	0.86	27	-	true	2.6	200	-	true	0.093	20	-	true	0.38	27	-	timeout	920	170	-	true	7.1	270	-	timeout	920	1200	-
minepump_spec4_product25_true-unreach-call.cil.c	true	0.057	13	-	unknown	0.99	80	-	true	0.78	27	-	true	2.4	170	-	true	0.078	19	-	true	0.35	27	-	true	4.7	130	-	true	7.1	270	-	timeout	920	1600	-
minepump_spec4_product26_true-unreach-call.cil.c	true	0.069	12	-	unknown	0.99	80	-	true	0.79	27	-	true	2.4	170	-	true	0.10	19	-	true	0.37	27	-	true	7.3	140	-	true	7.4	280	-	timeout	920	1200	-
minepump_spec4_product27_true-unreach-call.cil.c	true	0.056	13	-	unknown	0.99	78	-	true	0.80	27	-	true	2.5	170	-	true	0.086	19	-	true	0.22	27	-	true	66	140	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec4_product28_true-unreach-call.cil.c	true	0.051	14	-	unknown	0.94	80	-	true	0.82	29	-	true	2.6	190	-	true	0.097	19	-	true	0.22	27	-	true	580	110	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec4_product29_true-unreach-call.cil.c	true	0.054	14	-	unknown	0.95	80	-	true	0.77	27	-	true	2.5	170	-	true	0.10	19	-	true	0.22	27	-	true	5.8	160	-	true	6.9	270	-	timeout	920	1200	-
minepump_spec4_product30_true-unreach-call.cil.c	true	0.076	14	-	unknown	0.88	78	-	true	0.82	27	-	true	2.4	170	-	true	0.11	19	-	true	0.23	27	-	true	8.1	180	-	true	7.3	270	-	timeout	920	1200	-
minepump_spec4_product31_true-unreach-call.cil.c	true	0.053	12	-	unknown	0.96	80	-	true	0.84	27	-	true	2.6	190	-	true	0.11	19	-	true	0.24	27	-	true	59	180	-	true	7.2	280	-	timeout	920	1200	-
minepump_spec4_product32_true-unreach-call.cil.c	true	0.048	14	-	unknown	0.97	81	-	true	0.85	27	-	true	2.7	170	-	true	0.093	20	-	true	0.38	27	-	true	660	160	-	true	7.2	270	-	timeout	920	1200	-
minepump_spec4_product49_true-unreach-call.cil.c	true	50	46	-	unknown	0.99	79	-	true	1.8	41	-	true	2.8	200	-	true	0.13	20	-	true	0.29	31	-	true	4.3	180	-	true	13	420	-	timeout	920	1200	-
minepump_spec4_product50_true-unreach-call.cil.c	true	38	49	-	unknown	0.94	78	-	true	1.9	41	-	true	2.9	210	-	true	0.15	21	-	true	0.31	31	-	true	4.5	180	-	true	13	420	-	timeout	920	1200	-
minepump_spec4_product51_true-unreach-call.cil.c	true	29	55	-	unknown	0.99	78	-	true	2.0	48	-	true	2.8	200	-	true	0.15	22	-	true	0.46	37	-	true	4.8	190	-	true	12	420	-	timeout	920	1200	-
minepump_spec4_product52_true-unreach-call.cil.c	true	36	56	-	unknown	1.0	79	-	true	2.0	49	-	true	3.0	200	-	true	0.17	23	-	true	0.34	35	-	true	310	210	-	true	13	420	-	timeout	920	1200	-
minepump_spec4_product53_true-unreach-call.cil.c	true	170	92	-	unknown	0.94	80	-	true	3.2	65	-	true	3.1	210	-	true	0.18	26	-	true	0.34	34	-	true	7.0	280	-	true	12	420	-	timeout	920	1200	-
minepump_spec4_product54_true-unreach-call.cil.c	true	65	54	-	unknown	0.87	80	-	true	3.1	65	-	true	2.9	200	-	true	0.18	28	-	true	0.32	33	-	true	8.8	280	-	true	14	440	-	timeout	920	1200	-
minepump_spec4_product55_true-unreach-call.cil.c	true	27	51	-	unknown	0.99	79	-	true	3.5	83	-	true	2.9	200	-	true	0.21	29	-	true	0.42	37	-	true	35	260	-	true	13	420	-	timeout	920	1200	-
minepump_spec4_product56_true-unreach-call.cil.c	true	36	59	-	unknown	0.99	80	-	true	3.5	82	-	true	3.0	200	-	true	0.20	29	-	true	0.39	37	-	true	320	250	-	true	14	420	-	timeout	920	1200	-
minepump_spec4_product57_true-unreach-call.cil.c	true	81	60	-	unknown	0.89	80	-	true	2.2	53	-	true	2.8	200	-	true	0.17	22	-	true	0.35	32	-	true	5.4	180	-	true	13	430	-	timeout	920	1200	-
minepump_spec4_product58_true-unreach-call.cil.c	true	43	50	-	unknown	0.95	80	-	true	2.3	54	-	true	2.9	200	-	true	0.14	23	-	true	0.40	32	-	true	6.8	200	-	true	12	430	-	timeout	920	1200	-
minepump_spec4_product59_true-unreach-call.cil.c	true	51	49	-	unknown	0.98	80	-	true	2.5	63	-	true	2.8	200	-	true	0.17	24	-	true	0.48	36	-	true	14	210	-	true	13	420	-	timeout	920	1200	-
minepump_spec4_product60_true-unreach-call.cil.c	true	79	57	-	unknown	0.96	80	-	true	2.5	63	-	true	3.0	200	-	true	0.18	24	-	true	0.33	34	-	true	320	220	-	true	14	420	-	timeout	920	1200	-
minepump_spec4_product61_true-unreach-call.cil.c	true	88	58	-	unknown	0.99	80	-	true	4.3	84	-	true	2.9	200	-	true	0.19	29	-	true	0.37	32	-	true	8.6	290	-	true	14	460	-	timeout	920	1200	-
minepump_spec4_product62_true-unreach-call.cil.c	true	99	73	-	unknown	0.89	80	-	true	4.3	86	-	true	2.9	200	-	true	0.21	30	-	true	0.37	32	-	true	9.8	320	-	true	12	410	-	timeout	920	1600	-
minepump_spec4_product63_true-unreach-call.cil.c	true	54	50	-	unknown	0.96	84	-	true	4.7	100	-	true	2.9	200	-	true	0.23	31	-	true	0.52	35	-	true	35	320	-	true	13	420	-	timeout	920	1200	-
minepump_spec4_product64_true-unreach-call.cil.c	true	250	120	-	unknown	1.0	78	-	true	4.6	100	-	true	3.0	200	-	true	0.23	31	-	true	0.43	37	-	true	340	300	-	true	16	640	-	timeout	920	1200	-
minepump_spec5_product01_true-unreach-call.cil.c	true	0.050	13	-	unknown	0.96	80	-	true	0.82	27	-	true	2.4	160	-	true	0.093	19	-	true	0.34	27	-	true	4.5	120	-	true	8.3	280	-	timeout	920	1200	-
minepump_spec5_product02_true-unreach-call.cil.c	true	0.072	13	-	unknown	0.95	77	-	true	0.82	27	-	true	2.4	170	-	true	0.096	19	-	true	0.35	27	-	true	6.6	130	-	true	6.8	280	-	timeout	920	1200	-
minepump_spec5_product03_true-unreach-call.cil.c	true	0.068	14	-	unknown	0.85	80	-	true	0.82	27	-	true	2.6	200	-	true	0.10	19	-	true	0.23	27	-	true	29	120	-	true	6.7	270	-	timeout	920	1200	-
minepump_spec5_product04_true-unreach-call.cil.c	true	0.063	12	-	unknown	0.98	81	-	true	0.82	27	-	true	2.6	190	-	true	0.10	19	-	true	0.24	27	-	true	59	130	-	true	6.6	270	-	timeout	920	1200	-
minepump_spec5_product05_true-unreach-call.cil.c	true	0.054	13	-	unknown	0.97	80	-	true	0.78	27	-	true	2.5	170	-	true	0.10	19	-	true	0.37	27	-	true	5.2	140	-	true	7.0	280	-	timeout	920	1200	-
minepump_spec5_product06_true-unreach-call.cil.c	true	0.045	13	-	unknown	0.96	78	-	true	0.83	27	-	true	2.5	170	-	true	0.097	19	-	true	0.38	27	-	true	7.0	140	-	true	6.9	270	-	timeout	920	1200	-
minepump_spec5_product07_true-unreach-call.cil.c	true	0.060	13	-	unknown	0.99	80	-	true	0.81	27	-	true	2.8	200	-	true	0.11	19	-	true	0.22	28	-	true	62	150	-	true	7.2	280	-	timeout	920	1200	-
minepump_spec5_product08_true-unreach-call.cil.c	true	0.048	14	-	unknown	0.97	80	-	true	0.86	27	-	true	2.7	200	-	true	0.096	19	-	true	0.23	27	-	true	100	110	-	true	7.0	270	-	timeout	920	1200	-
minepump_spec5_product09_true-unreach-call.cil.c	true	0.069	12	-	unknown	1.00	81	-	true	0.79	27	-	true	2.4	170	-	true	0.078	19	-	true	0.23	27	-	true	4.2	120	-	true	6.9	270	-	timeout	920	1200	-
minepump_spec5_product10_true-unreach-call.cil.c	true	0.042	12	-	unknown	0.96	80	-	true	0.84	27	-	true	2.4	160	-	true	0.11	19	-	true	0.21	27	-	true	6.4	120	-	true	6.7	270	-	timeout	920	1200	-
minepump_spec5_product11_true-unreach-call.cil.c	true	0.044	12	-	unknown	0.87	80	-	true	0.81	27	-	true	2.7	200	-	true	0.092	19	-	true	0.22	27	-	true	29	130	-	true	6.9	270	-	true	320	1200	-
minepump_spec5_product12_true-unreach-call.cil.c	true	0.064	14	-	unknown	0.99	79	-	true	0.86	27	-	true	2.6	170	-	true	0.11	19	-	true	0.21	28	-	true	59	130	-	true	6.5	270	-	timeout	920	1200	-
minepump_spec5_product13_true-unreach-call.cil.c	true	0.064	12	-	unknown	0.93	80	-	true	0.85	27	-	true	2.5	170	-	true	0.093	19	-	true	0.21	27	-	true	5.2	140	-	true	7.1	270	-	timeout	920	1600	-
minepump_spec5_product14_true-unreach-call.cil.c	true	0.050	14	-	unknown	0.96	80	-	true	0.81	27	-	true	2.5	170	-	true	0.11	19	-	true	0.24	27	-	true	6.8	150	-	true	6.9	270	-	timeout	920	1600	-
minepump_spec5_product15_true-unreach-call.cil.c	true	0.057	12	-	unknown	0.94	80	-	true	0.86	27	-	true	2.7	200	-	true	0.10	19	-	true	0.25	27	-	true	60	150	-	true	6.7	280	-	timeout	920	1600	-
minepump_spec5_product16_true-unreach-call.cil.c	true	0.050	13	-	unknown	0.95	80	-	true	0.86	27	-	true	2.7	200	-	true	0.099	19	-	true	0.24	27	-	true	100	120	-	true	7.0	270	-	timeout	920	1200	-
minepump_spec5_product17_true-unreach-call.cil.c	true	0.054	13	-	unknown	0.97	79	-	true	0.79	27	-	true	2.7	170	-	true	0.11	19	-	true	0.23	27	-	true	5.2	150	-	true	6.8	270	-	timeout	920	1200	-
minepump_spec5_product18_true-unreach-call.cil.c	true	0.052	14	-	unknown	0.99	80	-	true	0.82	27	-	true	2.5	170	-	true	0.11	19	-	true	0.34	27	-	true	7.9	150	-	true	6.7	280	-	timeout	920	1200	-
minepump_spec5_product19_true-unreach-call.cil.c	true	0.060	14	-	unknown	0.88	79	-	true	0.86	27	-	true	2.7	200	-	true	0.082	19	-	true	0.23	27	-	true	61	160	-	true	7.1	280	-	timeout	920	1600	-
minepump_spec5_product20_true-unreach-call.cil.c	true	0.071	12	-	unknown	0.95	80	-	true	0.80	27	-	true	2.9	200	-	true	0.11	19	-	true	0.23	27	-	true	100	120	-	true	7.1	270	-	timeout	920	1200	-
minepump_spec5_product21_true-unreach-call.cil.c	true	0.055	13	-	unknown	0.99	79	-	true	0.81	27	-	true	2.5	180	-	true	0.10	19	-	true	0.24	27	-	true	6.3	190	-	true	6.8	270	-	timeout	920	1600	-
minepump_spec5_product22_true-unreach-call.cil.c	true	0.052	12	-	unknown	1.00	79	-	true	0.84	27	-	true	2.6	180	-	true	0.12	20	-	true	0.37	27	-	true	8.3	190	-	true	7.1	270	-	timeout	920	1200	-
minepump_spec5_product23_true-unreach-call.cil.c	true	0.071	14	-	unknown	0.97	81	-	true	0.84	27	-	true	2.9	200	-	true	0.10	20	-	true	0.23	27	-	true	70	200	-	true	6.8	270	-	timeout	920	1600	-
minepump_spec5_product24_true-unreach-call.cil.c	true	0.059	13	-	unknown	0.99	78	-	true	0.86	27	-	true	2.7	200	-	true	0.11	20	-	true	0.26	27	-	true	100	140	-	true	7.3	270	-	timeout	920	1200	-
minepump_spec5_product25_true-unreach-call.cil.c	true	0.037	14	-	unknown	0.99	80	-	true	0.88	27	-	true	2.5	170	-	true	0.11	19	-	true	0.25	23	-	true	5.1	150	-	true	7.1	280	-	timeout	920	1200	-
minepump_spec5_product26_true-unreach-call.cil.c	true	0.039	14	-	unknown	0.96	80	-	true	0.81	29	-	true	2.5	170	-	true	0.12	19	-	true	0.24	27	-	true	7.0	150	-	true	6.9	270	-	timeout	920	1600	-
minepump_spec5_product27_true-unreach-call.cil.c	true	0.068	13	-	unknown	0.96	79	-	true	0.83	27	-	true	2.7	200	-	true	0.084	20	-	true	0.23	27	-	true	62	160	-	true	6.8	270	-	timeout	920	1200	-
minepump_spec5_product28_true-unreach-call.cil.c	true	0.054	12	-	unknown	0.98	81	-	true	0.83	27	-	true	2.7	200	-	true	0.11	20	-	true	0.25	27	-	true	100	110	-	true	7.3	280	-	timeout	920	1200	-
minepump_spec5_product29_true-unreach-call.cil.c	true	0.064	13	-	unknown	1.0	79	-	true	0.84	27	-	true	2.7	170	-	true	0.11	20	-	true	0.23	27	-	true	6.2	190	-	true	6.7	270	-	timeout	920	1200	-
minepump_spec5_product30_true-unreach-call.cil.c	true	0.049	14	-	unknown	0.97	80	-	true	0.86	27	-	true	2.5	170	-	true	0.083	20	-	true	0.25	27	-	true	8.3	190	-	true	7.3	270	-	timeout	920	1200	-
minepump_spec5_product31_true-unreach-call.cil.c	true	0.058	14	-	unknown	1.0	80	-	true	0.86	27	-	true	2.8	200	-	true	0.10	20	-	true	0.25	27	-	true	68	210	-	true	7.1	280	-	timeout	920	2000	-
minepump_spec5_product32_true-unreach-call.cil.c	true	0.066	14	-	unknown	0.97	80	-	true	0.85	27	-	true	2.8	200	-	true	0.11	20	-	true	0.23	28	-	true	100	140	-	true	6.7	270	-	timeout	920	1200	-
minepump_spec5_product33_true-unreach-call.cil.c	true	73	63	-	unknown	0.94	81	-	true	1.2	38	-	true	3.6	200	-	true	0.13	19	-	true	0.30	31	-	true	3.6	150	-	true	9.3	300	-	timeout	920	1600	-
minepump_spec5_product34_true-unreach-call.cil.c	true	37	42	-	unknown	0.94	80	-	true	1.3	38	-	true	3.6	200	-	true	0.13	20	-	true	0.43	31	-	true	3.7	150	-	true	9.4	320	-	timeout	920	1200	-
minepump_spec5_product35_true-unreach-call.cil.c	true	110	120	-	unknown	0.98	81	-	true	1.3	38	-	true	3.5	200	-	true	0.12	20	-	true	0.30	31	-	true	14	150	-	true	10.0	330	-	timeout	920	1200	-
minepump_spec5_product36_true-unreach-call.cil.c	exception (gremlins)	160	150	-	unknown	0.98	81	-	true	1.6	40	-	true	3.8	200	-	true	0.15	20	-	true	0.33	31	-	true	150	160	-	true	20	680	-	timeout	920	1200	-
minepump_spec5_product37_true-unreach-call.cil.c	true	210	140	-	unknown	0.96	81	-	true	1.9	40	-	true	4.0	200	-	true	0.15	21	-	true	0.38	32	-	true	7.3	190	-	true	18	680	-	timeout	920	1200	-
minepump_spec5_product38_true-unreach-call.cil.c	true	270	150	-	unknown	0.86	82	-	true	1.9	40	-	true	3.8	200	-	true	0.15	21	-	true	0.39	32	-	true	11	190	-	true	19	680	-	timeout	920	1200	-
minepump_spec5_product39_true-unreach-call.cil.c	true	130	130	-	unknown	0.98	80	-	true	2.1	48	-	true	4.1	200	-	true	0.15	22	-	true	0.44	35	-	true	310	210	-	true	18	670	-	timeout	920	1200	-
minepump_spec5_product40_true-unreach-call.cil.c	exception (gremlins)	230	150	-	unknown	0.98	80	-	true	2.1	47	-	true	4.0	200	-	true	0.16	22	-	true	0.30	32	-	true	320	230	-	true	22	680	-	timeout	920	1200	-
minepump_spec5_product41_true-unreach-call.cil.c	true	150	91	-	unknown	0.86	80	-	true	1.4	40	-	true	3.5	200	-	true	0.14	20	-	true	0.33	34	-	true	14	160	-	true	12	400	-	timeout	920	1600	-
minepump_spec5_product42_true-unreach-call.cil.c	true	71	66	-	unknown	0.98	80	-	true	1.5	40	-	true	3.5	200	-	true	0.14	20	-	true	0.33	34	-	true	20	160	-	true	9.9	350	-	timeout	920	1600	-
minepump_spec5_product43_true-unreach-call.cil.c	true	340	160	-	unknown	0.96	80	-	true	1.6	42	-	true	3.5	200	-	true	0.12	20	-	true	0.29	32	-	true	66	160	-	true	9.8	410	-	timeout	920	1600	-
minepump_spec5_product44_true-unreach-call.cil.c	exception (gremlins)	430	170	-	unknown	0.98	80	-	true	1.8	42	-	true	3.8	200	-	true	0.15	20	-	true	0.39	32	-	true	330	170	-	true	19	670	-	timeout	920	1200	-
minepump_spec5_product45_true-unreach-call.cil.c	true	390	150	-	unknown	0.98	79	-	true	2.5	46	-	true	3.8	200	-	true	0.16	21	-	true	0.33	31	-	true	12	220	-	true	20	680	-	timeout	920	1200	-
minepump_spec5_product46_true-unreach-call.cil.c	true	320	150	-	unknown	0.97	80	-	true	2.4	47	-	true	3.7	200	-	true	0.16	23	-	true	0.36	31	-	true	24	220	-	true	20	680	-	timeout	920	1200	-
minepump_spec5_product47_true-unreach-call.cil.c	true	490	160	-	unknown	0.98	83	-	true	2.5	56	-	true	3.9	200	-	true	0.17	23	-	true	0.43	32	-	true	130	220	-	true	20	680	-	timeout	920	1600	-
minepump_spec5_product48_true-unreach-call.cil.c	exception (gremlins)	550	180	-	unknown	0.96	80	-	true	2.5	55	-	true	4.0	200	-	true	0.17	23	-	true	0.34	32	-	true	330	250	-	true	23	890	-	timeout	920	1600	-
minepump_spec5_product49_true-unreach-call.cil.c	true	23	33	-	unknown	0.99	80	-	true	1.9	41	-	true	3.4	210	-	true	0.14	21	-	true	0.31	31	-	true	4.8	190	-	true	18	670	-	timeout	920	1200	-
minepump_spec5_product50_true-unreach-call.cil.c	true	33	65	-	unknown	0.89	79	-	true	1.9	42	-	true	3.4	200	-	true	0.15	22	-	true	0.35	32	-	true	5.0	200	-	true	18	670	-	timeout	920	1200	-
minepump_spec5_product51_true-unreach-call.cil.c	true	140	140	-	unknown	1.0	80	-	true	2.1	48	-	true	3.3	200	-	true	0.39	24	-	true	0.36	35	-	true	19	210	-	true	18	670	-	timeout	920	1600	-
minepump_spec5_product52_true-unreach-call.cil.c	true	180	150	-	unknown	0.97	80	-	true	2.1	49	-	true	3.5	200	-	true	0.40	24	-	true	0.34	32	-	true	26	210	-	true	19	680	-	timeout	920	1600	-
minepump_spec5_product53_true-unreach-call.cil.c	true	49	38	-	unknown	0.96	79	-	true	3.3	65	-	true	3.5	210	-	true	0.19	27	-	true	0.51	32	-	true	8.1	290	-	true	19	680	-	timeout	920	1600	-
minepump_spec5_product54_true-unreach-call.cil.c	true	100	83	-	unknown	0.98	78	-	true	3.1	66	-	true	3.8	200	-	true	0.19	28	-	true	0.43	32	-	true	8.5	300	-	true	19	680	-	timeout	920	1200	-
minepump_spec5_product55_true-unreach-call.cil.c	true	260	150	-	unknown	0.97	80	-	true	3.6	84	-	true	3.4	210	-	true	0.47	31	-	true	0.41	34	-	true	270	330	-	true	19	680	-	timeout	920	1200	-
minepump_spec5_product56_true-unreach-call.cil.c	true	590	210	-	unknown	1.00	79	-	true	3.8	83	-	true	3.6	200	-	true	0.44	30	-	true	0.36	32	-	true	330	310	-	true	21	680	-	timeout	920	1200	-
minepump_spec5_product57_true-unreach-call.cil.c	true	25	28	-	unknown	0.97	82	-	true	2.4	53	-	true	3.4	200	-	true	0.17	22	-	true	0.32	32	-	true	5.8	220	-	true	18	670	-	timeout	920	1600	-
minepump_spec5_product58_true-unreach-call.cil.c	true	25	32	-	unknown	0.97	80	-	true	2.4	54	-	true	3.7	200	-	true	0.15	23	-	true	0.34	32	-	true	7.2	210	-	true	18	680	-	timeout	920	1200	-
minepump_spec5_product59_true-unreach-call.cil.c	true	400	150	-	unknown	1.0	79	-	true	2.7	66	-	true	3.3	200	-	true	0.15	24	-	true	0.42	32	-	true	20	210	-	true	20	680	-	timeout	920	1200	-
minepump_spec5_product60_true-unreach-call.cil.c	exception (gremlins)	520	250	-	unknown	1.00	80	-	true	2.6	64	-	true	3.4	200	-	true	0.17	24	-	true	0.31	32	-	true	330	230	-	true	19	690	-	timeout	920	1200	-
minepump_spec5_product61_true-unreach-call.cil.c	true	26	30	-	unknown	0.99	80	-	true	4.4	85	-	true	3.4	200	-	true	0.20	29	-	true	0.36	31	-	true	9.3	340	-	true	19	670	-	timeout	920	1600	-
minepump_spec5_product62_true-unreach-call.cil.c	true	27	33	-	unknown	0.98	80	-	true	4.4	84	-	true	3.8	200	-	true	0.21	31	-	true	0.37	31	-	true	11	340	-	true	20	680	-	timeout	920	1200	-
minepump_spec5_product63_true-unreach-call.cil.c	true	610	190	-	unknown	1.0	82	-	true	4.9	100	-	true	3.5	200	-	true	0.21	31	-	true	0.46	32	-	true	37	340	-	true	19	690	-	timeout	920	1200	-
minepump_spec5_product64_true-unreach-call.cil.c	timeout	920	330	-	unknown	1.00	82	-	true	4.9	100	-	true	3.4	200	-	true	0.22	32	-	true	0.39	32	-	true	340	360	-	true	21	690	-	timeout	920	1200	-
minepump_spec5_productSimulator_true-unreach-call.cil.c	timeout	920	380	-	unknown	0.90	81	-	true	15	240	-	true	46	2300	-	true	0.46	52	-	true	0.73	37	-	true	800	460	-	true	26	1200	-	timeout	920	1600	-
../../sv-benchmarks/c/product-lines/	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness	status	time(s)	memory(MB)	time(s) for witness
total files	597	160000	130000	2200	597	690	54000	-	597	4900	30000	3500	597	4700	260000	7100	597	1400	40000	4600	597	7000	34000	4400	597	36000	470000	4400	597	91000	1200000	270	597	320000	600000	160
correct results	389	19000	21000	1000	0	-	-	-	523	1900	22000	2700	569	4100	220000	4300	586	430	31000	3700	584	3500	29000	3500	586	32000	440000	3600	325	3300	110000	270	76	5000	51000	160
false negatives	0	-	-	-	0	-	-	-	38	1800	3800	0	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-
false positives	2	180	430	0	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-
false properties	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-	0	-	-	-
score (597 files, max score: 929)	637	-	-	-	0	-	-	-	399	-	-	-	901	-	-	-	917	-	-	-	913	-	-	-	917	-	-	-	554	-	-	-	87	-	-	-
Tool	BLAST 2.7.3				Cascade 0.1				CBMC 4.9				CPAchecker 1.3.10-svcomp15				ESBMC 1.24				Seahorn				SMACK				Ultimate Automizer r12950				Ultimate Kojak r12950