results.2016-09-03_1437 – BenchExec results

Tool	CPAchecker 1.6.1-svn 22870
Limits	timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
OS	Linux 4.4.0-34-generic
System	CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135148 MB
Run set	bmc-bitprecise.BMC.ProductLines									k-induction-bitprecise.k-Induction.ProductLines												predicateAnalysis-bitprecise.PredicateAbstraction.ProductLines															impact-bitprecise.Impact.ProductLines
Options	-heap 10000M -noout -bmc -setprop solver.solver=MATHSAT5 -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.bounds.maxLoopIterationsUpperBound=0 -setprop cpa.bounds.maxLoopIterations=1 -setprop cpa.bounds.maxLoopIterationAdjusterFactory=INCREMENT									-heap 10000M -noout -sv-comp16--k-induction -setprop limits.time.cpu.thread=10000s												-heap 10000M -noout -predicateAnalysis-PredAbsRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC															-heap 10000M -noout -predicateAnalysis-ImpactRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.forcedCovering=cpa.predicate.PredicateForcedCovering
test/programs/benchmarks/product-lines/	status	cputime (s)	walltime (s)	memUsage	host	k	BMC formula creation (s)	SMT check (s)	Bounds check (s)	status	cputime (s)	walltime (s)	memUsage	host	k	BMC formula creation (s)	SMT check (s)	Invariant generation (s)	Bounds check (s)	Induction formula creation (s)	Induction check (s)	status	cputime (s)	walltime (s)	memUsage	host	Refinement (s)	Precision adjustment (s)	CPA algorithm (s)	Post operator (s)	Prec operator (s)	Abstraction (s)	Solving (s)	Model enumeration (s)	SMT without itp (s)	Boolean abstraction (s)	status	cputime (s)	walltime (s)	memUsage	host	Attempted forced coverings	Refinement (s)	Precision adjustment (s)	CPA algorithm (s)	Post operator (s)	Prec operator (s)	Abstraction (s)	Solving (s)	Model enumeration (s)	SMT without itp (s)	Forced covering (s)	Successful forced coverings	Boolean abstraction (s)
elevator_spec14_product20_false-unreach-call.cil.c	false(reach)	19.6	11.1	727957504		1	1.53	.004		false(reach)	72.5	36.7	1351553024		1	2.36	.017	9.29				false(reach)	78.0	52.6	1859104768		22.2	7.96	19.1	5.80	7.25	7.08	5.94	.00	5.94		false(reach)	66.1	43.5	1862713344		0	17.9	.899	13.8	7.32	.150	.001	.00	.00	.00	.070
elevator_spec14_product24_false-unreach-call.cil.c	false(reach)	21.0	12.2	762789888		1	1.58	.005		false(reach)	90.3	45.6	1605537792		1	2.91	.004	14.5				false(reach)	87.1	63.3	2394165248		22.9	8.93	26.0	8.63	7.86	7.61	6.45	.00	6.45		false(reach)	79.7	56.6	2199109632		0	24.3	.934	17.8	9.46	.186	.002	.00	.00	.00	.082
elevator_spec14_product28_false-unreach-call.cil.c	false(reach)	19.6	11.1	726867968		1	1.46	.005		false(reach)	80.4	40.7	1359736832		1	2.42	.006	12.1				false(reach)	80.7	54.7	1907412992		21.6	7.74	21.3	6.71	6.97	6.84	5.73	.00	5.73		false(reach)	67.9	45.7	1872072704		0	20.2	.819	13.5	6.98	.155	.004	.00	.00	.00	.099
elevator_spec14_product32_false-unreach-call.cil.c	false(reach)	21.3	12.4	763023360		1	1.86	.032		false(reach)	86.8	43.8	1613574144		1	2.84	.011	.005				false(reach)	95.5	66.8	2354495488		24.8	8.86	27.0	9.14	7.99	7.79	6.44	.00	6.44		false(reach)	80.5	57.3	2356092928		0	25.5	.901	17.5	10.1	.169	.001	.00	.00	.00	.116
elevator_spec14_productSimulator_false-unreach-call.cil.c	false(reach)	214	190	2360836096		1	11.8	2.57		false(reach)	523	262	5285154816		1	17.7	2.40	200				timeout	1000	967	4689915904												timeout	1000	968	4577275904
elevator_spec1_product18_false-unreach-call.cil.c	false(reach)	18.7	10.1	571920384		3	1.86	.004	.014	false(reach)	96.9	48.9	1659928576		3	3.66	.005	13.2	.023	19.0	3.83	timeout	903	869	1437609984		3.93	833	860	13.5	831	831	13.7	813	827	828	false(reach)	87.7	60.7	1618284544		6	17.4	6.72	32.8	8.58	5.89	5.66	3.42	1.39	4.89	10.8	1	4.82
elevator_spec1_product20_false-unreach-call.cil.c	false(reach)	17.8	9.64	581402624		3	1.80	.002	.008	false(reach)	105	52.8	1838899200		3	4.44	.014	.005	.033	20.1	5.59	false(reach)	794	756	2264457216		15.3	692	729	18.4	689	689	31.0	652	683	683	false(reach)	94.4	68.5	1782702080		6	17.6	9.93	41.1	10.3	8.93	8.68	5.23	2.47	7.88	13.0	0	7.72
elevator_spec1_product22_false-unreach-call.cil.c	false(reach)	19.7	10.7	622419968		3	2.03	.018	.009	false(reach)	113	57.1	2000007168		3	3.28	.004	19.2	.028	21.3	5.61	timeout	903	868	1955151872		9.11	817	854	17.9	814	813	32.7	775	807	808	false(reach)	104	76.5	2036858880		4	20.7	9.19	42.7	12.2	8.13	7.84	4.98	1.84	7.06	12.1	1	6.84
elevator_spec1_product24_false-unreach-call.cil.c	false(reach)	18.9	10.4	568958976		3	1.75	.004	.020	false(reach)	130	65.8	2269085696		3	3.31	.006	21.6	.042	25.6	7.90	timeout	903	869	1802854400		5.05	824	859	17.8	822	822	18.8	798	817	818	false(reach)	121	92.7	2087391232		4	22.7	9.57	57.2	11.8	8.46	8.22	4.74	2.41	7.37	25.9	1	7.18
elevator_spec1_product26_false-unreach-call.cil.c	false(reach)	18.6	10.0	571379712		3	1.72	.003	.012	false(reach)	108	54.4	1692684288		3	3.17	.004	15.3	.028	19.4	3.74	timeout	903	869	1624776704		5.95	826	858	14.6	824	823	23.2	795	818	818	false(reach)	92.7	64.9	1685303296		6	18.3	8.06	36.3	9.43	6.94	6.74	4.11	1.76	5.95	11.6	1	5.88
elevator_spec1_product28_false-unreach-call.cil.c	false(reach)	18.7	10.2	586661888		3	1.91	.003	.035	false(reach)	106	53.7	1785593856		3	3.88	.005	15.5	.033	19.6	4.41	timeout	904	868	1719083008		8.18	819	855	16.4	817	816	33.8	776	810	811	false(reach)	96.2	70.2	1891782656		6	17.6	11.1	41.8	10.2	9.70	9.35	5.04	3.21	8.49	12.2	0	8.27
elevator_spec1_product30_false-unreach-call.cil.c	false(reach)	19.8	10.9	722743296		3	2.14	.004	.006	false(reach)	115	58.1	2209026048		3	2.81	.004	19.9	.009	19.4	7.39	timeout	903	870	1689251840		4.93	828	860	15.7	826	825	20.5	801	821	822	false(reach)	145	116	2030002176		6	22.7	9.24	81.2	11.1	7.74	7.53	4.34	2.18	6.62	52.4	1	6.53
elevator_spec1_product32_false-unreach-call.cil.c	false(reach)	18.9	10.3	587161600		3	1.79	.004	.023	false(reach)	129	65.0	2269237248		3	3.32	.006	23.1	.056	23.6	10.8	timeout	903	871	1559007232		5.04	829	861	15.9	827	826	18.7	804	822	823	false(reach)	116	86.3	2078511104		4	22.7	11.9	50.4	11.8	10.1	9.85	5.56	3.24	8.99	17.4	1	8.81
elevator_spec1_productSimulator_false-unreach-call.cil.c	false(reach)	47.8	27.6	1122344960		3	12.1	.346	.771	false(reach)	212	107	4389982208		3	8.56	.554	58.6	1.27	36.1	9.90	timeout	904	867	2549751808		9.12	792	852	28.8	787	786	24.3	756	780	781	timeout	1000	967	4215369728
elevator_spec2_product18_false-unreach-call.cil.c	false(reach)	18.9	10.4	584937472		3	1.78	.023	.019	false(reach)	91.4	46.1	1749454848		3	3.20	.004	.004	.118	17.6	3.94	false(reach)	157	128	1778364416		11.7	84.4	106	10.5	82.9	82.5	12.8	67.0	79.8	80.0	false(reach)	103	76.8	1755901952		6	19.7	13.1	46.2	10.2	12.1	11.9	4.84	5.91	11.2	14.8	0	10.8
elevator_spec2_product20_false-unreach-call.cil.c	false(reach)	18.9	10.2	662130688		3	1.71	.012	.011	false(reach)	104	52.2	1808683008		3	3.80	.006	14.1	.024	19.5	5.11	false(reach)	375	339	2130632704		12.9	287	315	13.4	285	284	18.1	262	280	281	false(reach)	101	74.8	1813147648		6	19.0	14.1	45.0	10.4	13.3	13.1	4.55	7.35	12.2	12.3	0	11.9
elevator_spec2_product22_false-unreach-call.cil.c	false(reach)	19.4	10.5	564174848		3	1.63	.004	.007	false(reach)	111	56.0	1911672832		3	3.13	.004	.006	.013	20.8	5.27	false(reach)	454	419	2441936896		17.8	352	388	15.8	350	349	29.8	314	344	344	false(reach)	164	128	2236174336		6	23.3	20.5	92.0	16.7	19.1	18.8	6.25	11.3	18.0	44.5	0	17.6
elevator_spec2_product24_false-unreach-call.cil.c	false(reach)	19.9	10.8	617963520		3	2.12	.004	.024	false(reach)	121	61.0	1989627904		3	4.12	.006	22.4	.151	18.3	6.37	false(reach)	270	237	2468900864		17.5	177	207	14.5	175	175	22.5	148	170	170	false(reach)	200	167	2276114432		6	26.3	23.0	127	15.6	21.9	21.6	5.32	15.1	20.8	76.7	0	20.5
elevator_spec2_product26_false-unreach-call.cil.c	false(reach)	19.1	10.2	517488640		3	1.82	.003	.009	false(reach)	102	51.2	1775403008		3	3.41	.016	13.7	.007	21.0	3.46	false(reach)	321	287	2112299008		16.0	235	260	11.6	233	232	23.3	204	227	228	false(reach)	102	74.7	1817018368		6	20.1	13.1	44.1	11.4	12.1	11.9	4.87	5.91	11.1	11.5	0	10.8
elevator_spec2_product28_false-unreach-call.cil.c	false(reach)	20.0	10.8	558333952		3	2.18	.015	.018	false(reach)	104	52.5	1802739712		3	4.03	.012	15.4	.037	19.8	4.34	false(reach)	166	135	2006573056		15.2	86.0	109	11.1	84.3	83.9	14.8	65.8	80.5	80.7	false(reach)	112	85.8	1864863744		6	22.1	16.9	52.5	10.4	15.5	15.2	5.20	8.84	14.4	16.7	0	14.1
elevator_spec2_product30_false-unreach-call.cil.c	false(reach)	18.2	9.98	596725760		3	1.52	.003	.006	false(reach)	112	56.6	2029924352		3	3.45	.005	.005	.023	22.1	6.75	false(reach)	238	206	2397917184		15.9	152	177	13.4	150	150	17.0	130	147	147	false(reach)	151	114	2345308160		6	26.0	20.7	75.2	16.7	19.2	18.8	7.43	10.0	17.9	25.5	0	17.5
elevator_spec2_product32_false-unreach-call.cil.c	false(reach)	18.7	10.4	582004736		3	1.55	.004	.007	false(reach)	135	68.1	2224668672		3	2.71	.005	.004	.028	20.3	6.25	false(reach)	891	858	2543235072		16.3	791	828	18.0	789	788	22.0	761	783	784	false(reach)	139	106	2216226816		6	25.2	19.3	67.4	16.3	17.8	17.4	6.35	9.93	16.7	19.7	0	16.3
elevator_spec2_productSimulator_false-unreach-call.cil.c	false(reach)	42.7	24.5	1226792960		3	10.8	.346	.734	false(reach)	199	100	4146581504		3	8.76	.537	.005	1.83	33.2	12.4	timeout	905	872	2794962944		11.4	786	854	34.6	781	780	27.3	747	775	775	timeout	1000	964	4726034432
elevator_spec3_product03_false-unreach-call.cil.c	false(reach)	18.9	10.3	578674688		1	1.75	.006		false(reach)	65.3	33.1	1204330496		1	5.00	.029	6.49				false(reach)	79.1	55.3	1550118912		25.1	12.5	19.9	3.71	12.0	11.9	9.95	.00	9.95		false(reach)	60.8	41.5	1434570752		0	22.9	.553	8.70	4.43	.081	.00	.00	.00	.00	.046
elevator_spec3_product11_false-unreach-call.cil.c	false(reach)	19.5	10.7	617324544		1	1.84	.005		false(reach)	66.9	33.8	1138761728		1	5.23	.048	6.39				false(reach)	80.1	56.0	1576194048		25.0	12.5	20.1	4.03	12.0	11.8	9.81	.00	9.81		false(reach)	58.2	39.4	1483419648		0	19.7	.512	9.77	4.91	.101	.001	.00	.00	.00	.041
elevator_spec3_product19_false-unreach-call.cil.c	false(reach)	19.5	10.6	602222592		1	1.64	.004		false(reach)	65.4	33.1	1204404224		1	4.49	.047	6.68				false(reach)	76.0	53.5	1514172416		23.4	12.2	19.5	3.17	11.6	11.5	9.56	.00	9.56		false(reach)	60.9	40.9	1453318144		0	22.6	.437	8.20	3.99	.088	.002	.00	.00	.00	.051
elevator_spec3_product20_false-unreach-call.cil.c	false(reach)	20.3	11.5	742240256		1	1.81	.006		false(reach)	87.7	44.3	1367019520		1	3.43	.021	12.2				false(reach)	101	73.4	1922146304		33.5	15.9	27.9	6.50	15.2	15.0	12.5	.00	12.5		false(reach)	78.5	56.8	1885433856		0	30.8	.761	14.0	7.19	.157	.001	.00	.00	.00	.107
elevator_spec3_product23_false-unreach-call.cil.c	false(reach)	19.2	10.8	681218048		1	1.60	.006		false(reach)	70.3	35.5	1966206976		1	3.93	.048	8.86				false(reach)	94.9	68.5	1851691008		32.3	14.8	24.4	4.85	14.1	14.0	11.7	.00	11.7		false(reach)	80.3	55.4	1776787456		0	32.4	.645	10.9	5.46	.142	.002	.00	.00	.00	.054
elevator_spec3_product24_false-unreach-call.cil.c	false(reach)	22.6	13.1	786300928		1	1.97	.007		false(reach)	90.1	45.5	1595469824		1	3.02	.008	13.2				false(reach)	114	86.6	2356920320		35.9	18.0	36.0	9.87	17.1	16.8	13.8	.00	13.8		false(reach)	93.9	69.4	2289106944		0	37.3	.951	17.0	9.50	.175	.00	.00	.00	.00	.085
elevator_spec3_product27_false-unreach-call.cil.c	false(reach)	19.6	10.8	604442624		1	1.72	.005		false(reach)	74.3	37.6	1299415040		1	3.28	.019	10.2				false(reach)	80.6	57.6	1607340032		26.1	13.3	20.8	4.12	12.9	12.8	10.7	.00	10.7		false(reach)	64.9	44.8	1536434176		0	23.1	.820	11.3	5.76	.077	.001	.00	.00	.00	.070
elevator_spec3_product28_false-unreach-call.cil.c	false(reach)	21.2	12.2	776503296		1	1.59	.006		false(reach)	88.6	44.8	1385459712		1	3.48	.015	.005				false(reach)	107	78.0	1983385600		36.0	15.8	28.9	6.11	15.1	14.9	12.3	.00	12.3		false(reach)	89.2	62.7	1883152384		0	35.7	.791	13.8	7.04	.147	.001	.00	.00	.00	.058
elevator_spec3_product31_false-unreach-call.cil.c	false(reach)	19.1	10.8	695152640		1	1.57	.007		false(reach)	92.2	46.7	1491357696		1	3.15	.022	14.2				false(reach)	99.8	72.0	1866571776		34.5	15.3	26.0	5.52	14.6	14.4	12.1	.00	12.1		false(reach)	80.2	56.3	1805094912		0	34.0	.646	10.6	5.22	.169	.002	.00	.00	.00	.065
elevator_spec3_product32_false-unreach-call.cil.c	false(reach)	21.5	12.6	780713984		1	1.50	.007		false(reach)	98.9	49.9	1598164992		1	3.56	.032	16.4				false(reach)	124	94.1	2406051840		41.1	18.6	36.7	10.0	17.8	17.6	14.6	.00	14.6		false(reach)	102	75.3	2294702080		0	40.3	1.15	19.2	10.0	.212	.001	.00	.00	.00	.109
elevator_spec3_productSimulator_false-unreach-call.cil.c	timeout	1000	970	2446704640						timeout	1000	501	6017011712									timeout	1000	961	5281808384												timeout	1000	968	5093507072
elevator_spec9_product26_false-unreach-call.cil.c	false(reach)	19.4	10.4	599359488		3	1.89	.015	.017	false(reach)	100	50.5	1824288768		3	3.19	.005	14.3	.020	16.9	4.30	false(reach)	202	167	1970135040		12.7	117	143	11.9	115	115	15.7	95.7	111	112	false(reach)	106	78.1	1798053888		6	19.3	15.7	48.0	10.6	14.1	13.9	5.21	7.63	13.1	13.5	0	12.9
elevator_spec9_product28_false-unreach-call.cil.c	false(reach)	19.4	10.6	541548544		3	1.97	.004	.007	false(reach)	108	54.5	1867890688		3	4.02	.004	17.6	.030	16.9	4.34	timeout	903	871	1715810304		5.74	834	861	12.3	832	831	20.9	806	827	828	false(reach)	109	81.5	1872302080		6	22.6	13.5	47.8	11.2	12.5	12.2	4.88	6.20	11.5	15.0	0	11.1
elevator_spec9_product30_false-unreach-call.cil.c	false(reach)	19.0	10.5	646529024		3	1.62	.005	.023	false(reach)	115	57.7	1903616000		3	3.44	.005	20.2	.043	19.8	5.43	false(reach)	461	428	2377273344		16.6	365	398	15.6	363	362	22.4	336	358	359	false(reach)	203	170	2345484288		6	24.6	15.8	132	16.7	14.6	14.3	5.92	6.98	13.2	87.6	0	12.9
elevator_spec9_product32_false-unreach-call.cil.c	false(reach)	20.3	11.1	626827264		3	2.12	.003	.028	false(reach)	120	60.6	2287783936		3	3.14	.006	.004	.034	18.0	6.53	timeout	904	871	1742155776		3.63	828	862	17.4	826	826	18.0	804	822	822	false(reach)	157	126	2402107392		6	25.9	20.6	87.1	15.1	19.2	18.9	7.58	10.2	18.2	39.6	0	17.8
elevator_spec9_productSimulator_false-unreach-call.cil.c	false(reach)	43.9	25.4	1171914752		3	10.8	.465	.773	false(reach)	218	110	3793092608		3	9.37	.575	60.6	1.28	41.6	8.81	timeout	904	871	2564108288		11.3	801	854	25.6	796	795	20.3	771	791	791	timeout	1000	965	4426334208
elevator_spec13_product21_true-unreach-call.cil.c	timeout	903	881	2213449728		6524	82.5	.864	368	timeout	902	452	5637623808		1	4.58	.00	369	.048			timeout	903	876	2263826432		165	691	705	7.32	690	690	40.8	623	664	678	timeout	903	875	1996800000		219	821	2.44	39.0	18.5	.581	.036	.00	.00	1.55	3.48	150
elevator_spec13_product22_true-unreach-call.cil.c	timeout	903	882	3685228544		6616	86.1	.951	349	timeout	902	452	5539610624		1	3.30	.001	364	.022			timeout	903	869	3727761408		447	367	415	26.6	364	363	105	228	333	334	timeout	903	874	2553913344		115	794	3.71	58.3	30.3	.785	.041	.00	.00	.810	1.91	100
elevator_spec13_product23_true-unreach-call.cil.c	timeout	903	879	2052317184		8054	83.5	.973	355	timeout	902	452	5578674176		1	4.20	.009	368	.049			true	270	248	2065207296		168	61.9	75.2	6.32	60.9	60.7	46.5	4.33	50.9	47.9	timeout	904	876	2035798016		163	819	2.54	40.8	20.4	.604	.044	.00	.00	1.25	2.46	119
elevator_spec13_product24_true-unreach-call.cil.c	timeout	903	880	2467176448		7923	79.8	1.02	377	timeout	902	452	5798019072		1	2.64	.00	.004	.030			timeout	903	868	3073339392		244	573	618	22.4	570	570	101	446	547	544	timeout	903	874	2500902912		165	794	3.26	60.6	30.2	.769	.036	.00	.00	1.25	3.11	102
elevator_spec13_product29_true-unreach-call.cil.c	timeout	903	880	2390376448		6703	86.5	.959	337	timeout	902	452	5669298176		1	4.88	.001	368	.058			timeout	902	874	1938399232		163	694	705	5.70	693	693	39.6	644	683	682	timeout	903	876	2248630272		179	803	2.08	62.4	17.2	.453	.050	.00	.00	1.35	30.7	148
elevator_spec13_product30_true-unreach-call.cil.c	timeout	903	879	2586058752		6552	85.3	.850	351	timeout	903	452	5617618944		1	2.62	.00	368	.021			timeout	903	870	2915819520		261	562	602	20.2	560	559	82.6	456	539	536	timeout	902	877	1704562688		2285	107	1.02	764	10.8	.205	.027	.00	.00	58.7	719	101
elevator_spec13_product31_true-unreach-call.cil.c	timeout	903	880	1981317120		7993	81.5	.946	375	timeout	902	452	5775073280		1	4.20	.00	.008	.044			timeout	903	874	2335088640		181	669	687	9.18	668	668	53.4	603	656	655	timeout	903	873	1894981632		2134	444	1.51	420	13.1	.409	.050	.00	.00	35.3	379	141
elevator_spec13_product32_true-unreach-call.cil.c	timeout	903	880	2197090304		7970	80.5	.929	364	timeout	902	452	5680766976		1	3.14	.00	369	.026			timeout	903	873	2621403136		192	650	676	13.1	648	647	61.0	573	634	630	timeout	903	874	2681786368		103	795	3.91	60.0	31.2	.775	.028	.00	.00	.627	1.59	92
elevator_spec13_productSimulator_true-unreach-call.cil.c	timeout	1000	889	7717310464						timeout	903	452	6277881856		1	18.8	1.45	.005	2.77			timeout	904	863	4525625344		502	262	351	45.8	257	256	144	73.3	217	208	timeout	904	868	3129987072		1693	522	3.85	321	33.1	.845	.019	.00	.00	27.6	247	152
elevator_spec14_product03_true-unreach-call.cil.c	true	19.2	10.4	559599616		9	2.98	.001	.103	true	81.2	41.1	1492500480		1	5.08	.00	9.72	.051	7.20	7.81	true	83.8	64.9	1427890176		11.8	35.7	48.2	6.30	34.9	34.7	20.1	11.1	31.2	19.4	true	50.5	33.8	1345335296		3	16.1	.641	13.3	5.31	.132	.002	.00	.00	.022	3.21	1
elevator_spec14_product11_true-unreach-call.cil.c	true	20.5	11.0	547164160		9	3.19	.001	.102	true	77.2	39.0	1482330112		1	4.00	.00	9.67	.037	8.67	4.63	true	75.0	55.5	1391976448		12.8	26.7	37.6	5.21	26.1	25.9	16.5	6.42	22.9	12.7	true	53.8	37.7	1363283968		3	19.7	.565	13.2	4.68	.099	.001	.00	.00	.034	3.43	1
elevator_spec14_product19_true-unreach-call.cil.c	true	20.6	11.0	592723968		9	3.40	.003	.105	true	76.3	38.5	1474605056		1	4.68	.00	9.03	.026	9.87	5.32	true	63.3	47.2	1398169600		11.6	20.8	31.0	5.36	20.2	20.0	15.0	2.12	17.1	8.38	true	52.0	36.4	1367416832		3	17.9	.762	13.9	5.86	.087	.00	.00	.00	.020	3.58	1
elevator_spec14_product23_true-unreach-call.cil.c	true	21.9	12.0	684265472		12	3.78	.00	.143	true	107	53.8	1993842688		2	3.46	.00	18.1	.183	12.9	9.01	true	91.8	69.9	1510506496		17.6	33.2	47.4	7.03	32.3	32.0	20.4	8.36	28.8	16.8	true	102	81.9	1740804096		6	33.4	.953	43.7	7.15	.160	.002	.00	.00	.052	29.7	1
elevator_spec14_product27_true-unreach-call.cil.c	true	21.6	11.8	598888448		9	3.50	.002	.100	true	82.5	41.8	1533108224		1	3.88	.001	12.2	.037	7.14	4.93	true	73.0	54.1	1470992384		14.1	23.6	35.1	5.65	23.0	22.8	17.3	2.63	19.9	9.90	true	56.4	39.5	1413304320		3	18.8	.695	16.0	5.79	.117	.002	.00	.00	.021	4.14	1
elevator_spec14_product31_true-unreach-call.cil.c	true	23.4	12.8	715075584		12	3.88	.002	.192	true	129	64.8	2473746432		2	4.45	.001	24.5	.043	14.2	8.73	true	285	259	1830711296		20.0	214	233	10.6	213	212	29.8	178	207	190	true	83.7	63.6	1555394560		3	24.0	.711	34.8	6.62	.103	.001	.00	.00	.023	21.4	1
elevator_spec1_product01_true-unreach-call.cil.c	true	18.0	9.54	479035392		9	2.67	.001	.078	true	207	104	4641976320		9	4.94	.002	62.3	.101	22.1	61.6	true	541	512	1748566016		11.3	463	495	16.2	461	460	40.3	412	453	453	true	91.8	70.4	1259081728		14	19.3	8.08	46.6	5.08	7.66	7.50	4.28	2.34	6.92	28.8	2	6.64
elevator_spec1_product03_true-unreach-call.cil.c	true	20.2	10.6	494444544		9	3.64	.001	.082	true	283	142	4728242176		9	5.23	.00	97.7	.117	20.7	101	timeout	903	874	1583476736		17.0	834	852	7.31	832	832	32.2	793	825	826	true	97.0	75.1	1313669120		13	22.4	9.34	48.1	6.25	8.93	8.83	5.35	2.37	8.05	27.1	1	7.74
elevator_spec1_product09_true-unreach-call.cil.c	true	19.0	9.99	521965568		9	3.00	.002	.112	true	227	114	4608782336		9	4.89	.002	70.8	.092	21.2	70.8	timeout	902	873	1425219584		11.5	842	857	5.98	840	840	24.4	811	835	836	true	104	81.2	1321299968		14	24.7	9.47	51.8	5.74	8.76	8.62	4.83	2.71	7.96	31.5	1	7.56
elevator_spec1_product11_true-unreach-call.cil.c	true	18.7	9.93	509526016		9	2.96	.00	.062	true	267	134	4704636928		9	5.29	.020	.005	.131	21.8	89.7	timeout	903	871	1994153984		15.5	817	851	16.0	815	814	48.6	757	805	806	true	97.4	75.7	1342328832		13	21.5	9.42	49.7	6.08	8.24	8.10	5.16	1.74	7.33	29.0	1	6.95
elevator_spec1_product17_true-unreach-call.cil.c	true	19.3	10.2	506802176		9	3.10	.00	.096	true	220	111	4434677760		9	5.08	.00	64.6	.119	22.4	66.2	timeout	904	871	1803423744		17.2	820	849	12.4	818	817	51.2	757	808	809	true	74.2	52.8	1226637312		9	15.3	7.71	33.0	5.84	7.18	7.08	4.10	1.94	6.21	14.1	1	6.05
elevator_spec1_product19_true-unreach-call.cil.c	true	19.4	10.3	495075328		9	3.24	.001	.085	true	308	155	4814708736		9	5.14	.00	111	.116	20.7	111	true	364	337	1393152000		8.90	303	322	9.55	301	301	22.0	275	297	297	true	152	129	1385844736		20	32.7	10.5	91.6	6.60	9.76	9.56	5.18	3.24	9.42	68.7	2	8.45
elevator_spec1_product21_true-unreach-call.cil.c	true	18.6	9.92	524328960		9	2.83	.00	.065	true	540	271	5255311360		9	4.42	.012	222	.103	25.4	222	timeout	903	871	1555607552		6.73	834	859	11.9	831	831	26.8	799	826	827	timeout	903	877	1868283904		21	44.5	12.8	827	8.64	12.0	11.8	7.63	2.92	12.0	798	1	10.6
elevator_spec1_product23_true-unreach-call.cil.c	true	22.5	11.8	604364800		9	4.13	.001	.116	true	655	328	5547192320		9	4.57	.001	269	.141	28.6	274	timeout	903	872	1337769984		7.19	837	860	11.0	836	835	23.8	807	831	831	timeout	903	878	2147254272		34	127	18.1	746	10.4	16.7	16.4	9.82	4.94	18.5	709	1	14.8
elevator_spec1_product25_true-unreach-call.cil.c	true	19.2	10.1	545824768		9	2.94	.00	.085	true	269	135	4712402944		9	4.99	.002	89.2	.121	21.6	93.0	timeout	902	876	1184313344		9.23	851	862	4.76	850	850	14.7	832	846	847	true	77.3	55.3	1234993152		9	16.6	7.56	34.1	6.22	6.99	6.87	4.39	1.53	6.11	15.3	1	5.95
elevator_spec1_product27_true-unreach-call.cil.c	true	20.7	10.8	506474496		9	3.30	.00	.090	true	350	176	4964069376		9	5.01	.001	127	.127	20.4	134	timeout	902	871	1682411520		15.4	830	851	9.65	828	828	36.1	785	821	822	true	130	107	1400811520		18	23.6	10.6	78.2	7.26	9.92	9.71	6.02	2.52	8.94	54.5	2	8.55
elevator_spec1_product29_true-unreach-call.cil.c	true	18.6	9.96	520687616		9	2.96	.003	.066	true	624	313	5390364672		9	4.41	.001	261	.101	25.3	262	timeout	903	872	1487298560		6.13	836	861	12.0	834	833	30.9	797	828	828	timeout	903	878	2124349440		21	47.6	14.1	826	9.28	13.3	13.1	7.20	4.46	12.6	795	1	11.7
elevator_spec1_product31_true-unreach-call.cil.c	true	20.2	10.7	595464192		9	3.54	.002	.097	true	748	375	5889708032		9	4.68	.001	308	.111	26.3	323	timeout	903	870	1778200576		10.1	827	855	13.0	824	824	43.1	774	817	818	timeout	903	877	2343096320		27	80.1	18.6	792	9.55	17.7	17.5	11.3	4.60	19.8	757	1	15.9
elevator_spec2_product01_true-unreach-call.cil.c	true	17.2	9.10	520388608		5	2.65	.001	.033	true	96.2	48.5	1789358080		5	3.40	.00	16.9	.051	16.1	12.2	true	125	95.6	1390755840		16.3	60.1	74.6	6.40	58.9	58.6	20.8	33.9	54.6	54.9	true	166	146	1455140864		16	63.8	12.1	76.9	5.53	11.5	11.3	6.09	4.05	14.3	54.0	1	10.2
elevator_spec2_product03_true-unreach-call.cil.c	true	17.8	9.45	505335808		5	2.55	.00	.019	true	112	56.8	2060115968		5	4.86	.002	19.8	.071	17.7	19.9	true	129	103	1483513856		13.6	68.8	85.2	6.84	67.2	66.9	21.3	41.3	62.5	62.8	true	129	107	1348419584		11	45.3	13.6	56.8	5.64	13.0	12.9	5.42	6.24	13.8	31.9	1	11.7
elevator_spec2_product09_true-unreach-call.cil.c	true	16.7	8.92	475648000		5	2.11	.00	.025	true	105	52.8	1961807872		5	4.12	.001	.004	.038	15.3	19.0	true	161	134	1559736320		25.3	87.6	103	6.27	86.0	85.6	33.9	45.5	79.4	79.7	true	117	96.0	1341280256		11	41.1	11.8	50.3	6.22	11.2	11.0	5.32	4.48	11.2	27.1	1	9.82
elevator_spec2_product11_true-unreach-call.cil.c	true	17.3	9.11	547913728		5	2.24	.00	.021	true	114	57.3	2312527872		5	4.56	.00	21.2	.059	18.7	19.8	timeout	902	872	1731936256		22.3	828	845	7.00	827	826	34.3	783	817	821	true	132	110	1367408640		11	44.5	15.5	60.8	6.86	14.8	14.6	5.69	7.70	15.6	33.0	1	13.4
elevator_spec2_product17_true-unreach-call.cil.c	true	16.9	8.96	521674752		5	2.13	.00	.013	true	102	51.3	1984905216		5	4.42	.002	17.9	.056	15.5	14.4	true	161	134	1613725696		24.8	89.9	105	5.88	88.7	87.9	28.5	53.8	82.3	82.6	true	123	101	1356148736		11	41.4	12.1	55.5	6.66	11.5	11.4	5.17	5.12	11.9	30.7	1	10.3
elevator_spec2_product19_true-unreach-call.cil.c	true	18.1	9.54	491995136		5	2.49	.006	.037	true	112	56.7	2776367104		5	4.64	.00	.015	.051	13.1	17.9	true	115	89.4	1427304448		17.9	52.8	66.7	5.58	51.8	51.5	22.7	24.3	46.9	47.1	true	188	167	1599361024		16	71.1	14.2	90.8	6.74	13.6	13.5	6.54	5.62	15.9	63.9	1	12.2
elevator_spec2_product21_true-unreach-call.cil.c	true	19.0	10.1	459448320		5	2.53	.001	.027	true	137	68.9	2540482560		5	3.51	.001	.004	.039	17.4	28.6	timeout	903	871	1857015808		23.3	814	843	11.3	812	812	40.6	762	803	805	timeout	903	878	2276995072		8	20.7	13.0	853	8.42	12.2	12.0	6.06	4.94	11.5	824	0	11.0
elevator_spec2_product23_true-unreach-call.cil.c	true	18.5	9.91	526700544		5	2.63	.001	.026	true	146	73.5	2770616320		5	4.25	.002	34.9	.071	19.7	29.5	true	774	740	1894404096		20.9	684	714	13.5	682	681	44.9	628	673	674	true	288	264	1620615168		11	64.8	19.0	195	9.38	18.2	18.0	8.62	8.05	20.1	160	1	16.7
elevator_spec2_product25_true-unreach-call.cil.c	true	16.6	8.87	489111552		5	2.03	.00	.036	true	111	56.1	1908940800		5	4.60	.00	.004	.053	18.9	18.3	true	151	124	1509502976		16.4	87.7	103	6.12	86.3	86.0	22.3	59.1	81.4	81.7	true	129	107	1372016640		11	43.3	14.4	59.0	7.27	13.9	13.7	5.63	6.89	14.6	31.8	1	12.6
elevator_spec2_product27_true-unreach-call.cil.c	true	18.2	9.55	544681984		5	2.37	.00	.044	true	118	59.4	2206023680		5	4.79	.001	23.4	.060	18.2	19.6	true	135	105	1593712640		19.7	64.4	80.2	7.01	63.1	62.8	25.1	32.9	58.1	58.3	true	145	122	1441841152		11	51.2	14.7	65.6	6.95	14.1	13.9	6.31	6.08	14.2	38.2	1	12.4
elevator_spec2_product29_true-unreach-call.cil.c	true	17.0	9.11	511938560		5	2.09	.00	.021	true	172	86.5	3350327296		5	4.32	.002	48.5	.048	17.6	43.0	timeout	903	874	1638486016		8.29	833	860	13.3	831	830	37.2	786	824	825	timeout	903	878	1860743168		17	68.1	21.5	805	10.0	20.6	20.3	8.36	10.6	22.9	765	0	19.0
elevator_spec2_product31_true-unreach-call.cil.c	true	18.0	9.48	526667776		5	2.46	.001	.055	true	185	93.2	3612209152		5	4.34	.001	.007	.052	19.2	49.1	timeout	903	875	1503956992		5.26	841	864	10.7	840	839	24.8	810	835	835	true	437	412	1797488640		16	105	25.8	302	9.71	24.8	24.5	10.3	12.6	31.0	258	1	23.0
elevator_spec3_product01_true-unreach-call.cil.c	true	21.3	11.5	605335552		12	3.64	.00	.162	true	87.6	44.5	1481785344		1	4.91	.001	10.6	.046	8.09	7.79	true	145	128	1438277632		16.7	94.4	107	6.70	93.6	93.4	28.1	60.4	88.5	68.4	true	832	808	2413051904		40	449	.755	354	7.96	.192	.003	.00	.00	26.5	336	1
elevator_spec3_product09_true-unreach-call.cil.c	true	22.0	11.8	605933568		12	3.88	.001	.199	true	89.6	45.3	1519538176		1	5.35	.008	10.9	.051	9.01	7.32	true	82.1	62.7	1383698432		19.2	29.3	38.7	4.89	28.6	28.5	19.0	6.00	25.0	11.0	timeout	903	881	2678587392		41	492	.979	384	6.97	.185	.001	.00	.00	25.4	368	0
elevator_spec3_product17_true-unreach-call.cil.c	true	20.5	11.1	589606912		12	3.43	.001	.126	true	87.3	44.3	1469468672		1	4.75	.00	11.4	.017	7.26	6.66	true	147	127	1424769024		18.7	88.7	104	7.84	87.8	87.6	33.7	47.8	81.6	57.4	timeout	904	881	2540867584		45	458	.884	418	8.20	.199	.002	.00	.00	23.8	400	0
elevator_spec3_product18_true-unreach-call.cil.c	true	22.6	12.6	719413248		12	3.84	.001	.165	true	97.9	49.4	1732304896		1	3.27	.00	14.9	.042	12.4	3.55	true	132	107	1695625216		28.6	55.5	72.9	8.81	54.3	54.1	25.1	24.0	49.1	31.1	timeout	903	877	3056513024		32	567	1.49	305	12.3	.265	.003	.00	.00	16.3	280	0
elevator_spec3_product21_true-unreach-call.cil.c	true	23.8	13.3	744194048		12	4.19	.00	.127	true	94.2	47.5	1561001984		1	4.12	.00	.005	.024	11.3	2.96	true	125	99.9	1608118272		28.1	51.8	66.9	8.26	50.6	50.4	28.1	17.8	45.9	26.4	timeout	904	880	2379870208		15	320	1.12	555	9.02	.166	.012	.00	.00	3.92	538	0
elevator_spec3_product22_true-unreach-call.cil.c	true	23.9	13.7	753270784		12	3.81	.001	.174	true	130	65.8	2323156992		1	3.04	.00	26.7	.030	14.5	2.72	true	229	204	2128195584		33.6	136	164	15.5	135	134	40.9	86.9	128	102	timeout	904	877	2885001216		17	542	1.69	330	15.5	.301	.003	.00	.00	6.79	300	0
elevator_spec3_product25_true-unreach-call.cil.c	true	21.9	11.9	595304448		12	3.61	.004	.196	true	82.0	41.4	1488314368		1	4.55	.001	9.78	.037	8.42	6.40	true	133	112	1443622912		20.1	72.9	86.5	6.89	72.2	71.9	25.8	41.2	67.0	48.6	timeout	903	881	2976907264		39	523	1.07	352	8.70	.196	.003	.00	.00	29.0	333	0
elevator_spec3_product26_true-unreach-call.cil.c	true	22.3	12.6	754266112		12	3.41	.00	.125	true	96.7	48.8	1833664512		1	3.42	.001	15.0	.008	11.8	3.24	true	212	184	1867034624		27.3	129	152	11.6	128	127	36.0	84.9	121	96.3	timeout	904	878	3054411776		28	628	1.62	245	12.6	.285	.005	.00	.00	9.57	220	0
elevator_spec3_product29_true-unreach-call.cil.c	true	23.1	12.6	723816448		12	3.79	.00	.166	true	102	51.6	1738919936		1	3.65	.00	16.8	.036	10.4	2.28	true	182	159	1733185536		30.4	107	123	7.97	106	106	31.5	69.5	101	78.5	timeout	904	879	2448330752		15	356	.894	518	8.20	.159	.003	.00	.00	4.01	502	0
elevator_spec3_product30_true-unreach-call.cil.c	true	25.6	14.5	782188544		12	3.94	.00	.206	true	111	56.2	3356172288		1	3.69	.001	19.1	.030	14.2	2.66	true	287	262	2101661696		34.2	194	222	15.8	193	192	41.5	144	186	158	timeout	903	876	2707369984		12	448	1.57	422	14.3	.353	.004	.00	.00	4.76	395	0
elevator_spec9_product09_true-unreach-call.cil.c	true	17.3	9.18	483938304		5	2.27	.00	.038	true	104	52.7	1908318208		5	4.05	.00	17.2	.256	18.0	15.6	timeout	903	874	1195073536		6.61	848	862	7.09	847	847	14.7	828	843	844	true	125	103	1346899968		11	40.9	12.7	57.4	6.87	12.1	11.9	5.46	5.28	12.4	32.2	1	10.8
elevator_spec9_product11_true-unreach-call.cil.c	true	17.9	9.56	497926144		5	2.45	.002	.021	true	118	59.3	2037243904		5	4.66	.00	19.9	.071	18.5	19.2	true	172	144	1599254528		24.3	95.9	115	6.98	94.2	93.6	29.5	58.3	87.8	88.3	true	191	169	1553440768		16	75.7	17.2	88.7	6.94	16.5	16.4	6.34	8.69	19.0	58.9	1	15.1
elevator_spec9_product25_true-unreach-call.cil.c	true	17.8	9.43	491139072		5	2.30	.00	.031	true	107	54.1	2044547072		5	4.45	.001	.004	.072	18.9	15.2	true	131	105	1510785024		15.6	70.7	84.4	7.12	69.6	69.3	22.6	42.4	65.0	65.2	true	122	102	1331822592		11	41.9	13.6	54.7	6.31	13.0	12.9	5.24	6.52	13.9	28.9	1	11.8
elevator_spec9_product27_true-unreach-call.cil.c	true	17.4	9.30	426369024		5	2.23	.00	.026	true	117	59.1	2160078848		5	4.45	.00	.004	.026	17.6	21.3	timeout	903	876	1176281088		6.82	850	864	6.72	849	849	11.5	834	845	846	true	133	111	1442009088		11	46.5	13.8	60.1	6.80	13.2	13.0	5.71	6.13	13.6	33.6	1	11.9
elevator_spec9_product29_true-unreach-call.cil.c	true	18.3	9.81	540532736		5	2.41	.001	.019	true	165	82.8	3231870976		5	4.39	.00	.005	.066	17.8	40.1	true	250	222	1909317632		17.4	175	200	11.6	173	172	33.9	133	166	167	true	692	668	1832038400		11	58.4	18.9	605	8.84	18.0	17.8	7.86	8.76	20.6	570	1	16.6
elevator_spec9_product31_true-unreach-call.cil.c	true	19.0	10.1	517754880		5	2.69	.00	.032	true	159	80.1	3115343872		5	4.55	.001	.004	.050	20.9	34.6	timeout	903	872	1509376000		11.7	833	856	10.3	831	830	32.7	790	823	825	true	768	743	2022514688		16	108	24.6	630	9.55	23.6	23.4	9.88	12.1	29.0	587	1	22.0
email_spec0_product16_false-unreach-call.cil.c	timeout	1000	983	3192164352						timeout	1000	501	7066873856									timeout	1000	984	2813186048												timeout	1000	982	2605023232
email_spec0_product21_false-unreach-call.cil.c	timeout	1000	981	3488739328						timeout	1000	501	6824329216									timeout	902	881	1118916608		2.06	866	874	3.66	865	865	18.0	832	850	848	timeout	1000	981	2731970560
email_spec0_product22_false-unreach-call.cil.c	timeout	1000	982	3163889664						timeout	1000	501	6374416384									timeout	1000	981	2326888448												timeout	1000	984	2507853824
email_spec0_product26_false-unreach-call.cil.c	timeout	1000	981	3516071936						timeout	1000	501	7497871360									timeout	902	880	1129320448		2.63	864	872	3.79	863	863	23.1	827	850	840	timeout	1000	981	2894073856
email_spec0_product31_false-unreach-call.cil.c	timeout	1000	982	3559690240						timeout	1000	501	6159773696									timeout	1000	982	3001856000												timeout	1000	981	2629427200
email_spec0_product33_false-unreach-call.cil.c	timeout	1000	982	3526479872						timeout	1000	501	7273533440									timeout	1000	981	2438598656												timeout	1000	982	2653659136
email_spec0_product34_false-unreach-call.cil.c	timeout	1000	983	3924529152						timeout	1000	501	7245660160									timeout	902	880	1269035008		1.92	865	873	3.75	865	865	17.7	832	850	847	timeout	1000	980	2898198528
email_spec0_product35_false-unreach-call.cil.c	timeout	1000	980	3671023616						timeout	1000	501	7610630144									timeout	1000	979	2728927232												timeout	1000	980	2963910656
email_spec0_productSimulator_false-unreach-call.cil.c	timeout	1000	971	4982878208						timeout	1000	501	7968370688									timeout	902	873	3512569856		2.78	810	865	25.7	807	806	193	542	735	554	timeout	1000	964	5297926144
email_spec11_product15_false-unreach-call.cil.c	timeout	1000	985	3118604288						timeout	1000	501	6339543040									timeout	1000	981	2535182336												timeout	1000	982	2565541888
email_spec11_product20_false-unreach-call.cil.c	timeout	1000	982	3604512768						timeout	1000	501	5978796032									timeout	902	883	1219780608		2.03	869	876	3.09	869	869	16.9	826	842	854	timeout	1000	981	2678542336
email_spec11_product22_false-unreach-call.cil.c	timeout	1000	986	3269042176						timeout	1000	501	5854683136									timeout	1000	980	2788524032												timeout	1000	983	2518106112
email_spec11_product26_false-unreach-call.cil.c	timeout	1000	981	4022915072						timeout	1000	501	7477604352									timeout	1000	979	2599546880												timeout	1000	982	2974978048
email_spec11_product30_false-unreach-call.cil.c	timeout	1000	981	3143659520						timeout	1000	501	6282342400									timeout	1000	982	2690072576												timeout	1000	983	2514948096
email_spec11_product32_false-unreach-call.cil.c	timeout	1000	980	3644846080						timeout	1000	501	7353704448									timeout	902	881	1027735552		1.33	868	875	3.25	868	867	9.11	849	858	860	timeout	1000	979	2947510272
email_spec11_product33_false-unreach-call.cil.c	timeout	1000	984	3217960960						timeout	1000	501	7316959232									timeout	1000	980	2631331840												timeout	1000	983	2627325952
email_spec11_product35_false-unreach-call.cil.c	timeout	1000	980	3600535552						timeout	1000	501	7772401664									timeout	1000	978	2658217984												timeout	1000	980	2799734784
email_spec11_productSimulator_false-unreach-call.cil.c	timeout	1000	971	4929380352						timeout	1000	501	8175828992									timeout	904	873	2919591936		2.60	817	864	20.0	814	812	515	181	697	185	timeout	905	867	4661166080		6	721	4.35	68.3	32.6	.947	.035	.00	.00	32.0	3.43	0
email_spec1_product14_false-unreach-call.cil.c	unknown	159	148	2750676992		3	4.28	.564	.413	timeout	1000	734	6509584384									timeout	902	886	794234880		.393	876	881	2.50	876	876	2.02	868	870	875	unknown	185	168	2943733760		6	9.95	.367	7.33	3.04	.083	.002	.00	.00	.769	1.52	1
email_spec1_product15_false-unreach-call.cil.c	unknown	145	134	2617896960		3	3.77	.692	.215	timeout	1000	718	6148550656									timeout	1000	984	2749620224												unknown	169	154	2724945920		6	5.46	.324	5.47	2.18	.059	.001	.00	.00	.103	1.16	1
email_spec1_product16_false-unreach-call.cil.c	unknown	127	117	2618933248		3	3.90	.735	.229	timeout	1000	712	6212640768									timeout	1000	984	2729197568												unknown	160	146	2698522624		6	5.82	.248	5.40	1.82	.037	.00	.00	.00	.084	1.00	1
email_spec1_product20_false-unreach-call.cil.c	unknown	713	690	3074162688		3	5.49	2.21	.283	timeout	1000	501	6362173440									timeout	902	886	819040256		.682	876	881	2.36	876	875	2.73	867	870	874	timeout	1000	978	3146711040
email_spec1_product21_false-unreach-call.cil.c	unknown	762	738	3128766464		3	6.64	3.01	.357	timeout	1000	501	6611165184									timeout	902	881	967720960		1.17	869	875	3.21	868	868	8.19	850	858	861	timeout	1000	976	3187695616
email_spec1_product22_false-unreach-call.cil.c	unknown	169	156	2630201344		3	4.25	.729	.385	timeout	1000	694	6593449984									timeout	1000	979	3025178624												unknown	183	168	2772299776		6	6.32	.755	5.78	2.04	.096	.002	.00	.00	.230	1.29	1
email_spec1_product26_false-unreach-call.cil.c	unknown	800	776	3228188672		3	6.34	3.96	.297	timeout	1000	501	7145947136									timeout	1000	977	3306078208												timeout	1000	976	3248214016
email_spec1_product29_false-unreach-call.cil.c	unknown	169	157	2766667776		3	3.80	.524	.252	timeout	1000	729	6379610112									timeout	1000	977	3155820544												unknown	187	170	3070951424		6	10.1	.983	9.32	3.41	.059	.001	.00	.00	.506	2.32	1
email_spec1_product30_false-unreach-call.cil.c	unknown	155	144	2623008768		3	4.11	.784	.295	timeout	1000	699	6299815936									timeout	1000	981	2832674816												unknown	184	168	2739290112		6	5.36	.251	6.87	2.22	.073	.004	.00	.00	.105	1.95	1
email_spec1_product31_false-unreach-call.cil.c	unknown	145	131	2753433600		3	4.21	.673	.211	timeout	1000	685	6791446528									timeout	1000	976	3024019456												unknown	202	186	2782269440		6	5.69	.386	7.07	2.32	.087	.001	.00	.00	.283	1.89	1
email_spec1_product32_false-unreach-call.cil.c	unknown	655	632	3219218432		3	6.81	3.48	.261	timeout	1000	501	7201665024									timeout	1000	977	3280826368												timeout	1000	977	3281887232
email_spec1_product33_false-unreach-call.cil.c	unknown	174	158	2770472960		3	4.39	.967	.307	timeout	1000	676	6773972992									timeout	1000	979	2988167168												unknown	203	187	2799403008		6	5.33	.297	7.61	2.52	.036	.002	.00	.00	.282	2.00	1
email_spec1_product34_false-unreach-call.cil.c	timeout	902	879	3292954624		3	8.56	2.54	.258	timeout	1000	501	7455313920									timeout	1000	977	3287384064												timeout	1000	976	3291426816
email_spec1_product35_false-unreach-call.cil.c	timeout	965	943	3300306944		3	6.33	5.17	.352	timeout	1000	501	7346753536									timeout	1000	977	3378270208												timeout	1000	976	3264794624
email_spec1_productSimulator_false-unreach-call.cil.c	timeout	1000	971	4463611904						timeout	1000	501	8022781952									timeout	902	880	1895251968		2.08	846	873	15.6	844	844	21.7	812	833	819	timeout	1000	962	5628964864
email_spec27_product17_false-unreach-call.cil.c	unknown	357	346	2765504512		3	3.49	.508	.356	timeout	1000	501	6274134016									timeout	902	885	883068928		.692	875	880	2.05	875	875	3.93	862	866	872	unknown	224	208	3021271040		6	11.3	.406	7.16	3.12	.063	.002	.00	.00	.425	1.45	1
email_spec27_product18_false-unreach-call.cil.c	unknown	233	222	2624438272		3	3.75	.658	.237	timeout	1000	556	6429462528									timeout	1000	981	2770452480												unknown	167	153	2749464576		6	6.17	.689	5.24	1.88	.059	.001	.00	.00	.161	.985	1
email_spec27_product19_false-unreach-call.cil.c	unknown	291	279	2618368000		3	3.85	.969	.301	timeout	1000	584	6167572480									timeout	1000	979	2929430528												unknown	187	172	2760302592		6	6.70	.325	5.42	1.96	.054	.001	.00	.00	.168	1.11	1
email_spec27_product23_false-unreach-call.cil.c	timeout	953	932	3186667520		3	5.74	4.29	.271	timeout	1000	501	6888345600									timeout	902	882	902488064		.991	871	876	2.69	871	871	3.89	858	862	868	timeout	1000	980	3120484352
email_spec27_product24_false-unreach-call.cil.c	unknown	236	224	2677403648		3	4.22	.809	.425	timeout	1000	576	6220177408									timeout	1000	980	3014373376												unknown	195	179	2764591104		6	6.50	.286	6.33	2.58	.052	.001	.00	.00	.220	1.42	1
email_spec27_product25_false-unreach-call.cil.c	timeout	1000	977	3215736832						timeout	1000	501	7053430784									timeout	902	884	980959232		1.30	872	878	2.65	872	872	7.83	854	862	865	timeout	1000	979	3209224192
email_spec27_product27_false-unreach-call.cil.c	timeout	1000	979	3263320064						timeout	1000	501	7343968256									timeout	902	882	1019326464		1.57	869	876	3.40	868	868	8.92	848	857	860	timeout	1000	974	3276288000
email_spec27_product29_false-unreach-call.cil.c	unknown	376	360	2929532928		3	3.82	.862	.234	timeout	1000	501	7343742976									timeout	1000	977	3211317248												unknown	226	209	3049218048		6	12.4	.371	7.51	2.86	.075	.008	.00	.00	.259	1.55	1
email_spec27_product30_false-unreach-call.cil.c	unknown	325	313	2728300544		3	4.73	1.07	.251	timeout	1000	513	7200337920									timeout	1000	982	2860871680												unknown	250	235	2754068480		6	5.16	.269	6.41	2.56	.037	.003	.00	.00	.151	1.40	1
email_spec27_product31_false-unreach-call.cil.c	unknown	286	271	2822045696		3	4.40	.941	.267	timeout	1000	538	7102279680									timeout	1000	982	2904842240												unknown	194	177	2871238656		6	6.28	.362	7.27	2.91	.095	.001	.00	.00	.252	1.75	1
email_spec27_product32_false-unreach-call.cil.c	timeout	1000	977	3304640512						timeout	1000	501	7526285312									timeout	1000	976	3354079232												timeout	1000	978	3265650688
email_spec27_product33_false-unreach-call.cil.c	unknown	334	317	2844008448		3	5.19	1.23	.241	timeout	1000	501	7687585792									timeout	1000	978	3042279424												unknown	201	185	2872516608		6	6.12	.713	7.88	2.47	.040	.001	.00	.00	.170	2.39	1
email_spec27_product34_false-unreach-call.cil.c	timeout	1000	977	3288948736						timeout	1000	501	7541592064									timeout	1000	976	3435171840												timeout	1000	975	3324821504
email_spec27_product35_false-unreach-call.cil.c	timeout	1000	976	3338141696						timeout	1000	501	8035278848									timeout	902	884	934522880		1.01	873	878	2.92	872	872	5.12	861	866	867	timeout	1000	975	3355484160
email_spec27_productSimulator_false-unreach-call.cil.c	timeout	1000	968	4874584064						timeout	1000	501	8725360640									timeout	903	873	3759460352		1.89	830	866	17.7	827	827	647	16.3	663	18.5	timeout	905	870	4176318464		1	753	2.88	48.3	25.2	.681	.028	.00	.00	9.57	.627	0
email_spec3_product13_false-unreach-call.cil.c	unknown	14.6	7.92	449478656		1	1.51	.003		timeout	903	806	4685447168		1	5.65	.049	733				timeout	1000	980	2931736576												unknown	287	271	2758402048		6	5.29	.232	4.99	1.68	.043	.002	.00	.00	.111	1.03	1
email_spec3_product17_false-unreach-call.cil.c	unknown	16.7	9.00	452325376		1	1.82	.003		timeout	902	807	4713312256		1	5.42	.029	.004				timeout	905	883	1068785664		3.82	864	870	2.42	863	863	13.0	835	848	851	timeout	1000	975	3194916864
email_spec3_product18_false-unreach-call.cil.c	unknown	15.6	8.44	432087040		1	1.76	.004		timeout	902	803	5662883840		1	3.09	.209	.021				timeout	1000	974	3070562304												timeout	1000	978	2871578624
email_spec3_product19_false-unreach-call.cil.c	unknown	15.6	8.41	459255808		1	1.87	.015		timeout	902	814	5291511808		1	5.53	.036	.005				timeout	1000	974	3089301504												timeout	1000	979	2902622208
email_spec3_product23_false-unreach-call.cil.c	unknown	16.2	8.68	477306880		1	1.79	.003		timeout	908	794	5947121664		1	6.32	.015	706				timeout	902	884	864292864		1.24	873	878	2.32	873	873	4.53	862	867	869	timeout	1000	974	3273195520
email_spec3_product24_false-unreach-call.cil.c	unknown	16.5	8.84	453406720		1	1.83	.002		timeout	903	794	5755281408		1	4.55	.343	711				timeout	1000	974	3078287360												timeout	1000	976	2929307648
email_spec3_product25_false-unreach-call.cil.c	unknown	16.7	9.02	484884480		1	1.82	.003		timeout	903	784	6153580544		1	6.03	.019	685				timeout	1000	974	3420037120												timeout	1000	976	3268833280
email_spec3_product27_false-unreach-call.cil.c	unknown	16.7	9.01	467431424		1	1.70	.002		timeout	902	771	6366494720		1	5.33	.032	661				timeout	902	884	936841216		1.37	873	878	2.27	872	872	5.70	859	865	868	timeout	1000	973	3287515136
email_spec3_product28_false-unreach-call.cil.c	unknown	16.6	8.94	471191552		1	2.29	.004		timeout	902	803	5069561856		1	5.36	.022	.005				timeout	1000	980	2987175936												unknown	289	270	2803924992		6	7.83	.299	5.02	2.17	.074	.001	.00	.00	.191	.934	1
email_spec3_product29_false-unreach-call.cil.c	unknown	17.0	9.14	450338816		1	1.81	.003		timeout	902	801	5921546240		1	5.39	.075	.004				timeout	1000	973	3317268480												timeout	1000	973	3217981440
email_spec3_product30_false-unreach-call.cil.c	unknown	15.5	8.31	468623360		1	1.88	.002		timeout	902	789	6163546112		1	5.37	.021	.004				timeout	1000	973	3116777472												timeout	1000	978	2960285696
email_spec3_product31_false-unreach-call.cil.c	unknown	17.3	9.15	465907712		1	1.82	.004		timeout	903	792	5939171328		1	5.39	.011	707				timeout	1000	977	3005747200												timeout	1000	976	3046612992
email_spec3_product32_false-unreach-call.cil.c	unknown	16.5	8.84	449519616		1	1.77	.003		timeout	902	769	6518104064		1	5.40	.045	.013				timeout	903	883	940625920		2.07	870	876	2.57	870	870	6.39	858	864	865	timeout	1000	974	3315032064
email_spec3_product33_false-unreach-call.cil.c	unknown	16.2	8.76	481583104		1	1.96	.003		timeout	902	765	6475051008		1	5.74	.155	.017				timeout	1000	974	3170349056												timeout	1000	977	3055747072
email_spec3_product34_false-unreach-call.cil.c	unknown	16.9	9.18	464302080		1	1.76	.005		timeout	902	752	7142518784		1	5.28	.021	.004				timeout	902	883	919097344		1.94	871	876	2.04	870	870	6.77	858	865	865	timeout	1000	974	3374116864
email_spec3_product35_false-unreach-call.cil.c	unknown	17.9	9.58	463048704		1	1.87	.002		timeout	902	728	7245975552		1	5.21	.030	575				timeout	902	883	963444736		2.08	871	876	2.65	870	870	7.11	858	865	864	timeout	1000	974	3363684352
email_spec3_productSimulator_false-unreach-call.cil.c	unknown	38.8	24.9	1391112192		1	4.05	.090		timeout	907	695	7687184384		1	5.65	.157	.005				timeout	904	879	1690759168		4.33	848	867	10.2	847	847	29.1	804	833	812	timeout	1000	967	5635235840
email_spec4_product18_false-unreach-call.cil.c	unknown	201	190	2613141504		3	3.67	.632	.209	timeout	1000	573	6701621248									unknown	167	154	2695208960		1.75	4.16	8.58	2.15	3.88	3.79	2.84	.343	3.18	1.50	unknown	174	161	2684792832		6	4.71	.686	5.11	1.77	.040	.00	.00	.00	.054	.897	1
email_spec4_product19_false-unreach-call.cil.c	unknown	257	246	2636759040		3	4.39	.535	.325	timeout	1000	595	6597558272									unknown	206	193	2731372544		2.03	4.58	9.10	2.13	4.29	4.25	2.63	.835	3.47	2.17	unknown	155	140	2772652032		6	6.61	.806	4.95	1.66	.083	.001	.00	.00	.059	1.00	1
email_spec4_product23_false-unreach-call.cil.c	unknown	825	803	3088175104		3	5.21	3.40	.260	timeout	1000	501	7456501760									timeout	1000	980	3197706240												timeout	1000	978	3060568064
email_spec4_product24_false-unreach-call.cil.c	unknown	233	222	2679025664		3	4.47	.529	.284	timeout	1000	595	6980403200									timeout	1000	979	2924163072												unknown	175	159	2752454656		6	6.16	.239	5.71	2.38	.056	.003	.00	.00	.123	1.13	1
email_spec4_product25_false-unreach-call.cil.c	timeout	918	897	3088076800		3	5.79	3.84	.292	timeout	1000	501	6863511552									timeout	1000	979	3249217536												timeout	1000	978	3091603456
email_spec4_product27_false-unreach-call.cil.c	unknown	856	832	3192770560		3	7.38	3.79	.328	timeout	1000	501	7620706304									timeout	1000	978	3216269312												timeout	1000	978	3096064000
email_spec4_product30_false-unreach-call.cil.c	unknown	267	254	2655657984		3	4.55	.728	.452	timeout	1000	582	6884323328									unknown	192	179	2741202944		1.98	4.28	8.77	2.27	4.03	3.95	2.56	.718	3.28	1.89	unknown	188	171	2782785536		6	6.64	.267	6.16	2.04	.073	.003	.00	.00	.059	1.57	1
email_spec4_product31_false-unreach-call.cil.c	unknown	257	241	2759778304		3	4.32	.731	.214	timeout	1000	621	6793084928									timeout	1000	980	2848518144												unknown	207	191	2792366080		6	5.07	.339	7.38	2.89	.083	.003	.00	.00	.109	1.98	1
email_spec4_product32_false-unreach-call.cil.c	unknown	872	849	3239407616		3	6.83	3.11	.262	timeout	1000	501	7285383168									timeout	1000	979	3259334656												timeout	1000	977	3194667008
email_spec4_product33_false-unreach-call.cil.c	unknown	294	277	2783424512		3	4.91	1.01	.266	timeout	1000	577	7205855232									timeout	1000	982	2798256128												unknown	211	195	2777997312		6	4.89	.291	7.72	3.10	.062	.001	.00	.00	.102	1.93	1
email_spec4_product34_false-unreach-call.cil.c	unknown	832	810	3290464256		3	6.45	2.00	.292	timeout	1000	501	7222337536									timeout	1000	975	3409739776												timeout	1000	976	3273359360
email_spec4_product35_false-unreach-call.cil.c	timeout	1000	976	3352588288						timeout	1000	501	7894855680									timeout	1000	977	3247706112												timeout	1000	976	3263418368
email_spec4_productSimulator_false-unreach-call.cil.c	timeout	1000	972	4290281472						timeout	1000	501	7976943616									timeout	1000	965	6080794624												timeout	1000	968	5665951744
email_spec6_product12_false-unreach-call.cil.c	unknown	119	110	2607882240		3	3.38	.520	.228	timeout	1000	742	6246031360									timeout	1000	979	2893045760												unknown	159	145	2630320128		6	3.83	.268	4.82	2.13	.046	.009	.00	.00	.082	.947	1
email_spec6_product14_false-unreach-call.cil.c	unknown	387	376	2752933888		3	3.58	.529	.252	timeout	1000	501	6993567744									timeout	1000	976	3291860992												timeout	1000	979	2932248576
email_spec6_product15_false-unreach-call.cil.c	unknown	259	249	2608467968		3	3.73	.513	.274	timeout	1000	577	6875176960									timeout	1000	978	2980728832												timeout	1000	981	2688831488
email_spec6_product16_false-unreach-call.cil.c	unknown	226	214	2645385216		3	4.29	.751	.297	timeout	1000	578	6776737792									timeout	902	885	951164928		.732	875	880	2.34	874	874	3.20	860	863	873	timeout	1000	980	2730573824
email_spec6_product20_false-unreach-call.cil.c	unknown	894	871	3190968320		3	5.49	3.61	.259	timeout	1000	501	7034945536									timeout	902	880	1126653952		1.13	868	874	3.08	868	867	11.4	840	852	859	timeout	1000	978	3049279488
email_spec6_product21_false-unreach-call.cil.c	timeout	1000	979	3187920896						timeout	1000	501	7206481920									timeout	902	881	1132965888		2.27	865	874	3.68	864	863	22.3	809	831	844	timeout	1000	978	3065597952
email_spec6_product22_false-unreach-call.cil.c	unknown	224	213	2637164544		3	4.15	.751	.342	timeout	1000	551	6888525824									timeout	1000	975	3070545920												timeout	1000	980	2750275584
email_spec6_product26_false-unreach-call.cil.c	unknown	897	873	3282997248		3	7.62	3.10	.457	timeout	1000	501	7355011072									timeout	1000	978	3423543296												timeout	1000	979	3072495616
email_spec6_product28_false-unreach-call.cil.c	unknown	110	99.4	2572963840		3	3.79	.538	.193	timeout	1000	735	6256582656									timeout	1000	983	2828218368												unknown	160	144	2762391552		6	5.71	.293	6.24	2.07	.044	.003	.00	.00	.102	1.51	1
email_spec6_product29_false-unreach-call.cil.c	unknown	390	377	2864742400		3	3.87	.676	.239	timeout	1000	501	7253876736									timeout	902	885	1079185408		.557	873	879	3.26	873	872	5.56	848	853	868	timeout	1000	979	3008942080
email_spec6_product30_false-unreach-call.cil.c	unknown	236	223	2657771520		3	4.53	.832	.283	timeout	1000	602	6314737664									timeout	1000	979	2994581504												timeout	1000	980	2719318016
email_spec6_product31_false-unreach-call.cil.c	unknown	284	268	2758430720		3	4.69	.854	.270	timeout	1000	531	7263936512									timeout	1000	980	2989068288												timeout	1000	981	2769297408
email_spec6_product32_false-unreach-call.cil.c	timeout	1000	978	3248803840						timeout	1000	501	7198351360									timeout	902	881	1276604416		1.12	869	876	3.50	868	868	11.5	836	847	857	timeout	1000	978	3108298752
email_spec6_product33_false-unreach-call.cil.c	unknown	297	280	2805940224		3	5.36	1.18	.273	timeout	1000	517	7621562368									timeout	1000	976	3106123776												timeout	1000	980	2752442368
email_spec6_product34_false-unreach-call.cil.c	timeout	1000	979	3244003328						timeout	1000	501	7549222912									timeout	902	878	1355292672		1.78	864	872	3.69	863	863	19.1	820	839	845	timeout	1000	977	3159654400
email_spec6_product35_false-unreach-call.cil.c	timeout	1000	977	3320242176						timeout	1000	501	7584608256									timeout	1000	978	3513122816												timeout	1000	976	3171577856
email_spec6_productSimulator_false-unreach-call.cil.c	timeout	1000	971	4336873472						timeout	1000	501	8089399296									timeout	902	880	1603444736		2.42	853	873	10.4	852	851	11.3	832	843	840	timeout	1000	965	5269639168
email_spec7_product28_false-unreach-call.cil.c	unknown	121	111	2605035520		3	3.16	.657	.197	timeout	1000	728	6147776512									timeout	1000	980	2841423872												unknown	165	151	2683805696		6	3.67	.294	5.11	2.13	.058	.001	.00	.00	.094	1.02	1
email_spec7_product29_false-unreach-call.cil.c	unknown	366	353	2827702272		3	3.89	.788	.235	timeout	1000	501	6651260928									timeout	902	882	1076568064		1.17	869	877	2.99	869	869	9.97	835	845	860	timeout	1000	976	3043328000
email_spec7_product30_false-unreach-call.cil.c	unknown	268	257	2647449600		3	4.15	1.01	.298	timeout	1000	579	6499368960									timeout	1000	979	3007266816												timeout	1000	981	2674917376
email_spec7_product31_false-unreach-call.cil.c	unknown	305	294	2667540480		3	4.44	.865	.216	timeout	1000	535	6692958208									timeout	1000	976	3209498624												timeout	1000	981	2741866496
email_spec7_product32_false-unreach-call.cil.c	timeout	1000	976	3245674496						timeout	1000	501	7640289280									timeout	1000	975	3303981056												timeout	1000	979	3029225472
email_spec7_product33_false-unreach-call.cil.c	unknown	316	298	2778750976		3	5.04	1.46	.256	timeout	1000	576	7010643968									timeout	1000	975	3153543168												timeout	1000	981	2765598720
email_spec7_product34_false-unreach-call.cil.c	timeout	1000	978	3282481152						timeout	1000	501	7513182208									timeout	902	879	1253302272		1.48	866	873	3.68	865	865	11.7	833	845	854	timeout	1000	979	3095990272
email_spec7_product35_false-unreach-call.cil.c	timeout	1000	977	3303407616						timeout	1000	501	7881551872									timeout	1000	980	3417710592												timeout	1000	978	3180539904
email_spec7_productSimulator_false-unreach-call.cil.c	timeout	1000	969	4556800000						timeout	1000	501	7991164928									timeout	1000	965	5111959552												timeout	1000	964	5560844288
email_spec8_product15_false-unreach-call.cil.c	unknown	148	137	2621882368		3	3.77	.611	.230	timeout	1000	734	6178148352									unknown	175	162	2717667328		1.82	3.86	8.43	2.22	3.59	3.48	2.13	.727	2.86	1.90	unknown	190	176	2706497536		6	4.62	.298	5.19	1.99	.061	.003	.00	.00	.067	.938	1
email_spec8_product16_false-unreach-call.cil.c	unknown	168	157	2637537280		3	4.08	.587	.332	timeout	1000	710	6181666816									timeout	1000	983	2825650176												unknown	195	179	2737000448		6	5.82	.308	5.74	2.34	.037	.001	.00	.00	.120	1.31	1
email_spec8_product20_false-unreach-call.cil.c	unknown	756	734	3108327424		3	5.13	3.96	.286	timeout	1000	501	7179239424									timeout	1000	974	3267072000												timeout	1000	978	3074490368
email_spec8_product21_false-unreach-call.cil.c	unknown	683	661	3162468352		3	5.22	5.28	.277	timeout	1000	501	7239483392									timeout	1000	979	3185229824												timeout	1000	978	3105669120
email_spec8_product22_false-unreach-call.cil.c	unknown	136	125	2621403136		3	3.76	.686	.302	timeout	1000	707	6674841600									timeout	1000	981	2862792704												unknown	198	183	2739937280		6	5.08	.678	5.60	1.62	.041	.002	.00	.00	.079	1.55	1
email_spec8_product26_false-unreach-call.cil.c	unknown	733	709	3207045120		3	8.14	2.90	.285	timeout	1000	501	8047702016									timeout	902	885	965488640		1.27	874	879	2.64	873	873	7.76	858	866	867	timeout	1000	976	3185905664
email_spec8_product30_false-unreach-call.cil.c	unknown	183	171	2641944576		3	4.28	.760	.281	timeout	1000	720	6637387776									timeout	1000	980	2828988416												unknown	210	194	2778902528		6	6.16	.695	6.59	2.21	.033	.001	.00	.00	.074	1.77	1
email_spec8_product31_false-unreach-call.cil.c	unknown	158	143	2746744832		3	4.38	.769	.299	timeout	1000	700	6958198784									timeout	1000	981	2832850944												unknown	197	182	2762186752		6	5.34	.879	6.61	2.38	.056	.002	.00	.00	.097	1.27	1
email_spec8_product32_false-unreach-call.cil.c	timeout	929	904	3230289920		3	8.89	2.34	.287	timeout	1000	501	7470354432									timeout	1000	977	3233710080												timeout	1000	977	3154354176
email_spec8_product33_false-unreach-call.cil.c	unknown	173	158	2768449536		3	4.54	.914	.269	timeout	1000	682	6665269248									timeout	1000	980	2914361344												unknown	214	199	2801197056		6	5.39	.421	7.34	3.11	.091	.003	.00	.00	.090	1.50	1
email_spec8_product34_false-unreach-call.cil.c	unknown	810	785	3298258944		3	8.54	2.62	.242	timeout	1000	501	7551426560									timeout	902	886	941973504		1.33	876	881	2.68	875	875	5.18	863	868	871	timeout	1000	978	3188875264
email_spec8_product35_false-unreach-call.cil.c	unknown	869	845	3310235648		3	6.60	4.14	.256	timeout	1000	501	7452835840									timeout	902	883	961957888		1.58	870	876	3.25	869	869	9.37	851	860	861	timeout	1000	977	3267440640
email_spec8_productSimulator_false-unreach-call.cil.c	timeout	1000	973	4308709376						timeout	1000	501	8217571328									timeout	902	879	2394853376		3.63	826	870	20.8	823	822	40.8	766	806	773	timeout	1000	967	5538050048
email_spec9_product15_false-unreach-call.cil.c	unknown	153	143	2588463104		3	3.80	.587	.232	timeout	1000	737	6094442496									unknown	176	164	2720165888		1.93	4.00	8.15	2.19	3.68	3.61	2.28	.683	2.96	2.01	unknown	193	178	2699468800		6	5.62	.229	5.29	2.35	.053	.011	.00	.00	.074	.972	1
email_spec9_product16_false-unreach-call.cil.c	unknown	124	113	2608177152		3	4.03	.594	.342	timeout	1000	735	6160736256									timeout	1000	982	2838347776												unknown	167	153	2726809600		6	5.36	.290	5.75	2.52	.061	.003	.00	.00	.167	1.28	1
email_spec9_product20_false-unreach-call.cil.c	unknown	694	673	3058413568		3	5.57	3.41	.290	timeout	1000	501	7254003712									timeout	1000	976	3249008640												timeout	1000	978	3087937536
email_spec9_product21_false-unreach-call.cil.c	unknown	761	739	3150684160		3	5.89	4.40	.283	timeout	1000	501	7569272832									timeout	1000	976	3225817088												timeout	1000	977	3132530688
email_spec9_product22_false-unreach-call.cil.c	unknown	144	133	2631749632		3	3.70	.798	.283	timeout	1000	704	6605955072									timeout	1000	983	2860994560												unknown	175	161	2709864448		6	4.38	.619	5.38	1.89	.093	.001	.00	.00	.075	1.15	1
email_spec9_product26_false-unreach-call.cil.c	unknown	864	841	3211108352		3	8.89	2.08	.292	timeout	1000	501	7311872000									timeout	902	884	928473088		1.40	872	878	2.67	871	871	9.38	854	864	863	timeout	1000	977	3176923136
email_spec9_product30_false-unreach-call.cil.c	unknown	139	128	2635005952		3	4.29	.797	.488	timeout	1000	721	6617268224									timeout	1000	981	2801238016												unknown	182	166	2726473728		6	6.56	.279	6.31	2.72	.050	.002	.00	.00	.056	1.22	1
email_spec9_product31_false-unreach-call.cil.c	unknown	158	143	2743599104		3	4.59	.797	.275	timeout	1000	686	6887661568									timeout	1000	980	2846490624												unknown	213	196	2808090624		6	5.32	.436	7.84	2.64	.140	.002	.00	.00	.147	2.15	1
email_spec9_product32_false-unreach-call.cil.c	unknown	627	606	3245625344		3	7.88	2.71	.256	timeout	1000	501	7575748608									timeout	1000	977	3209318400												timeout	1000	977	3187220480
email_spec9_product33_false-unreach-call.cil.c	unknown	148	134	2742902784		3	4.33	.807	.218	timeout	1000	663	6988742656									timeout	1000	981	2898640896												unknown	162	146	2824011776		6	6.13	.493	6.83	3.03	.082	.003	.00	.00	.125	1.27	1
email_spec9_product34_false-unreach-call.cil.c	unknown	735	713	3250339840		3	6.32	1.95	.238	timeout	1000	501	7528787968									timeout	902	884	946257920		1.36	873	878	2.56	872	872	5.46	859	865	868	timeout	1000	976	3252678656
email_spec9_product35_false-unreach-call.cil.c	timeout	923	901	3299880960		3	6.65	5.45	.262	timeout	1000	501	7504097280									timeout	902	884	976859136		1.58	871	878	3.33	871	871	9.45	853	862	862	timeout	1000	976	3232186368
email_spec9_productSimulator_false-unreach-call.cil.c	timeout	1000	969	4328349696						timeout	1000	501	8028262400									timeout	902	877	2388942848		3.94	827	869	21.3	823	822	44.0	763	807	770	timeout	1000	967	5577220096
email_spec0_product05_true-unreach-call.cil.c	true	15.7	8.37	410005504		5	2.71	.00	.450	true	21.1	11.1	509972480		1	3.85	.00	.011	.349			true	10.1	5.55	387375104		.258	.147	1.30	.386	.043	.037	.001	.00	.001		true	10.5	5.75	351981568		0	.277	.093	1.32	.487	.012	.002	.00	.00	.00	.007
email_spec0_product09_true-unreach-call.cil.c	true	24.9	13.0	534843392		5	5.82	.00	.691	true	33.4	17.1	846413824		1	4.18	.00	.013	.619			true	12.9	7.07	423657472		1.00	.258	1.90	.548	.124	.105	.011	.00	.011		true	12.7	7.06	377876480		0	.764	.611	2.01	.712	.013	.002	.00	.00	.00	.010
email_spec0_product10_true-unreach-call.cil.c	true	16.0	8.57	439472128		5	2.71	.004	.468	true	28.5	14.7	668405760		1	3.54	.00	.005	.620			true	10.4	5.71	393048064		.333	.137	1.40	.407	.059	.046	.003	.00	.003		true	10.6	5.85	369328128		0	.384	.110	1.54	.505	.011	.001	.00	.00	.00	.012
email_spec0_product11_true-unreach-call.cil.c	true	19.9	10.6	486666240		5	4.04	.00	.781	true	37.5	19.1	871116800		1	4.11	.001	2.81	.710	5.95	.023	true	11.9	6.51	416333824		.310	.229	1.92	.944	.066	.033	.001	.00	.001		true	11.9	6.49	393224192		0	.272	.613	2.08	.728	.465	.447	.00	.00	.00	.006
email_spec0_product19_true-unreach-call.cil.c	true	22.8	12.1	508227584		5	5.26	.001	.838	true	47.6	24.3	1143980032		1	5.21	.00	.004	1.29	8.23	.048	true	13.0	7.16	445521920		.471	.240	2.35	1.21	.074	.050	.003	.00	.003		true	13.7	7.38	426012672		0	.503	.232	2.56	.943	.064	.001	.00	.00	.00	.022
email_spec0_product24_true-unreach-call.cil.c	true	24.1	12.9	522575872		5	5.49	.00	.860	true	49.8	25.5	924278784		1	4.94	.00	3.98	1.54	9.22	.047	true	13.7	7.43	459874304		.730	.280	2.27	1.08	.122	.073	.004	.00	.004		true	14.3	7.72	434667520		0	.727	.155	2.67	1.44	.037	.001	.00	.00	.00	.014
email_spec0_product25_true-unreach-call.cil.c	true	31.9	16.9	864862208		5	8.62	.001	1.76	true	66.7	33.8	1013796864		1	5.90	.00	.007	1.68	14.8	.071	true	18.0	9.88	526249984		2.27	.430	3.18	1.48	.239	.174	.035	.00	.035		true	17.8	9.91	489930752		0	1.96	.218	3.48	1.46	.039	.001	.00	.00	.00	.011
email_spec0_product27_true-unreach-call.cil.c	true	34.6	18.5	893657088		5	8.89	.001	2.71	true	69.0	35.0	1061957632		1	5.45	.001	5.52	.996	15.8	.075	true	18.3	10.2	520536064		2.17	.485	3.58	1.71	.223	.145	.020	.00	.020		true	24.2	13.0	565325824		0	4.04	.309	3.98	1.74	.060	.002	.00	.00	.00	.011
email_spec0_product36_true-unreach-call.cil.c	true	25.5	13.5	585596928		5	6.47	.00	.904	true	48.2	24.6	900579328		1	4.04	.001	.005	.544	9.79	.050	true	13.3	7.55	457158656		1.19	.298	2.15	.649	.124	.090	.011	.00	.011		true	13.2	7.48	430190592		0	1.17	.491	2.12	.800	.030	.002	.00	.00	.00	.002
email_spec0_product37_true-unreach-call.cil.c	true	20.2	10.7	483749888		5	4.14	.00	.990	true	43.1	22.1	887463936		1	5.16	.025	3.79	.905	6.56	.024	true	12.3	6.69	436699136		.336	.202	2.14	1.14	.051	.033	.002	.00	.002		true	12.8	7.00	403693568		0	.352	.159	2.41	.841	.038	.002	.00	.00	.00	.010
email_spec0_product38_true-unreach-call.cil.c	true	29.2	15.4	636481536		5	6.27	.00	2.12	true	57.1	29.0	961671168		1	5.81	.00	.009	1.21	10.6	.053	true	15.2	8.20	462008320		1.13	.276	2.71	1.34	.132	.101	.014	.00	.014		true	14.9	8.12	395390976		0	1.17	.223	2.73	1.50	.036	.002	.00	.00	.00	.035
email_spec0_product40_true-unreach-call.cil.c	true	31.0	16.4	712159232		5	7.83	.001	2.27	true	61.9	31.5	1010028544		1	5.73	.024	5.02	1.82	12.2	.069	true	16.6	9.07	490409984		1.64	.373	2.97	1.51	.161	.134	.025	.00	.025		true	15.5	8.58	459952128		0	1.40	.226	3.07	1.26	.039	.001	.00	.00	.00	.030
email_spec11_product03_true-unreach-call.cil.c	true	15.1	8.20	404500480		5	2.35	.00	.462	true	25.8	13.3	593256448		1	4.38	.00	.010	.389			true	10.6	5.83	395853824		.247	.133	1.19	.308	.070	.037	.002	.00	.002		true	10.6	5.77	364437504		0	.257	.124	1.38	.833	.034	.00	.00	.00	.00	.005
email_spec11_product07_true-unreach-call.cil.c	true	21.4	11.2	462827520		5	4.74	.00	.656	true	35.0	18.0	815210496		1	3.14	.002	.011	1.20			true	12.6	6.98	446484480		.863	.282	1.80	.606	.147	.124	.009	.00	.009		true	12.4	6.97	412930048		0	.807	.174	1.82	1.01	.023	.002	.00	.00	.00	.007
email_spec11_product08_true-unreach-call.cil.c	true	17.7	9.54	468058112		5	3.29	.00	.842	true	39.0	19.9	883269632		1	5.04	.00	2.96	.749	6.14	.023	true	11.9	6.48	419418112		.335	.201	1.87	.948	.057	.038	.001	.00	.001		true	12.2	6.69	393740288		0	.302	.156	2.06	1.12	.025	.001	.00	.00	.00	.008
email_spec11_product10_true-unreach-call.cil.c	true	16.2	8.70	441192448		5	3.04	.00	.488	true	27.8	14.3	625729536		1	3.05	.00	.006	1.30			true	11.4	6.19	396988416		.355	.126	1.45	.377	.048	.040	.002	.00	.002		true	10.7	5.87	378388480		0	.326	.123	1.48	.444	.022	.002	.00	.00	.00	.001
email_spec11_product18_true-unreach-call.cil.c	true	21.7	11.5	500875264		5	4.70	.00	.996	true	46.7	23.8	863404032		1	5.34	.00	3.78	1.35	7.37	.045	true	12.4	6.82	443662336		.432	.190	2.22	1.22	.062	.045	.003	.00	.003		true	13.1	7.13	420851712		0	.463	.147	2.60	1.40	.037	.001	.00	.00	.00	.019
email_spec11_product23_true-unreach-call.cil.c	true	31.3	16.3	777584640		5	7.27	.00	2.31	true	67.4	34.2	980078592		1	5.30	.00	5.47	1.49	14.0	.046	true	17.3	9.48	507961344		2.02	.390	3.13	1.62	.173	.145	.016	.00	.016		true	16.0	8.93	463966208		0	1.53	.280	3.28	1.87	.072	.001	.00	.00	.00	.009
email_spec11_product24_true-unreach-call.cil.c	true	25.2	13.3	561577984		5	5.42	.001	1.37	true	48.2	24.6	884334592		1	5.61	.00	.003	1.04	8.64	.029	true	14.0	7.60	448061440		.543	.277	2.40	1.16	.125	.061	.004	.00	.004		true	14.1	7.67	429957120		0	.479	.560	2.76	1.12	.066	.002	.00	.00	.00	.016
email_spec11_product27_true-unreach-call.cil.c	true	33.9	18.1	911052800		5	9.15	.00	2.23	true	70.0	35.4	1001500672		1	5.17	.00	5.76	1.91	14.5	.045	true	18.5	10.3	517656576		2.09	.415	3.60	1.72	.158	.116	.021	.00	.021		true	20.4	11.2	530391040		0	2.36	.720	3.92	1.69	.048	.001	.00	.00	.00	.022
email_spec11_product36_true-unreach-call.cil.c	true	23.6	12.5	539082752		5	6.07	.00	.555	true	47.7	24.3	919089152		1	4.05	.001	.006	.534	9.89	.033	true	13.7	7.72	441012224		1.21	.273	2.18	.727	.134	.093	.009	.00	.009		true	13.5	7.57	427286528		0	1.16	.211	2.24	1.28	.026	.002	.00	.00	.00	.008
email_spec11_product37_true-unreach-call.cil.c	true	20.3	10.9	493547520		5	4.09	.00	.870	true	42.2	21.6	898686976		1	4.47	.001	3.28	.788	7.11	.043	true	12.8	6.95	408522752		.339	.226	2.07	1.09	.070	.028	.002	.00	.002		true	12.6	6.90	374374400		0	.334	.166	2.40	.847	.014	.001	.00	.00	.00	.009
email_spec11_product39_true-unreach-call.cil.c	true	24.8	13.2	560594944		5	5.46	.001	1.11	true	50.3	25.6	876392448		1	4.94	.028	4.14	1.25	9.37	.044	true	14.5	7.86	468148224		1.23	.394	2.41	1.14	.186	.153	.018	.00	.018		true	15.3	8.33	439799808		0	1.14	.206	2.92	1.15	.043	.001	.00	.00	.00	.017
email_spec11_product40_true-unreach-call.cil.c	true	30.1	15.8	739708928		5	6.84	.001	2.59	true	60.6	30.7	980054016		1	5.04	.001	.010	1.04	11.4	.090	true	16.0	8.71	482668544		1.48	.285	2.88	1.48	.140	.083	.011	.00	.011		true	15.6	8.64	460222464		0	1.31	.182	2.85	1.53	.047	.002	.00	.00	.00	.024
email_spec1_product12_true-unreach-call.cil.c	true	17.8	9.65	443248640		5	3.17	.001	.908	true	71.6	36.3	1475076096		3	7.75	.00	.004	4.77	10.3	4.56	true	16.1	8.58	447336448		.390	1.45	3.66	1.12	1.27	1.22	.904	.020	.924	.394	true	13.3	7.13	383180800		1	.465	.174	2.50	.940	.027	.009	.00	.00	.013	.130	1
email_spec1_product28_true-unreach-call.cil.c	true	20.7	11.0	503771136		5	4.07	.00	1.05	true	93.7	47.4	1565741056		4	10.2	.00	.006	5.01	12.9	9.96	true	17.8	9.58	510386176		.439	1.83	4.61	1.34	1.50	1.47	1.17	.010	1.18	.293	true	14.5	7.82	436449280		1	.624	.180	2.90	1.66	.023	.001	.00	.00	.007	.084	1
email_spec27_product13_true-unreach-call.cil.c	true	21.1	11.6	517562368		5	3.65	1.41	.752	true	87.6	44.2	1307975680		3	8.26	1.92	8.83	3.14	12.5	9.29	true	25.1	14.3	508219392		.585	5.71	9.39	1.86	5.41	5.34	2.48	2.25	4.72	3.43	true	17.3	9.51	467365888		3	1.03	.249	3.93	1.83	.058	.002	.00	.00	.048	.503	1
email_spec27_product28_true-unreach-call.cil.c	true	22.2	12.2	530432000		5	4.10	1.17	.858	true	99.5	50.3	1672744960		4	7.87	1.93	.004	2.52	15.0	13.5	true	26.1	15.4	529551360		.702	5.96	10.2	2.27	5.70	5.65	3.14	1.85	5.00	2.76	true	19.5	10.4	513548288		3	1.70	.241	4.22	1.90	.032	.001	.00	.00	.042	.757	1
email_spec4_product13_true-unreach-call.cil.c	true	20.5	11.0	506798080		5	3.56	.920	.795	true	82.7	41.9	1323245568		3	8.11	1.48	8.80	3.50	11.6	8.15	true	15.8	8.57	461451264		.341	1.40	3.67	1.19	1.19	1.14	.877	.010	.887	.413	true	12.8	6.96	414838784		1	.496	.594	2.32	.821	.421	.386	.00	.00	.007	.091	1
email_spec4_product17_true-unreach-call.cil.c	true	22.4	12.6	533278720		5	4.41	.954	.810	true	94.6	47.8	1537626112		3	9.27	.945	11.8	3.48	16.1	8.05	true	33.2	20.2	749535232		.598	9.75	15.3	2.79	9.40	9.23	6.26	1.59	7.85	3.26	true	36.3	20.3	676245504		5	8.47	.334	7.17	2.56	.060	.004	.00	.00	.189	1.60	1
email_spec4_product28_true-unreach-call.cil.c	true	20.7	11.4	497324032		5	4.03	.773	.746	true	98.4	49.8	1660366848		5	9.99	1.71	13.5	2.26	13.9	10.2	true	24.2	13.6	529457152		.648	4.14	8.44	2.23	3.80	3.73	2.42	.648	3.07	1.86	true	16.7	9.19	470913024		3	1.07	.293	3.83	1.81	.077	.001	.00	.00	.022	.375	1
email_spec4_product29_true-unreach-call.cil.c	true	32.5	17.5	727855104		5	5.69	2.53	2.10	true	123	62.1	2491113472		5	10.3	2.33	23.1	2.79	20.5	13.2	true	33.2	21.1	792907776		.869	10.1	15.6	2.66	9.64	9.55	7.20	.846	8.04	2.51	true	37.0	21.9	765267968		5	9.31	.441	8.07	3.42	.089	.001	.00	.00	.182	1.66	1
email_spec7_product13_true-unreach-call.cil.c	true	18.2	9.90	489893888		5	3.29	.00	.873	true	45.5	23.3	894140416		1	5.57	.001	3.75	1.52	7.00	.023	true	12.4	6.78	410558464		.307	.244	2.04	1.00	.052	.030	.003	.00	.003		true	13.3	7.21	389042176		0	.434	.159	2.48	1.46	.021	.001	.00	.00	.00	.004
email_spec7_product17_true-unreach-call.cil.c	true	21.3	11.5	502026240		5	4.41	.001	.928	true	63.0	32.1	993153024		1	5.72	.00	5.53	1.81	11.1	.032	true	16.5	9.11	477712384		1.49	.336	3.08	1.55	.148	.107	.013	.00	.013		true	15.6	8.66	419434496		0	1.30	.672	3.05	1.18	.056	.002	.00	.00	.00	.011
email_spec7_product18_true-unreach-call.cil.c	true	20.6	11.0	486436864		5	4.21	.00	.957	true	43.3	22.1	879906816		1	4.39	.020	3.45	.837	7.49	.018	true	12.1	6.65	428847104		.306	.175	2.13	1.14	.055	.034	.003	.00	.003		true	13.2	7.11	417812480		0	.504	.195	2.29	.982	.031	.002	.00	.00	.00	.026
email_spec7_product19_true-unreach-call.cil.c	true	22.4	11.9	487469056		5	4.89	.00	.918	true	47.1	24.1	907300864		1	5.03	.00	3.97	.766	8.79	.042	true	12.6	6.93	439181312		.421	.183	2.19	1.18	.072	.051	.003	.00	.003		true	13.6	7.33	403959808		0	.445	.234	2.56	1.44	.037	.001	.00	.00	.00	.011
email_spec7_product23_true-unreach-call.cil.c	true	33.3	17.3	791625728		5	8.27	.002	2.28	true	60.1	30.4	984834048		1	5.51	.001	4.69	.957	13.1	.052	true	16.7	9.23	494624768		1.64	.311	3.09	1.51	.124	.106	.017	.00	.017		true	15.8	8.78	419860480		0	1.23	.292	3.19	1.67	.063	.001	.00	.00	.00	.015
email_spec7_product24_true-unreach-call.cil.c	true	25.3	13.5	569810944		5	5.43	.003	.953	true	53.5	27.3	891097088		1	6.17	.001	4.31	1.27	8.97	.042	true	12.8	6.88	435085312		.397	.197	2.24	1.15	.057	.034	.003	.00	.003		true	13.8	7.46	425046016		0	.503	.734	2.65	.953	.060	.012	.00	.00	.00	.013
email_spec7_product25_true-unreach-call.cil.c	true	34.3	18.3	872493056		5	9.41	.00	1.90	true	70.4	35.7	965881856		1	5.77	.00	5.85	1.53	14.3	.032	true	17.6	9.72	512036864		1.68	.363	3.42	1.68	.182	.146	.013	.00	.013		true	16.9	9.37	487514112		0	1.66	.224	3.25	1.36	.055	.00	.00	.00	.00	.024
email_spec7_product27_true-unreach-call.cil.c	true	34.2	18.4	900726784		5	9.11	.001	2.48	true	67.8	34.3	988807168		1	5.46	.00	5.61	1.34	14.0	.057	true	19.0	10.3	530718720		2.15	.393	3.67	1.80	.167	.124	.014	.00	.014		true	17.1	9.61	481206272		0	1.67	.197	3.49	1.71	.043	.002	.00	.00	.00	.035
email_spec8_product12_true-unreach-call.cil.c	true	18.6	9.90	485339136		5	3.32	.00	.940	true	74.6	37.7	1059332096		3	7.80	.00	.013	3.46	12.2	5.04	true	15.0	8.17	453287936		.367	1.01	3.47	.775	.831	.799	.607	.008	.615	.344	true	13.1	7.18	420077568		1	.427	.517	2.41	.956	.036	.007	.00	.00	.005	.065	1
email_spec8_product14_true-unreach-call.cil.c	true	22.3	12.6	536801280		5	4.56	1.11	.857	true	96.1	48.5	1544749056		3	7.94	1.46	.005	3.44	17.4	7.53	true	550	532	954863616		2.38	517	525	3.56	516	516	20.3	488	509	497	true	49.1	32.2	881381376		14	15.6	.428	11.9	3.51	.115	.002	.00	.00	1.05	5.21	1
email_spec8_product28_true-unreach-call.cil.c	true	20.1	10.8	490889216		5	4.03	.001	.884	true	93.3	47.4	1560080384		4	9.79	.002	.005	2.65	12.7	12.2	true	17.0	9.17	513286144		.413	1.89	4.33	1.24	1.69	1.66	1.35	.009	1.36	.477	true	14.0	7.63	429846528		1	.477	.580	2.77	1.03	.382	.001	.00	.00	.007	.131	1
email_spec8_product29_true-unreach-call.cil.c	true	31.2	16.9	712159232		5	5.80	2.98	1.28	true	123	62.2	2545819648		5	9.24	2.54	24.1	2.77	21.1	13.8	timeout	902	883	1035370496		1.97	869	877	3.71	868	868	12.1	841	853	858	true	58.9	43.9	939020288		19	22.7	.552	16.3	3.73	.111	.003	.00	.00	1.85	8.43	1
email_spec9_product12_true-unreach-call.cil.c	true	18.7	9.98	496164864		5	3.32	.00	.940	true	72.2	36.6	1039618048		3	7.81	.002	.014	4.99	10.7	3.77	true	15.6	8.36	463265792		.384	1.30	3.48	1.07	1.11	1.06	.838	.022	.860	.264	true	13.3	7.23	417021952		1	.439	.568	2.39	.825	.047	.012	.00	.00	.006	.097	1
email_spec9_product14_true-unreach-call.cil.c	true	24.2	13.5	571711488		5	4.18	1.64	.842	true	95.2	48.1	1584726016		3	8.92	1.59	12.3	2.59	16.3	7.41	true	544	527	972898304		2.29	512	520	3.34	511	511	19.9	484	504	492	true	49.5	32.5	887267328		14	15.5	.871	12.3	3.17	.111	.005	.00	.00	1.10	5.60	1
email_spec9_product28_true-unreach-call.cil.c	true	20.7	11.1	491352064		5	4.21	.001	.888	true	92.9	47.0	1499754496		5	9.54	.001	.005	4.12	12.6	10.8	true	16.0	8.74	480866304		.427	1.26	4.04	1.46	1.11	1.08	.861	.009	.870	.271	true	13.6	7.39	394780672		1	.517	.186	2.52	.912	.014	.001	.00	.00	.005	.072	1
email_spec9_product29_true-unreach-call.cil.c	true	31.2	17.1	708288512		5	5.67	2.71	1.44	true	122	61.7	2711949312		5	9.35	2.80	23.7	3.00	19.3	12.7	timeout	902	884	1086132224		1.72	872	878	2.71	871	871	11.0	843	854	862	true	62.8	45.5	1004945408		19	23.6	.579	17.1	4.50	.155	.001	.00	.00	1.95	8.67	1
minepump_spec1_product33_false-unreach-call.cil.c	false(reach)	8.39	4.72	343687168		1	.761	.013		false(reach)	19.9	10.3	499462144		1	.919	.065	1.55				false(reach)	9.52	5.40	376913920		.681	.278	.669	.175	.143	.129	.059	.001	.060	.048	false(reach)	8.74	4.92	341680128		1	.256	.529	.961	.190	.014	.001	.00	.00	.004	.022	1
minepump_spec1_product34_false-unreach-call.cil.c	false(reach)	8.27	4.63	343511040		1	.721	.013		false(reach)	19.1	10.0	505856000		1	.755	.047	1.57				false(reach)	8.67	4.91	367644672		.689	.207	.615	.175	.148	.138	.061	.00	.061	.039	false(reach)	8.44	4.75	344018944		1	.271	.084	.919	.614	.006	.001	.00	.00	.003	.017	1
minepump_spec1_product35_false-unreach-call.cil.c	false(reach)	8.75	4.92	359112704		1	.777	.015		false(reach)	17.7	9.30	440578048		1	.781	.044	1.48				false(reach)	8.95	5.05	376557568		.696	.221	.670	.195	.149	.133	.056	.00	.056	.035	false(reach)	8.41	4.77	332996608		1	.253	.070	.956	.208	.009	.00	.00	.00	.004	.018	1
minepump_spec1_product36_false-unreach-call.cil.c	false(reach)	8.16	4.59	346685440		1	.717	.019		false(reach)	16.6	8.70	467955712		1	.578	.039	1.09				false(reach)	8.67	4.92	371068928		.561	.236	.653	.198	.153	.143	.059	.002	.061	.043	false(reach)	8.48	4.77	342495232		1	.266	.538	.958	.225	.008	.001	.00	.00	.004	.017	1
minepump_spec1_product37_false-unreach-call.cil.c	false(reach)	8.36	4.70	347717632		1	.821	.010		false(reach)	18.4	9.67	483549184		1	.883	.087	.005				false(reach)	9.18	5.22	380293120		.738	.292	.812	.198	.183	.159	.089	.00	.089	.042	false(reach)	8.53	4.82	343502848		1	.627	.089	.649	.270	.012	.006	.00	.00	.004	.028	1
minepump_spec1_product38_false-unreach-call.cil.c	false(reach)	8.25	4.71	351748096		1	.605	.013		false(reach)	22.5	11.7	527110144		1	1.18	.104	1.63				false(reach)	8.72	4.93	384282624		.659	.254	.791	.248	.166	.156	.075	.002	.077	.049	false(reach)	8.48	4.82	346636288		1	.692	.068	.648	.266	.005	.00	.00	.00	.004	.022	1
minepump_spec1_product39_false-unreach-call.cil.c	false(reach)	8.89	5.00	356122624		1	.802	.018		false(reach)	22.4	11.7	528871424		1	1.06	.072	1.71				false(reach)	9.51	5.35	373682176		.911	.265	.826	.230	.185	.171	.083	.002	.085	.043	false(reach)	8.91	4.98	346025984		1	.320	.087	1.18	.777	.012	.008	.00	.00	.007	.037	1
minepump_spec1_product40_false-unreach-call.cil.c	false(reach)	8.87	4.93	354488320		1	.773	.019		false(reach)	21.3	11.1	511946752		1	1.27	.099	1.68				false(reach)	9.39	5.27	382128128		.737	.245	.810	.230	.164	.153	.089	.001	.090	.048	false(reach)	9.09	5.11	348635136		1	.287	.078	1.18	.304	.012	.002	.00	.00	.003	.023	1
minepump_spec1_product41_false-unreach-call.cil.c	false(reach)	9.03	5.08	366772224		2	.870	.083	.016	false(reach)	32.2	16.5	708833280		2	1.27	.338	2.50	.096	5.11	.953	false(reach)	11.0	6.17	396021760		1.09	.603	1.27	.276	.488	.467	.287	.018	.305	.178	false(reach)	9.16	5.16	359084032		2	.860	.073	.694	.294	.004	.001	.00	.00	.369	.066	1
minepump_spec1_product42_false-unreach-call.cil.c	false(reach)	9.67	5.39	372146176		2	.999	.129	.015	false(reach)	32.9	16.9	685060096		2	1.34	.363	2.53	.032	4.61	.882	false(reach)	10.7	6.05	398110720		.852	.655	1.35	.292	.564	.548	.360	.018	.378	.215	false(reach)	9.26	5.25	359710720		2	.472	.094	1.26	.817	.012	.001	.00	.00	.013	.059	1
minepump_spec1_product43_false-unreach-call.cil.c	false(reach)	9.31	5.23	363614208		2	.865	.118	.018	false(reach)	36.8	18.8	725319680		2	1.42	.404	2.67	.063	4.14	2.41	false(reach)	10.7	6.06	391446528		1.01	.654	1.35	.269	.530	.509	.307	.029	.336	.207	false(reach)	9.32	5.26	349650944		2	.862	.098	.728	.272	.013	.002	.00	.00	.011	.064	1
minepump_spec1_product44_false-unreach-call.cil.c	false(reach)	9.52	5.38	362573824		2	.910	.066	.018	false(reach)	36.9	19.0	754003968		2	1.45	.562	2.87	.231	4.75	.859	false(reach)	10.3	5.87	391409664		.891	.588	1.26	.237	.493	.479	.298	.026	.324	.194	false(reach)	9.63	5.43	363659264		2	.921	.075	.740	.261	.013	.001	.00	.00	.012	.064	1
minepump_spec1_product49_false-unreach-call.cil.c	false(reach)	9.05	5.02	351961088		1	.779	.011		false(reach)	18.8	9.78	467795968		1	1.32	.126	1.32				false(reach)	10.1	5.72	383864832		.760	.292	.902	.260	.211	.190	.101	.003	.104	.051	false(reach)	8.64	4.90	350703616		1	.285	.098	1.11	.243	.011	.001	.00	.00	.003	.029	1
minepump_spec1_product50_false-unreach-call.cil.c	false(reach)	8.95	5.00	354291712		1	.784	.014		false(reach)	22.2	11.6	495833088		1	1.15	.068	1.74				false(reach)	9.61	5.37	383787008		.781	.279	.766	.230	.189	.173	.092	.002	.094	.049	false(reach)	8.85	4.97	343040000		1	.751	.065	.709	.308	.006	.001	.00	.00	.004	.021	1
minepump_spec1_product51_false-unreach-call.cil.c	false(reach)	8.44	4.73	349540352		1	.741	.013		false(reach)	24.6	12.7	570961920		1	1.27	1.07	.009				false(reach)	9.26	5.24	374628352		.756	.280	.842	.267	.192	.175	.108	.002	.110	.046	false(reach)	9.02	5.05	349990912		1	.295	.102	1.19	.293	.006	.002	.00	.00	.003	.025	1
minepump_spec1_product52_false-unreach-call.cil.c	false(reach)	8.96	5.05	355794944		1	.832	.014		false(reach)	22.4	11.7	496160768		1	1.24	.093	1.64				false(reach)	9.49	5.34	378265600		.808	.281	.820	.241	.199	.183	.098	.003	.101	.060	false(reach)	9.02	5.09	348553216		1	.301	.502	1.10	.260	.016	.00	.00	.00	.003	.025	1
minepump_spec1_product53_false-unreach-call.cil.c	false(reach)	9.04	5.04	345522176		1	.699	.010		false(reach)	24.4	12.6	569204736		1	1.66	.092	1.61				false(reach)	11.3	6.33	391241728		.418	.359	1.68	.373	.253	.222	.122	.002	.124	.070	false(reach)	9.50	5.35	347230208		1	.328	.142	1.46	.364	.013	.001	.00	.00	.003	.029	1
minepump_spec1_product54_false-unreach-call.cil.c	false(reach)	9.18	5.08	356392960		1	.757	.010		false(reach)	25.8	13.4	581390336		1	1.56	.622	2.00				false(reach)	9.82	5.59	397475840		.335	.371	1.53	.362	.255	.220	.145	.002	.147	.064	false(reach)	9.43	5.35	355278848		1	.343	.087	1.43	.394	.017	.001	.00	.00	.003	.026	1
minepump_spec1_product55_false-unreach-call.cil.c	false(reach)	9.04	5.04	360624128		1	.784	.013		false(reach)	27.2	14.0	628162560		1	1.94	.554	2.10				false(reach)	10.1	5.67	383307776		.396	.408	1.63	.288	.278	.253	.159	.002	.161	.068	false(reach)	9.80	5.43	364650496		1	.398	.102	1.36	.834	.014	.001	.00	.00	.004	.034	1
minepump_spec1_product56_false-unreach-call.cil.c	false(reach)	9.27	5.19	360980480		1	.763	.014		false(reach)	24.2	12.5	537567232		1	1.52	.204	1.78				false(reach)	10.4	5.84	390586368		.774	.459	1.26	.330	.356	.335	.213	.003	.216	.091	false(reach)	9.89	5.50	363978752		1	.404	.107	1.47	.463	.005	.001	.00	.00	.004	.039	1
minepump_spec1_productSimulator_false-unreach-call.cil.c	false(reach)	13.8	7.45	442527744		1	1.81	.088		false(reach)	37.3	19.1	782004224		1	3.33	.350	3.06				false(reach)	16.8	9.11	458502144		1.12	1.32	3.93	1.00	.627	.588	.392	.005	.397	.198	false(reach)	12.4	6.84	397516800		1	.634	.194	2.44	.857	.025	.001	.00	.00	.004	.044	1
minepump_spec2_product33_false-unreach-call.cil.c	false(reach)	9.27	5.15	357756928		2	.898	.041	.023	false(reach)	32.5	16.7	725958656		2	1.16	.236	2.61	.095	4.06	1.49	false(reach)	9.60	5.43	386723840		.755	.588	1.14	.255	.493	.479	.263	.022	.285	.309	false(reach)	10.6	6.02	368734208		6	.606	.448	1.71	.313	.363	.350	.213	.017	.258	.155	1	.237
minepump_spec2_product34_false-unreach-call.cil.c	false(reach)	9.26	5.14	355528704		2	.864	.057	.034	false(reach)	33.3	17.1	728018944		2	1.09	.222	2.69	.133	3.16	2.82	false(reach)	10.3	5.85	379342848		.844	.529	1.18	.269	.438	.425	.238	.029	.267	.304	false(reach)	9.91	5.59	352387072		3	.491	.729	1.36	.272	.648	.637	.537	.016	.572	.077	1	.559
minepump_spec2_product35_false-unreach-call.cil.c	false(reach)	9.47	5.30	368418816		2	.916	.082	.020	false(reach)	35.4	18.2	740921344		2	1.29	.277	2.77	.105	4.81	1.50	false(reach)	10.9	6.12	392122368		.863	.563	1.26	.271	.486	.473	.270	.031	.301	.322	false(reach)	9.57	5.39	353820672		3	.464	.355	1.47	.296	.269	.266	.162	.014	.191	.073	1	.181
minepump_spec2_product36_false-unreach-call.cil.c	false(reach)	9.13	5.12	363319296		2	.931	.036	.020	false(reach)	34.8	17.9	734400512		2	1.22	.241	3.09	.334	4.17	1.38	false(reach)	10.6	5.97	391897088		.868	.591	1.20	.257	.486	.477	.267	.034	.301	.321	false(reach)	9.67	5.49	357404672		3	.492	.760	1.39	.228	.637	.629	.136	.015	.168	.077	1	.159
minepump_spec2_product41_false-unreach-call.cil.c	false(reach)	10.1	5.66	368726016		3	1.07	.118	.063	false(reach)	53.0	27.1	929972224		3	1.73	.570	4.55	1.22	7.80	5.82	false(reach)	11.8	6.61	409071616		.905	.977	1.97	.381	.875	.847	.561	.043	.604	.639	false(reach)	12.1	6.97	383098880		8	1.00	.681	2.29	.882	.576	.562	.368	.036	.445	.324	1	.409
minepump_spec2_product42_false-unreach-call.cil.c	false(reach)	10.4	5.81	375857152		3	1.21	.105	.065	false(reach)	48.7	25.0	909230080		3	1.84	.747	4.57	1.29	7.33	4.49	false(reach)	11.6	6.55	409567232		.880	.893	1.95	.390	.775	.728	.433	.046	.479	.507	false(reach)	11.6	6.59	369524736		5	.747	.554	2.02	.901	.460	.449	.296	.027	.353	.194	1	.334
minepump_spec2_product43_false-unreach-call.cil.c	false(reach)	10.2	5.74	384045056		3	1.16	.117	.075	false(reach)	50.0	25.6	944562176		3	1.94	.758	4.44	1.33	8.21	4.37	false(reach)	11.6	6.52	402952192		.878	1.01	1.92	.341	.860	.842	.474	.085	.559	.616	false(reach)	10.8	6.21	372719616		5	.740	.963	1.90	.390	.468	.451	.304	.018	.348	.184	1	.329
minepump_spec2_product44_false-unreach-call.cil.c	false(reach)	10.1	5.64	375189504		3	1.14	.116	.076	false(reach)	54.9	28.0	949317632		3	1.79	.870	5.04	1.34	8.19	5.91	false(reach)	12.4	6.97	413966336		.971	1.23	2.21	.376	1.08	1.06	.600	.123	.723	.774	false(reach)	11.3	6.49	369356800		5	.787	.579	1.98	.354	.485	.471	.318	.025	.372	.186	1	.350
minepump_spec2_productSimulator_false-unreach-call.cil.c	false(reach)	16.0	8.71	495931392		2	2.73	.072	.222	false(reach)	63.1	32.0	1431203840		2	4.30	.183	7.24	.408	14.2	.657	false(reach)	21.5	11.7	518885376		1.25	1.83	5.79	1.33	1.43	1.36	.823	.125	.948	.970	false(reach)	19.9	10.8	471883776		3	2.02	1.21	4.39	1.38	1.04	1.01	.636	.042	.697	.159	1	.698
minepump_spec3_product01_false-unreach-call.cil.c	false(reach)	8.03	4.53	342532096		1	.648	.013		false(reach)	12.0	6.41	378494976		1	.598	.010	.014				false(reach)	8.73	4.90	366080000		.617	.170	.548	.180	.120	.108	.032	.001	.033	.031	false(reach)	8.12	4.62	331886592		1	.226	.050	.823	.188	.008	.002	.00	.00	.007	.023	1
minepump_spec3_product02_false-unreach-call.cil.c	false(reach)	8.59	4.82	342536192		1	.879	.009		false(reach)	14.6	7.71	442228736		1	.619	.012	.009				false(reach)	8.89	5.00	365936640		.691	.162	.507	.136	.106	.100	.036	.001	.037	.040	false(reach)	8.37	4.71	327770112		1	.228	.052	.976	.163	.006	.00	.00	.00	.018	.598	1
minepump_spec3_product03_false-unreach-call.cil.c	false(reach)	8.44	4.71	339189760		1	.796	.008		false(reach)	15.9	8.38	441159680		1	.660	.022	1.15				false(reach)	8.25	4.68	373682176		.660	.159	.493	.146	.105	.101	.034	.003	.037	.041	false(reach)	8.17	4.60	340193280		1	.217	.034	.798	.188	.006	.001	.00	.00	.007	.417	1
minepump_spec3_product04_false-unreach-call.cil.c	false(reach)	8.35	4.69	345960448		1	.734	.008		false(reach)	19.1	10.0	471752704		1	.726	.038	.010				false(reach)	8.50	4.79	362082304		.715	.167	.535	.180	.110	.100	.039	.001	.040	.033	false(reach)	8.38	4.67	332447744		1	.709	.038	.445	.206	.007	.001	.00	.00	.006	.043	1
minepump_spec3_product05_false-unreach-call.cil.c	false(reach)	8.28	4.63	336416768		1	.678	.008		false(reach)	16.7	8.79	448544768		1	.550	.022	.008				false(reach)	8.70	4.91	368144384		.666	.229	.650	.177	.152	.129	.062	.00	.062	.040	false(reach)	8.44	4.77	336523264		1	.266	.097	.889	.593	.011	.001	.00	.00	.009	.028	1
minepump_spec3_product06_false-unreach-call.cil.c	false(reach)	8.37	4.69	342282240		1	.630	.009		false(reach)	16.9	8.93	475652096		1	.539	.016	1.14				false(reach)	8.91	5.02	369745920		.613	.226	.617	.166	.127	.119	.049	.001	.050	.031	false(reach)	8.29	4.62	340041728		1	.737	.050	.459	.180	.006	.001	.00	.00	.007	.025	1
minepump_spec3_product07_false-unreach-call.cil.c	false(reach)	8.32	4.66	345796608		1	.683	.010		false(reach)	14.2	7.47	379543552		1	.446	.034	.004				false(reach)	8.58	4.82	376242176		.646	.211	.641	.186	.136	.130	.060	.001	.061	.047	false(reach)	8.97	4.99	338944000		1	.279	.084	.980	.191	.016	.002	.00	.00	.007	.026	1
minepump_spec3_product08_false-unreach-call.cil.c	false(reach)	8.60	4.79	346136576		1	.708	.010		false(reach)	21.1	11.1	520409088		1	.862	.345	1.83				false(reach)	9.04	5.10	375398400		.741	.230	.632	.170	.138	.129	.051	.001	.052	.036	false(reach)	8.55	4.82	336850944		1	.710	.059	.433	.184	.010	.001	.00	.00	.007	.021	1
minepump_spec3_product09_false-unreach-call.cil.c	false(reach)	8.34	4.69	332660736		1	.728	.015		false(reach)	16.6	8.81	506097664		1	.801	.010	1.25				false(reach)	8.50	4.78	373280768		.611	.173	.526	.164	.109	.096	.035	.00	.035	.037	false(reach)	8.06	4.55	343404544		1	.216	.056	.764	.530	.010	.00	.00	.00	.009	.024	1
minepump_spec3_product10_false-unreach-call.cil.c	false(reach)	8.40	4.75	344764416		1	.697	.009		false(reach)	17.5	9.22	488947712		1	.676	.013	.011				false(reach)	9.30	5.17	368496640		.708	.148	.548	.169	.098	.093	.037	.001	.038	.034	false(reach)	8.35	4.71	335159296		1	.596	.049	.409	.147	.009	.001	.00	.00	.007	.045	1
minepump_spec3_product11_false-unreach-call.cil.c	false(reach)	8.47	4.78	339021824		1	.695	.006		false(reach)	15.5	8.20	449306624		1	.699	.024	1.18				false(reach)	8.64	4.84	365821952		.644	.153	.514	.192	.100	.091	.035	.00	.035	.031	false(reach)	7.47	4.27	333778944		1	.484	.046	.388	.159	.014	.002	.00	.00	.008	.027	1
minepump_spec3_product12_false-unreach-call.cil.c	false(reach)	8.55	4.77	349843456		1	.738	.008		false(reach)	15.4	8.11	421949440		1	.584	.020	.006				false(reach)	8.43	4.74	364736512		.663	.166	.548	.184	.110	.103	.030	.002	.032	.039	false(reach)	8.38	4.70	340058112		1	.263	.043	.802	.171	.005	.001	.00	.00	.011	.034	1
minepump_spec3_product13_false-unreach-call.cil.c	false(reach)	8.70	4.86	343842816		1	.834	.008		false(reach)	17.7	9.40	494448640		1	.908	.040	1.35				false(reach)	8.61	4.80	373133312		.642	.236	.593	.144	.175	.157	.087	.00	.087	.056	false(reach)	8.55	4.84	331755520		1	.305	.070	.995	.206	.006	.001	.00	.00	.009	.027	1
minepump_spec3_product14_false-unreach-call.cil.c	false(reach)	8.13	4.60	337100800		1	.689	.009		false(reach)	18.1	9.55	494260224		1	.758	.040	1.54				false(reach)	8.84	4.99	373764096		.687	.239	.630	.180	.172	.149	.054	.002	.056	.056	false(reach)	7.71	4.35	333783040		1	.265	.047	.755	.219	.006	.001	.00	.00	.006	.027	1
minepump_spec3_product15_false-unreach-call.cil.c	false(reach)	8.38	4.70	347385856		1	.660	.010		false(reach)	17.4	9.15	469880832		1	.707	.104	.012				false(reach)	8.99	5.09	363335680		.640	.199	.609	.146	.126	.120	.060	.002	.062	.037	false(reach)	8.42	4.74	339877888		1	.262	.077	.921	.191	.009	.002	.00	.00	.006	.029	1
minepump_spec3_product16_false-unreach-call.cil.c	false(reach)	8.14	4.62	342675456		1	.698	.013		false(reach)	19.3	10.2	511406080		1	.980	.114	.004				false(reach)	8.93	5.07	370274304		.615	.210	.666	.200	.148	.137	.051	.00	.051	.042	false(reach)	8.43	4.75	337145856		1	.258	.050	1.00	.201	.008	.001	.00	.00	.010	.022	1
minepump_spec3_product17_false-unreach-call.cil.c	false(reach)	8.86	4.96	345550848		1	.794	.008		false(reach)	16.9	8.96	429142016		1	.639	.010	1.32				false(reach)	8.79	4.93	377737216		.843	.208	.610	.180	.134	.127	.066	.00	.066	.040	false(reach)	8.60	4.81	342663168		1	.299	.065	.957	.705	.009	.001	.00	.00	.011	.022	1
minepump_spec3_product18_false-unreach-call.cil.c	false(reach)	8.44	4.76	341327872		1	.737	.009		false(reach)	15.7	8.35	436195328		1	.737	.011	1.13				false(reach)	8.40	4.71	371609600		.586	.197	.582	.149	.137	.130	.058	.00	.058	.045	false(reach)	8.10	4.59	343691264		1	.267	.106	.910	.190	.010	.001	.00	.00	.012	.031	1
minepump_spec3_product19_false-unreach-call.cil.c	false(reach)	8.65	4.86	343998464		1	.705	.012		false(reach)	19.3	10.1	518688768		1	.859	.021	1.64				false(reach)	8.46	4.81	377040896		.603	.216	.638	.204	.149	.138	.062	.00	.062	.041	false(reach)	8.75	4.89	341086208		1	.309	.087	.980	.219	.013	.001	.00	.00	.013	.023	1
minepump_spec3_product20_false-unreach-call.cil.c	false(reach)	8.55	4.82	345579520		1	.721	.012		false(reach)	19.5	10.3	501559296		1	.965	.079	.004				false(reach)	8.25	4.68	374272000		.540	.194	.645	.225	.141	.131	.062	.001	.063	.041	false(reach)	8.36	4.76	335437824		1	.715	.081	.538	.215	.009	.001	.00	.00	.006	.022	1
minepump_spec3_product21_false-unreach-call.cil.c	false(reach)	8.08	4.51	346382336		1	.589	.010		false(reach)	19.0	9.97	468406272		1	.847	.079	1.46				false(reach)	9.70	5.44	385732608		.771	.298	.881	.245	.199	.188	.099	.001	.100	.049	false(reach)	8.82	4.96	344109056		1	.279	.093	1.17	.748	.017	.002	.00	.00	.006	.033	1
minepump_spec3_product22_false-unreach-call.cil.c	false(reach)	8.77	4.91	345690112		1	.709	.017		false(reach)	19.4	10.1	489570304		1	.800	.026	1.52				false(reach)	9.07	5.11	380411904		.739	.230	.746	.220	.163	.155	.079	.00	.079	.045	false(reach)	8.85	5.03	343552000		1	.276	.527	1.10	.265	.019	.001	.00	.00	.006	.032	1
minepump_spec3_product23_false-unreach-call.cil.c	false(reach)	8.84	4.89	346255360		1	.784	.009		false(reach)	21.8	11.4	526172160		1	1.09	.041	1.91				false(reach)	8.78	5.00	380293120		.568	.255	.812	.232	.190	.158	.085	.00	.085	.049	false(reach)	8.47	4.76	345993216		1	.616	.078	.637	.268	.014	.001	.00	.00	.005	.031	1
minepump_spec3_product24_false-unreach-call.cil.c	false(reach)	9.12	5.10	349876224		1	.837	.016		false(reach)	15.0	7.82	399253504		1	.977	.048	1.02				false(reach)	8.81	4.99	373694464		.672	.254	.762	.222	.174	.162	.082	.002	.084	.047	false(reach)	9.17	5.17	345014272		1	.815	.108	.650	.281	.006	.001	.00	.00	.006	.025	1
minepump_spec3_product25_false-unreach-call.cil.c	false(reach)	8.79	4.87	346308608		1	.820	.007		false(reach)	17.5	9.24	469716992		1	.733	.105	1.27				false(reach)	8.96	5.04	377188352		.800	.222	.621	.175	.154	.148	.053	.001	.054	.036	false(reach)	8.44	4.76	340000768		1	.264	.071	.952	.181	.006	.001	.00	.00	.007	.036	1
minepump_spec3_product26_false-unreach-call.cil.c	false(reach)	8.30	4.68	341864448		1	.672	.006		false(reach)	16.9	9.01	447242240		1	.649	.010	.003				false(reach)	8.94	5.03	373682176		.617	.214	.630	.194	.153	.148	.069	.002	.071	.044	false(reach)	8.34	4.74	343310336		1	.269	.060	.938	.218	.012	.001	.00	.00	.012	.022	1
minepump_spec3_product27_false-unreach-call.cil.c	false(reach)	8.16	4.58	346140672		1	.727	.007		false(reach)	17.0	8.95	446636032		1	.653	.012	.013				false(reach)	8.64	4.94	365625344		.608	.230	.637	.162	.140	.119	.057	.001	.058	.036	false(reach)	8.46	4.80	342106112		1	.292	.075	.906	.592	.008	.001	.00	.00	.012	.026	1
minepump_spec3_product28_false-unreach-call.cil.c	false(reach)	8.33	4.64	353726464		1	.635	.016		false(reach)	16.5	8.61	395603968		1	.715	.028	1.19				false(reach)	8.63	4.89	369618944		.673	.246	.659	.195	.182	.172	.080	.002	.082	.062	false(reach)	8.64	4.88	340717568		1	.726	.071	.517	.213	.009	.001	.00	.00	.462	.034	1
minepump_spec3_product29_false-unreach-call.cil.c	false(reach)	8.37	4.70	351051776		1	.545	.008		false(reach)	20.0	10.4	506298368		1	.980	.267	1.54				false(reach)	9.50	5.31	379166720		.704	.250	.820	.252	.174	.162	.073	.001	.074	.044	false(reach)	8.86	4.98	342876160		1	.296	.505	1.14	.286	.007	.001	.00	.00	.006	.029	1
minepump_spec3_product30_false-unreach-call.cil.c	false(reach)	8.54	4.79	346173440		1	.787	.008		false(reach)	19.2	10.1	518393856		1	1.06	.041	1.46				false(reach)	8.92	5.07	374788096		.646	.266	.752	.223	.176	.160	.089	.00	.089	.049	false(reach)	9.05	5.08	341221376		1	.735	.070	.666	.288	.012	.002	.00	.00	.007	.026	1
minepump_spec3_product31_false-unreach-call.cil.c	false(reach)	8.57	4.83	346456064		1	.717	.010		false(reach)	19.7	10.3	484200448		1	1.16	.024	1.52				false(reach)	9.43	5.33	379379712		.705	.268	.875	.265	.197	.191	.108	.001	.109	.044	false(reach)	8.80	4.94	346411008		1	.707	.083	.647	.249	.020	.003	.00	.00	.005	.035	1
minepump_spec3_product32_false-unreach-call.cil.c	false(reach)	8.78	4.92	347693056		1	.796	.009		false(reach)	17.9	9.42	490405888		1	.741	.052	.005				false(reach)	9.91	5.57	384032768		.766	.272	.848	.258	.182	.173	.091	.002	.093	.063	false(reach)	8.91	4.96	344215552		1	.733	.116	.730	.263	.011	.00	.00	.00	.007	.029	1
minepump_spec3_product35_false-unreach-call.cil.c	false(reach)	8.87	4.98	349995008		1	.818	.020		false(reach)	16.0	8.46	409272320		1	.602	.072	1.08				false(reach)	9.16	5.24	376324096		.692	.305	.763	.203	.226	.213	.096	.009	.105	.087	false(reach)	8.43	4.72	336261120		1	.278	.049	.901	.629	.008	.001	.00	.00	.008	.029	1
minepump_spec3_product36_false-unreach-call.cil.c	false(reach)	8.63	4.88	349569024		1	.635	.013		false(reach)	19.3	10.2	479141888		1	.854	.094	.016				false(reach)	9.00	5.09	376283136		.593	.286	.754	.214	.219	.208	.111	.011	.122	.073	false(reach)	9.01	5.05	343322624		1	.763	.081	.562	.219	.009	.001	.00	.00	.477	.036	1
minepump_spec3_product39_false-unreach-call.cil.c	false(reach)	8.89	4.95	355106816		1	.807	.012		false(reach)	18.7	9.77	430440448		1	.978	.150	1.30				false(reach)	9.91	5.53	384831488		.842	.404	1.00	.259	.286	.275	.163	.012	.175	.078	false(reach)	8.87	4.99	348766208		1	.303	.464	1.11	.311	.009	.002	.00	.00	.016	.045	1
minepump_spec3_product40_false-unreach-call.cil.c	false(reach)	8.45	4.74	354152448		1	.692	.018		false(reach)	25.1	13.0	537047040		1	1.72	.953	1.95				false(reach)	9.95	5.54	380502016		.684	.403	1.09	.275	.291	.278	.149	.020	.169	.099	false(reach)	9.15	5.15	345526272		1	.322	.092	1.17	.769	.017	.001	.00	.00	.013	.035	1
minepump_spec3_product43_false-unreach-call.cil.c	false(reach)	8.83	4.93	345788416		1	.774	.020		false(reach)	20.7	10.8	520548352		1	.935	.086	1.59				false(reach)	8.95	5.10	377204736		.657	.326	.856	.242	.239	.229	.128	.013	.141	.079	false(reach)	8.87	5.02	343502848		1	.691	.080	.544	.201	.012	.002	.00	.00	.374	.029	1
minepump_spec3_product44_false-unreach-call.cil.c	false(reach)	9.11	5.06	351698944		1	.890	.014		false(reach)	23.3	12.1	562802688		1	1.25	.627	2.03				false(reach)	9.16	5.10	386478080		.699	.352	.833	.196	.281	.271	.149	.018	.167	.091	false(reach)	8.84	4.99	346116096		1	.293	.496	1.06	.238	.437	.00	.00	.00	.007	.030	1
minepump_spec3_product47_false-unreach-call.cil.c	false(reach)	8.70	4.87	355926016		1	.873	.023		false(reach)	24.3	12.7	560128000		1	1.10	.378	2.02				false(reach)	10.8	6.06	397955072		.826	.539	1.36	.356	.429	.414	.269	.022	.291	.150	false(reach)	9.22	5.21	349655040		1	.345	.092	1.26	.342	.014	.003	.00	.00	.010	.034	1
minepump_spec3_product48_false-unreach-call.cil.c	false(reach)	8.92	5.00	344625152		1	.805	.023		false(reach)	23.0	12.0	537276416		1	1.36	.142	.005				false(reach)	9.67	5.53	386269184		.719	.460	1.17	.320	.306	.295	.157	.018	.175	.090	false(reach)	9.22	5.21	349319168		1	.332	.101	1.29	.384	.017	.003	.00	.00	.013	.037	1
minepump_spec3_product51_false-unreach-call.cil.c	false(reach)	8.47	4.76	351326208		1	.771	.013		false(reach)	24.4	12.7	543920128		1	1.34	.615	.011				false(reach)	10.4	5.82	380755968		.838	.302	1.00	.316	.200	.191	.104	.002	.106	.049	false(reach)	9.22	5.22	362717184		1	.372	.116	1.15	.728	.017	.002	.00	.00	.008	.043	0
minepump_spec3_product52_false-unreach-call.cil.c	false(reach)	9.17	5.09	356892672		1	.965	.013		false(reach)	21.8	11.4	519577600		1	1.29	.080	.007				false(reach)	8.99	5.06	386097152		.694	.293	.871	.254	.179	.159	.082	.002	.084	.053	false(reach)	8.98	5.06	353955840		1	.374	.085	1.25	.345	.016	.001	.00	.00	.010	.044	0
minepump_spec3_product55_false-unreach-call.cil.c	false(reach)	8.88	4.96	353955840		1	.750	.012		false(reach)	23.5	12.2	541417472		1	1.77	.286	1.70				false(reach)	10.5	5.85	394932224		.797	.428	1.31	.356	.264	.231	.130	.002	.132	.062	false(reach)	10.2	5.67	362135552		1	.487	.195	1.53	.811	.021	.001	.00	.00	.011	.054	0
minepump_spec3_product56_false-unreach-call.cil.c	false(reach)	8.77	4.93	359727104		1	.709	.012		false(reach)	23.7	12.3	570445824		1	1.72	.374	1.70				false(reach)	10.3	5.75	397209600		.363	.392	1.62	.719	.257	.242	.143	.001	.144	.061	false(reach)	10.4	5.86	366272512		1	.574	.106	1.56	.932	.015	.002	.00	.00	.009	.049	0
minepump_spec3_product59_false-unreach-call.cil.c	false(reach)	9.17	5.12	350822400		1	.889	.025		false(reach)	23.9	12.5	563150848		1	1.68	.217	1.86				false(reach)	10.2	5.73	387387392		.786	.368	1.04	.247	.266	.258	.168	.004	.172	.079	false(reach)	9.75	5.51	357441536		1	.451	.110	1.31	.354	.019	.001	.00	.00	.007	.052	0
minepump_spec3_product60_false-unreach-call.cil.c	false(reach)	8.63	4.86	359591936		1	.659	.024		false(reach)	21.5	11.2	571543552		1	1.19	.081	1.69				false(reach)	9.84	5.51	386781184		.618	.366	1.07	.336	.264	.253	.132	.004	.136	.078	false(reach)	9.27	5.20	358400000		1	.451	.085	1.20	.723	.019	.002	.00	.00	.007	.053	0
minepump_spec3_product63_false-unreach-call.cil.c	false(reach)	9.07	5.04	362483712		1	.765	.025		false(reach)	25.1	13.0	592371712		1	1.58	.151	.011				false(reach)	10.5	5.88	396488704		.398	.440	1.83	.798	.306	.276	.173	.002	.175	.061	false(reach)	10.6	5.90	376471552		1	1.04	.205	1.25	.448	.059	.001	.00	.00	.007	.064	0
minepump_spec3_product64_false-unreach-call.cil.c	false(reach)	9.59	5.32	357842944		1	.839	.037		false(reach)	25.5	13.2	568262656		1	1.70	.458	1.87				false(reach)	10.4	5.82	399568896		.390	.411	1.80	.758	.292	.252	.153	.002	.155	.102	false(reach)	10.7	6.01	377114624		1	.472	.146	1.94	1.14	.013	.001	.00	.00	.009	.066	0
minepump_spec3_productSimulator_false-unreach-call.cil.c	false(reach)	12.6	6.88	423698432		1	1.39	.045		false(reach)	35.6	18.3	788115456		1	3.75	.358	3.21				false(reach)	14.4	7.88	430477312		.924	.607	2.99	1.16	.444	.399	.245	.00	.245	.017	false(reach)	12.9	7.12	413696000		0	1.14	.175	2.05	.850	.025	.002	.00	.00	.006	.017
minepump_spec4_product33_false-unreach-call.cil.c	false(reach)	9.85	5.48	370249728		3	.998	.145	.042	false(reach)	41.2	21.0	820592640		3	1.33	.628	2.97	.439	5.55	1.79	false(reach)	10.5	5.92	381878272		.855	.574	1.22	.268	.445	.427	.222	.035	.257	.125	false(reach)	10.0	5.72	357601280		3	.712	.441	1.23	.306	.024	.002	.00	.00	.038	.110	0
minepump_spec4_product34_false-unreach-call.cil.c	false(reach)	9.61	5.39	365346816		3	.964	.095	.043	false(reach)	43.7	22.2	869228544		3	1.43	.702	3.37	.305	4.80	4.71	false(reach)	10.9	6.03	394899456		.861	.527	1.22	.300	.423	.405	.213	.024	.237	.101	false(reach)	10.1	5.64	353472512		3	.738	.083	1.29	.759	.023	.002	.00	.00	.035	.115	0
minepump_spec4_product35_false-unreach-call.cil.c	false(reach)	9.88	5.54	368754688		3	.975	.202	.055	false(reach)	44.7	22.8	893317120		3	2.19	.807	3.60	.488	6.65	2.57	false(reach)	10.4	5.95	384954368		.842	.582	1.27	.277	.490	.479	.263	.044	.307	.143	false(reach)	10.1	5.74	355172352		3	.723	.096	1.31	.370	.012	.001	.00	.00	.038	.119	0
minepump_spec4_product36_false-unreach-call.cil.c	false(reach)	9.70	5.40	367865856		3	.947	.180	.064	false(reach)	44.6	22.8	860893184		3	1.47	1.02	3.29	.565	6.62	1.88	false(reach)	11.1	6.21	397824000		.979	.649	1.29	.271	.561	.527	.289	.050	.339	.166	false(reach)	9.61	5.55	370417664		4	.722	.106	1.18	.301	.014	.001	.00	.00	.035	.123	1
minepump_spec4_product37_false-unreach-call.cil.c	false(reach)	10.2	5.68	384135168		3	1.17	.086	.045	false(reach)	49.1	25.0	1100996608		3	2.05	.829	3.85	.482	8.55	2.75	false(reach)	11.0	6.23	405229568		.917	.639	1.58	.403	.524	.506	.300	.025	.325	.109	false(reach)	10.8	6.14	366448640		3	.853	.102	1.57	.439	.012	.001	.00	.00	.045	.123	0
minepump_spec4_product38_false-unreach-call.cil.c	false(reach)	9.95	5.57	374902784		3	1.14	.085	.044	false(reach)	51.0	25.9	935854080		3	1.84	.855	4.27	.507	8.71	3.27	false(reach)	11.4	6.45	409071616		1.05	.602	1.55	.383	.476	.462	.268	.030	.298	.108	false(reach)	10.9	6.18	375779328		3	.806	.150	1.65	.441	.020	.002	.00	.00	.029	.125	0
minepump_spec4_product39_false-unreach-call.cil.c	false(reach)	10.0	5.58	381956096		3	1.12	.135	.055	false(reach)	55.7	28.3	920866816		3	2.76	1.43	4.60	.930	9.03	3.22	false(reach)	11.0	6.19	405409792		1.03	.721	1.52	.327	.616	.589	.352	.047	.399	.144	false(reach)	11.1	6.27	368783360		3	1.34	.117	1.16	.469	.015	.002	.00	.00	.048	.134	0
minepump_spec4_product40_false-unreach-call.cil.c	false(reach)	10.1	5.64	382054400		3	1.16	.147	.053	false(reach)	52.8	26.8	1138966528		3	2.54	1.10	4.25	.822	9.06	2.78	false(reach)	12.4	7.01	419852288		1.17	.827	1.89	.464	.655	.620	.361	.052	.413	.130	false(reach)	10.7	6.07	371396608		3	.835	.103	1.61	.398	.023	.003	.00	.00	.027	.128	0
minepump_spec4_product41_false-unreach-call.cil.c	false(reach)	9.73	5.47	364851200		3	.999	.190	.057	false(reach)	48.8	24.9	916402176		3	1.65	.933	4.33	.487	7.84	2.78	false(reach)	10.2	5.77	394342400		.839	.625	1.33	.303	.526	.509	.293	.038	.331	.128	false(reach)	10.1	5.72	363511808		3	1.24	.114	.865	.312	.022	.002	.00	.00	.444	.116	0
minepump_spec4_product42_false-unreach-call.cil.c	false(reach)	9.50	5.35	369053696		3	1.01	.148	.050	false(reach)	46.3	23.5	904593408		3	1.63	.933	3.75	.553	7.46	3.04	false(reach)	11.5	6.47	399556608		1.15	.675	1.37	.309	.579	.562	.330	.046	.376	.171	false(reach)	10.5	6.00	363585536		3	.827	.085	1.45	.871	.014	.001	.00	.00	.039	.127	0
minepump_spec4_product43_false-unreach-call.cil.c	false(reach)	9.74	5.48	373583872		3	1.13	.168	.055	false(reach)	47.8	24.3	925958144		3	1.48	1.23	.018	.718	7.31	3.29	false(reach)	10.8	6.13	404533248		1.08	.617	1.34	.283	.532	.510	.300	.068	.368	.152	false(reach)	10.6	6.01	360443904		4	.820	.117	1.41	.734	.019	.001	.00	.00	.048	.136	1
minepump_spec4_product44_false-unreach-call.cil.c	false(reach)	10.0	5.65	376356864		3	1.12	.149	.058	false(reach)	48.2	24.6	915828736		3	1.63	1.14	3.79	.651	5.92	3.57	false(reach)	11.4	6.47	398708736		.941	.670	1.43	.339	.582	.561	.293	.082	.375	.175	false(reach)	10.4	5.94	373780480		3	1.27	.080	.951	.343	.014	.006	.00	.00	.055	.128	0
minepump_spec4_product45_false-unreach-call.cil.c	false(reach)	10.6	5.98	385454080		3	1.24	.185	.054	false(reach)	50.3	25.6	910041088		3	2.13	.969	.008	.599	9.63	3.17	false(reach)	11.5	6.52	418172928		.921	.759	1.86	.469	.655	.632	.400	.040	.440	.190	false(reach)	10.9	6.30	367398912		3	.954	.143	1.69	.444	.022	.003	.00	.00	.042	.166	0
minepump_spec4_product46_false-unreach-call.cil.c	false(reach)	10.2	5.70	380956672		3	1.25	.144	.052	false(reach)	49.3	25.1	902864896		3	1.84	.707	4.60	.624	10.4	2.80	false(reach)	11.9	6.71	417288192		1.00	.895	1.92	.471	.753	.735	.453	.087	.540	.234	false(reach)	11.1	6.37	381952000		3	1.00	.126	1.64	.402	.021	.001	.00	.00	.038	.137	0
minepump_spec4_product47_false-unreach-call.cil.c	false(reach)	10.5	5.86	379068416		3	1.16	.176	.066	false(reach)	56.6	28.8	1327972352		3	2.04	1.34	5.03	.978	10.2	4.32	false(reach)	12.5	7.01	420913152		.964	.986	2.15	.481	.852	.825	.494	.120	.614	.237	false(reach)	10.7	6.15	380829696		4	.975	.148	1.65	.431	.013	.002	.00	.00	.044	.183	1
minepump_spec4_product48_false-unreach-call.cil.c	false(reach)	10.7	6.00	396910592		3	1.22	.269	.061	false(reach)	51.7	26.3	933138432		3	2.02	.684	4.63	.651	10.6	2.77	false(reach)	12.0	6.78	417288192		1.05	1.02	2.01	.402	.875	.852	.502	.103	.605	.246	false(reach)	11.0	6.36	388468736		3	.992	.159	1.58	.485	.025	.003	.00	.00	.040	.163	0
minepump_spec4_productSimulator_false-unreach-call.cil.c	false(reach)	17.0	9.45	504057856		3	2.79	.303	.169	false(reach)	81.6	41.2	1407119360		3	5.15	1.17	9.72	.812	19.0	2.56	false(reach)	21.3	12.0	515596288		1.12	2.21	5.86	1.09	1.94	1.85	.853	.626	1.48	.907	false(reach)	21.8	12.1	494940160		3	2.51	.298	4.54	1.95	.041	.002	.00	.00	.041	.236	0
minepump_spec1_product01_true-unreach-call.cil.c	timeout	906	892	5112897536		206	4.87	.022	878	true	10.5	5.64	364756992		1	.669	.00	.005	.089			true	8.01	4.46	332681216		.432	.147	.496	.138	.111	.104	.032	.001	.033	.038	true	7.67	4.26	303235072		2	.093	.062	.815	.177	.004	.002	.00	.00	.002	.450	2
minepump_spec1_product02_true-unreach-call.cil.c	timeout	905	887	3503267840		173	4.68	.015	874	true	10.6	5.67	355479552		1	.555	.00	.005	.071			true	8.00	4.44	330285056		.509	.145	.480	.173	.092	.085	.035	.002	.037	.036	true	7.57	4.22	300810240		2	.093	.053	.390	.178	.007	.001	.00	.00	.003	.025	2
minepump_spec1_product03_true-unreach-call.cil.c	timeout	905	889	3665260544		184	4.74	.010	876	true	11.4	6.14	362536960		1	.695	.00	.008	.082			true	7.99	4.45	332062720		.473	.168	.549	.172	.101	.093	.035	.003	.038	.034	true	8.06	4.48	306511872		2	.101	.069	.410	.164	.012	.003	.00	.00	.003	.038	2
minepump_spec1_product04_true-unreach-call.cil.c	timeout	905	892	3320442880		169	4.75	.012	878	true	10.8	5.79	389267456		1	.663	.001	.005	.374			true	7.57	4.25	338796544		.413	.167	.523	.157	.110	.101	.042	.002	.044	.038	true	8.11	4.51	309809152		2	.095	.058	.380	.141	.009	.001	.00	.00	.002	.030	2
minepump_spec1_product05_true-unreach-call.cil.c	timeout	906	892	5105774592		201	4.87	.010	877	true	10.9	5.85	333643776		1	.475	.00	.004	.106			true	8.81	4.93	357322752		.492	.478	1.04	.229	.378	.368	.210	.010	.220	.160	true	8.60	4.77	312549376		4	.280	.072	1.15	.748	.011	.002	.00	.00	.015	.103	2
minepump_spec1_product06_true-unreach-call.cil.c	timeout	905	891	3511189504		179	4.66	.014	878	true	10.9	5.84	351379456		1	.559	.00	.005	.024			true	8.76	4.94	350150656		.470	.425	.962	.260	.340	.322	.174	.013	.187	.123	true	8.81	4.92	312340480		5	.740	.071	.712	.258	.012	.002	.00	.00	.020	.130	3
minepump_spec1_product07_true-unreach-call.cil.c	timeout	912	898	5123010560		184	4.95	.018	884	true	11.7	6.28	391536640		1	.785	.00	.006	.036			true	9.20	5.06	354828288		.548	.488	1.06	.226	.407	.381	.238	.012	.250	.142	true	8.66	4.87	318222336		4	.248	.093	1.13	.619	.013	.002	.00	.00	.019	.119	2
minepump_spec1_product08_true-unreach-call.cil.c	timeout	906	891	5129388032		185	5.01	.015	877	true	13.6	7.24	427380736		1	.558	.017	.009	.028			true	9.50	5.31	353869824		.563	.587	1.14	.199	.474	.456	.253	.023	.276	.201	true	8.27	4.65	316833792		4	.637	.076	.665	.255	.025	.001	.00	.00	.019	.106	2
minepump_spec1_product09_true-unreach-call.cil.c	timeout	906	888	5167390720		203	4.88	.012	874	true	10.1	5.43	342548480		1	.467	.00	.007	.037			true	7.82	4.36	334012416		.449	.161	.512	.146	.107	.095	.031	.002	.033	.039	true	7.23	4.09	297619456		2	.107	.395	.730	.177	.011	.001	.00	.00	.004	.027	2
minepump_spec1_product10_true-unreach-call.cil.c	timeout	905	891	3484340224		176	4.62	.012	878	true	10.2	5.49	353697792		1	.569		.005				true	8.00	4.51	338628608		.457	.165	.539	.166	.113	.102	.037	.001	.038	.041	true	7.76	4.32	301113344		2	.098	.046	.399	.168	.006	.003	.00	.00	.004	.024	2
minepump_spec1_product11_true-unreach-call.cil.c	timeout	905	891	3713310720		188	4.70	.009	877	true	12.0	6.37	376782848		1	.420	.001	.004	.030	1.17	.176	true	7.79	4.36	337117184		.437	.176	.497	.139	.108	.102	.051	.00	.051	.049	true	7.97	4.43	302362624		2	.105	.067	.418	.177	.009	.002	.00	.00	.003	.027	2
minepump_spec1_product12_true-unreach-call.cil.c	timeout	904	887	3343417344		165	4.52	.010	874	true	11.3	6.07	399921152		1	.744	.00	.020	.066			true	7.74	4.38	328744960		.557	.160	.509	.123	.107	.082	.036	.002	.038	.033	true	8.16	4.52	307003392		2	.093	.051	.954	.689	.007	.001	.00	.00	.003	.035	2
minepump_spec1_product13_true-unreach-call.cil.c	timeout	906	892	5091307520		205	5.02	.014	877	true	10.7	5.80	349556736		1	.765	.00	.005	.060			true	9.22	5.10	346091520		.594	.443	1.03	.228	.337	.327	.171	.010	.181	.133	true	8.44	4.74	317841408		4	.238	.096	1.17	.279	.017	.001	.00	.00	.017	.542	2
minepump_spec1_product14_true-unreach-call.cil.c	timeout	905	891	3534557184		179	4.74	.010	878	true	11.4	6.11	356323328		1	.643	.00	.005	.054			true	8.85	4.94	352591872		.522	.479	.978	.202	.363	.333	.206	.009	.215	.123	true	8.39	4.69	311517184		5	.281	.076	1.08	.624	.016	.001	.00	.00	.021	.121	3
minepump_spec1_product15_true-unreach-call.cil.c	timeout	905	891	3722657792		183	5.21	.014	878	true	12.2	6.54	377044992		1	.576	.001	.004	.048			true	9.17	5.10	344399872		.541	.521	1.13	.251	.406	.395	.222	.009	.231	.139	true	8.77	4.87	316309504		4	.231	.082	1.13	.253	.013	.003	.00	.00	.018	.125	2
minepump_spec1_product16_true-unreach-call.cil.c	timeout	905	891	3644280832		179	4.99	.012	876	true	11.3	6.09	390365184		1	.564	.00	.014	.027			true	9.41	5.22	352260096		.620	.545	1.09	.206	.467	.453	.263	.025	.288	.179	true	8.75	4.89	319905792		4	.273	.093	1.22	.243	.014	.001	.00	.00	.017	.105	2
minepump_spec1_product17_true-unreach-call.cil.c	timeout	906	892	5103149056		205	4.55	.007	879	true	10.3	5.52	362147840		1	.672	.001	.005	.054			true	9.80	5.55	363286528		.560	.537	1.20	.243	.435	.396	.217	.010	.227	.138	true	8.55	4.80	306495488		5	.262	.111	1.19	.658	.017	.002	.00	.00	.021	.131	3
minepump_spec1_product18_true-unreach-call.cil.c	timeout	905	892	3413180416		174	4.50	.013	877	true	11.0	5.90	354951168		1	.543	.00	.004	.024			true	8.92	5.04	358985728		.604	.461	1.09	.256	.372	.329	.185	.010	.195	.124	true	8.55	4.83	324677632		4	.257	.078	1.23	.724	.014	.009	.00	.00	.023	.100	2
minepump_spec1_product19_true-unreach-call.cil.c	timeout	906	891	3679371264		181	5.00	.012	877	true	11.0	5.93	355487744		1	.873	.00	.006	.087			true	9.38	5.29	355475456		.584	.563	1.22	.282	.480	.459	.226	.020	.246	.165	true	8.57	4.83	323743744		4	.272	.128	1.17	.649	.018	.001	.00	.00	.015	.097	2
minepump_spec1_product20_true-unreach-call.cil.c	timeout	905	890	3725897728		182	5.08	.015	877	true	11.4	6.13	373559296		1	.951	.004	.006	.090			true	9.80	5.51	348467200		.722	.510	1.21	.274	.426	.407	.252	.008	.260	.155	true	8.46	4.74	312504320		4	.256	.079	1.23	.762	.008	.001	.00	.00	.014	.110	2
minepump_spec1_product21_true-unreach-call.cil.c	timeout	906	891	5093601280		201	5.41	.015	875	true	11.9	6.36	364937216		1	.598	.00	.013	.064			true	10.4	5.73	370241536		.628	.706	1.57	.341	.608	.580	.315	.031	.346	.243	true	9.08	5.08	323710976		4	.332	.103	1.35	.775	.014	.002	.00	.00	.024	.146	2
minepump_spec1_product22_true-unreach-call.cil.c	timeout	906	891	3461492736		176	5.10	.010	876	true	11.7	6.21	375422976		1	.947	.00	.007	.072			true	10.4	5.79	380112896		.615	.629	1.50	.329	.490	.452	.248	.020	.268	.178	true	9.06	5.15	324161536		4	.294	.108	1.47	.825	.012	.00	.00	.00	.023	.124	2
minepump_spec1_product23_true-unreach-call.cil.c	timeout	913	896	5174284288						true	12.0	6.42	375341056		1	1.16	.00	.003	.136			true	10.2	5.66	370233344		.677	.717	1.55	.331	.588	.539	.291	.043	.334	.221	true	9.26	5.23	323907584		4	.369	.123	1.37	.344	.022	.002	.00	.00	.018	.153	2
minepump_spec1_product24_true-unreach-call.cil.c	timeout	905	888	3798216704		179	5.25	.012	873	true	14.2	7.46	402096128		1	1.06	.010	.007	.085			true	10.3	5.73	378712064		.613	.756	1.61	.319	.617	.593	.351	.058	.409	.271	true	8.86	5.00	323817472		4	.349	.106	1.30	.306	.015	.002	.00	.00	.019	.134	2
minepump_spec1_product25_true-unreach-call.cil.c	timeout	906	892	5104164864		203	5.00	.015	877	true	10.8	5.80	359333888		1	.608	.00	.006	.026			true	8.75	4.91	359346176		.539	.473	1.10	.207	.385	.370	.212	.011	.223	.129	true	8.48	4.79	312225792		5	.271	.083	1.17	.644	.005	.001	.00	.00	.024	.132	3
minepump_spec1_product26_true-unreach-call.cil.c	timeout	905	888	3489587200		175	4.51	.009	875	true	11.6	6.16	358416384		1	.677	.00	.019	.033			true	8.98	5.03	351297536		.556	.460	1.09	.236	.365	.350	.182	.011	.193	.132	true	8.84	4.94	318922752		4	.283	.105	1.21	.692	.037	.002	.00	.00	.026	.114	2
minepump_spec1_product27_true-unreach-call.cil.c	timeout	906	891	3700584448		183	5.08	.015	877	true	11.7	6.24	368046080		1	.749	.00	.005	.032			true	9.78	5.51	355368960		.593	.549	1.27	.260	.465	.449	.210	.027	.237	.157	true	8.56	4.81	317816832		4	.265	.097	1.24	.276	.009	.002	.00	.00	.014	.117	2
minepump_spec1_product28_true-unreach-call.cil.c	timeout	905	888	3694981120		179	5.10	.014	874	true	12.2	6.53	392376320		1	.799	.00	.019	.106			true	9.49	5.32	353349632		.652	.562	1.22	.303	.476	.459	.270	.010	.280	.164	true	8.48	4.73	325001216		4	.719	.076	.728	.239	.014	.002	.00	.00	.015	.102	2
minepump_spec1_product29_true-unreach-call.cil.c	timeout	906	890	5107724288		200	5.28	.009	875	true	10.7	5.76	372510720		1	.794		.010				true	10.3	5.73	371933184		.759	.632	1.47	.322	.471	.451	.269	.017	.286	.183	true	9.10	5.12	334454784		4	.312	.122	1.34	.317	.019	.001	.00	.00	.026	.131	2
minepump_spec1_product30_true-unreach-call.cil.c	timeout	905	891	3573141504		181	4.99	.014	878	true	11.4	6.12	386207744		1	.677	.00	.005	.019			true	10.3	5.68	371347456		.688	.629	1.50	.276	.518	.482	.282	.015	.297	.185	true	9.17	5.17	330182656		4	.350	.096	1.30	.746	.015	.001	.00	.00	.022	.120	2
minepump_spec1_product31_true-unreach-call.cil.c	timeout	905	887	3792195584		178	5.14	.016	873	true	13.3	7.04	397918208		1	.865	.00	.006	.027			true	10.5	5.80	374108160		.761	.727	1.62	.338	.632	.605	.373	.048	.421	.295	true	8.99	5.03	325353472		4	.335	.095	1.33	.748	.018	.001	.00	.00	.017	.117	2
minepump_spec1_product32_true-unreach-call.cil.c	timeout	906	891	5111054336		183	5.21	.011	877	true	13.7	7.34	415793152		1	1.55	.001	.015	.266			true	10.0	5.55	365989888		.545	.716	1.60	.326	.611	.589	.364	.033	.397	.250	true	8.88	4.96	328716288		4	.749	.125	.982	.349	.015	.001	.00	.00	.015	.128	2
minepump_spec1_product45_true-unreach-call.cil.c	timeout	905	892	3455229952		76	5.35	48.7	815	true	30.9	15.9	674541568		1	1.61	.089	2.60	.412	6.67	1.09	true	11.7	6.46	375975936		.634	.996	2.26	.505	.855	.825	.557	.030	.587	.368	true	9.43	5.29	330203136		4	.365	.125	1.72	.431	.010	.001	.00	.00	.023	.159	2
minepump_spec1_product46_true-unreach-call.cil.c	timeout	905	890	3440361472		74	5.29	60.4	802	true	28.5	14.7	678203392		1	1.06	.135	.006	.524	6.99	.565	true	11.4	6.25	378785792		.634	.952	2.20	.508	.813	.782	.509	.032	.541	.327	true	9.85	5.51	330391552		4	.419	.098	1.57	.843	.012	.001	.00	.00	.024	.164	2
minepump_spec1_product47_true-unreach-call.cil.c	timeout	905	891	3810021376		77	5.51	418	441	true	33.8	17.4	775774208		2	1.71	.357	.021	.501	7.55	1.55	true	11.2	6.29	375525376		.752	.998	2.12	.408	.852	.819	.527	.062	.589	.330	true	9.77	5.43	330960896		4	.453	.124	1.60	.424	.017	.001	.00	.00	.019	.177	2
minepump_spec1_product48_true-unreach-call.cil.c	timeout	907	892	3456421888		71	5.05	250	613	true	35.7	18.3	796925952		2	1.94	.645	.014	.607	7.67	1.74	true	12.6	6.95	386940928		.821	1.46	2.70	.436	1.30	1.28	.825	.079	.904	.483	true	9.65	5.41	343326720		4	.424	.119	1.47	.434	.026	.003	.00	.00	.014	.150	2
minepump_spec1_product57_true-unreach-call.cil.c	timeout	905	891	2951618560		62	4.58	491	378	true	169	85.0	2827866112		12	2.40	7.84	.016	6.38	25.1	36.2	true	12.5	6.87	377032704		.773	1.36	2.66	.471	1.18	1.13	.721	.093	.814	.479	true	10.7	6.09	340971520		7	.736	.106	1.88	.840	.011	.002	.00	.00	.079	.392	2
minepump_spec1_product58_true-unreach-call.cil.c	timeout	904	891	2931511296		60	4.77	477	392	true	188	94.5	3387600896		13	2.74	8.99	.012	7.99	26.3	41.2	true	13.2	7.19	402939904		.433	1.62	3.31	.790	1.44	1.40	.960	.116	1.08	.598	true	9.46	5.31	335990784		4	.477	.476	1.49	.366	.010	.001	.00	.00	.039	.175	2
minepump_spec1_product59_true-unreach-call.cil.c	timeout	906	892	2977214464		61	5.00	598	270	true	177	89.0	2989899776		12	2.93	10.3	.004	7.86	26.5	34.1	true	13.3	7.39	402780160		.367	1.58	3.46	.952	1.42	1.37	.869	.148	1.02	.554	true	9.68	5.42	333959168		4	.435	.543	1.68	.446	.023	.001	.00	.00	.018	.165	2
minepump_spec1_product60_true-unreach-call.cil.c	timeout	905	892	2988572672		59	4.81	540	330	true	235	118	3683729408		14	3.14	15.4	.011	10.1	30.6	51.5	true	13.7	7.54	399925248		.926	1.55	2.96	.534	1.37	1.35	.825	.153	.978	.591	true	10.0	5.60	335417344		4	.388	.138	1.68	.420	.020	.002	.00	.00	.022	.185	2
minepump_spec1_product61_true-unreach-call.cil.c	timeout	905	890	3431387136		66	6.54	47.9	812	true	34.5	17.7	815099904		1	1.20	.576	.006	.474	8.72	.244	true	14.2	7.67	419688448		.311	1.42	3.76	1.09	1.18	1.12	.745	.047	.792	.448	true	10.5	5.97	342216704		4	.460	.140	2.12	.602	.015	.002	.00	.00	.021	.203	2
minepump_spec1_product62_true-unreach-call.cil.c	timeout	905	891	3441168384		66	6.18	58.4	804	true	38.2	19.6	839475200		1	2.37	.127	3.36	.202	8.03	1.10	true	16.0	8.65	428744704		.379	1.98	4.37	1.03	1.39	1.31	.847	.089	.936	.514	true	10.7	5.95	348434432		4	.559	.121	2.04	1.07	.020	.005	.00	.00	.020	.234	2
minepump_spec1_product63_true-unreach-call.cil.c	timeout	907	892	3650912256		67	6.24	380	480	true	37.6	19.2	842309632		2	1.92	.688	.008	.381	8.40	1.33	true	17.7	9.48	434585600		.524	2.28	5.35	.900	2.00	1.92	1.27	.141	1.41	.775	true	10.5	5.91	350941184		4	.929	.158	1.73	.683	.021	.001	.00	.00	.016	.196	2
minepump_spec1_product64_true-unreach-call.cil.c	timeout	905	890	3270782976		60	5.97	202	660	true	39.1	20.0	886022144		2	2.01	.756	.008	.756	8.38	1.59	true	16.5	8.85	451596288		.540	1.84	4.41	1.12	1.59	1.54	1.00	.134	1.14	.710	true	10.8	6.03	345120768		4	.491	.200	2.17	.579	.043	.002	.00	.00	.016	.212	2
minepump_spec2_product01_true-unreach-call.cil.c	timeout	906	891	5106475008		196	4.95	.010	878	true	10.1	5.43	369348608		1	.631	.001	.004	.046			true	7.79	4.34	340844544		.466	.170	.511	.141	.118	.113	.046	.003	.049	.059	true	8.01	4.40	305930240		2	.080	.644	.980	.148	.621	.611	.563	.007	.575	.036	2	.575
minepump_spec2_product02_true-unreach-call.cil.c	timeout	904	889	3491184640		173	4.31	.012	877	true	10.2	5.52	368132096		1	.763	.00	.018	.070			true	7.98	4.47	336191488		.624	.198	.518	.138	.137	.130	.043	.004	.047	.058	true	7.88	4.34	305664000		2	.085	.504	.872	.175	.463	.461	.413	.005	.422	.040	2	.422
minepump_spec2_product03_true-unreach-call.cil.c	timeout	905	891	3712765952		186	4.84	.013	877	true	11.2	6.00	375840768		1	.505	.00	.005	.062			true	8.29	4.59	333688832		.487	.181	.561	.184	.131	.124	.049	.004	.053	.069	true	7.80	4.34	302714880		2	.082	.150	.928	.599	.103	.096	.035	.007	.046	.028	2	.049
minepump_spec2_product04_true-unreach-call.cil.c	timeout	904	890	3354267648		168	4.62	.007	877	true	14.0	7.42	433872896		1	.576	.00	.006	.042			true	7.64	4.29	342581248		.468	.154	.515	.163	.117	.112	.043	.001	.044	.058	true	7.66	4.27	309080064		2	.080	.493	.868	.183	.440	.433	.050	.005	.058	.037	2	.063
minepump_spec2_product05_true-unreach-call.cil.c	timeout	906	889	5158408192		201	5.08	.010	874	true	10.7	5.69	332554240		1	.761	.00	.005	.042			true	10.3	5.76	361181184		.652	.659	1.46	.287	.564	.538	.307	.030	.337	.361	true	9.89	5.53	321171456		7	.285	.933	1.69	.269	.327	.317	.182	.017	.242	.200	3	.204
minepump_spec2_product06_true-unreach-call.cil.c	timeout	905	888	3562553344		175	4.81	.012	874	true	10.8	5.81	347435008		1	.797	.001	.013	.075			true	10.2	5.63	360325120		.576	.778	1.53	.281	.662	.632	.346	.035	.381	.408	true	9.84	5.59	326041600		7	.368	.865	1.79	.298	.788	.358	.222	.018	.282	.249	2	.248
minepump_spec2_product07_true-unreach-call.cil.c	timeout	906	890	3766177792		181	5.01	.006	876	true	11.9	6.38	379076608		1	.968	.00	.009	.070			true	9.58	5.32	361746432		.540	.647	1.39	.291	.563	.530	.244	.048	.292	.324	true	9.39	5.32	327012352		8	.372	.876	1.72	.328	.307	.290	.185	.012	.240	.206	2	.200
minepump_spec2_product08_true-unreach-call.cil.c	timeout	905	887	3720978432		177	5.19	.010	873	true	14.5	7.80	461119488		1	.711	.00	.016	.143			true	9.94	5.55	363147264		.556	.735	1.47	.290	.633	.611	.329	.060	.389	.416	true	9.80	5.55	326893568		10	.404	.849	1.75	.325	.768	.754	.619	.023	.699	.284	3	.651
minepump_spec2_product09_true-unreach-call.cil.c	timeout	905	889	5143724032		202	4.98	.014	872	true	10.7	5.78	363954176		1	.688	.00	.005	.029			true	7.76	4.29	335724544		.415	.179	.481	.142	.144	.132	.041	.004	.045	.064	true	8.00	4.43	308170752		2	.071	.168	.966	.196	.112	.107	.041	.004	.049	.033	2	.053
minepump_spec2_product10_true-unreach-call.cil.c	timeout	905	891	3460313088		174	4.37	.017	878	true	10.8	5.73	351141888		1	.614	.00	.005	.090			true	7.86	4.40	337932288		.434	.181	.524	.134	.138	.129	.056	.003	.059	.076	true	7.86	4.38	311660544		2	.075	.529	.899	.191	.470	.465	.409	.004	.417	.032	2	.420
minepump_spec2_product11_true-unreach-call.cil.c	timeout	906	891	3637329920		183	5.04	.010	878	true	11.5	6.08	368017408		1	.600	.00	.005	.061			true	7.20	3.98	337010688		.445	.169	.481	.149	.137	.127	.061	.003	.064	.080	true	8.06	4.47	306184192		2	.082	.504	.885	.160	.465	.447	.035	.005	.044	.046	2	.043
minepump_spec2_product12_true-unreach-call.cil.c	timeout	904	886	3304529920		162	4.58	.007	873	true	11.1	5.99	394604544		1	.900	.00	.013	.082			true	8.14	4.53	338833408		.486	.201	.528	.149	.150	.147	.043	.002	.045	.063	true	7.80	4.38	305033216		2	.074	.139	.939	.166	.106	.099	.048	.004	.055	.027	2	.056
minepump_spec2_product13_true-unreach-call.cil.c	timeout	906	888	5177974784		208	5.30	.009	873	true	10.3	5.53	363864064		1	.862		.006				true	10.4	5.74	362749952		.692	.747	1.46	.266	.634	.612	.328	.029	.357	.393	true	9.25	5.25	306872320		7	.303	.368	1.59	.265	.291	.276	.174	.016	.222	.176	3	.195
minepump_spec2_product14_true-unreach-call.cil.c	timeout	905	891	3424022528		172	4.61	.013	878	true	10.9	5.84	380821504		1	.633	.00	.006	.038			true	10.2	5.65	359960576		.565	.872	1.57	.266	.734	.718	.362	.046	.408	.463	true	9.64	5.48	331673600		7	.338	.419	1.78	.787	.352	.343	.214	.018	.270	.244	2	.241
minepump_spec2_product15_true-unreach-call.cil.c	timeout	905	891	5106991104		183	5.93	.015	876	true	12.7	6.70	393392128		1	.596	.00	.005	.026			true	9.92	5.49	356708352		.539	.681	1.47	.300	.595	.574	.275	.059	.334	.362	true	9.25	5.27	323792896		8	.692	.402	1.27	.312	.334	.322	.188	.020	.254	.222	2	.217
minepump_spec2_product16_true-unreach-call.cil.c	timeout	905	889	5170900992		182	5.11	.009	876	true	11.8	6.25	410943488		1	.595	.00	.013	.027			true	10.9	6.04	368898048		.677	.779	1.58	.326	.680	.655	.359	.061	.420	.450	true	9.53	5.45	330334208		10	.391	.445	1.75	.718	.368	.361	.209	.021	.291	.279	3	.243
minepump_spec2_product17_true-unreach-call.cil.c	timeout	906	890	5156581376		198	5.06	.015	875	true	10.5	5.61	361078784		1	.724	.00	.005	.104			true	10.4	5.77	372682752		.596	.734	1.53	.301	.600	.575	.301	.032	.333	.385	true	8.78	5.05	327360512		7	.276	.485	1.50	.552	.403	.390	.251	.024	.304	.190	3	.281
minepump_spec2_product18_true-unreach-call.cil.c	timeout	905	890	3405955072		171	4.51	.015	877	true	11.2	6.00	349298688		1	.774	.00	.003	.069			true	10.3	5.75	357732352		.742	.677	1.49	.307	.590	.571	.323	.031	.354	.384	true	10.1	5.78	339927040		7	.434	.534	1.87	.755	.455	.434	.264	.021	.325	.260	2	.291
minepump_spec2_product19_true-unreach-call.cil.c	timeout	905	891	5117419520		183	5.15	.007	877	true	12.2	6.58	416309248		1	.530	.00	.010	.040			true	10.3	5.79	358051840		.622	.778	1.56	.310	.683	.651	.315	.061	.376	.404	true	10.7	6.06	341970944		9	.475	.692	2.35	.340	.591	.578	.378	.030	.454	.343	3	.416
minepump_spec2_product20_true-unreach-call.cil.c	timeout	905	891	3651141632		178	5.15	.011	877	true	12.9	6.87	401764352		1	.917	.00	.010	.092			true	9.00	5.01	359948288		.487	.532	1.11	.235	.449	.440	.244	.038	.282	.320	true	10.1	5.80	338604032		8	.574	.587	1.97	.314	.489	.480	.322	.025	.402	.297	2	.357
minepump_spec2_product21_true-unreach-call.cil.c	timeout	906	889	5159862272		200	5.41	.013	875	true	11.5	6.19	388702208		1	1.19		.005				true	12.0	6.57	393691136		.673	.952	2.30	.488	.810	.783	.453	.049	.502	.528	true	10.3	5.82	342548480		7	.416	.597	2.09	.772	.490	.479	.298	.036	.369	.238	3	.341
minepump_spec2_product22_true-unreach-call.cil.c	timeout	904	890	3471396864		174	4.99	.009	876	true	11.9	6.39	390168576		1	.702	.001	.018	.020			true	12.4	6.77	378912768		.629	1.17	2.53	.539	1.01	.946	.572	.069	.641	.681	true	10.6	6.10	342441984		7	.510	.638	2.29	.839	.532	.508	.317	.023	.374	.327	2	.346
minepump_spec2_product23_true-unreach-call.cil.c	timeout	905	888	5178843136		180	5.04	.012	874	true	13.1	6.96	386994176		1	.982	.00	.023	.138			true	11.4	6.25	376283136		.835	.998	2.20	.446	.896	.869	.448	.095	.543	.581	true	10.8	6.18	350236672		7	.479	1.09	2.33	.436	.998	.963	.328	.031	.397	.364	2	.363
minepump_spec2_product24_true-unreach-call.cil.c	timeout	905	892	5100822528		178	5.33	.012	877	true	13.7	7.25	433700864		1	.839	.001	.010	.049			true	12.1	6.61	378339328		.654	1.22	2.42	.414	1.03	.984	.583	.083	.666	.694	true	11.9	6.74	351408128		8	.591	1.16	2.61	.471	.617	.597	.396	.042	.488	.461	2	.450
minepump_spec2_product25_true-unreach-call.cil.c	timeout	906	892	5111287808		201	5.07	.014	877	true	11.1	5.93	374566912		1	.543	.001	.005	.034			true	9.69	5.36	366075904		.519	.815	1.53	.258	.681	.639	.343	.038	.381	.411	true	9.33	5.34	330788864		7	.281	.976	1.76	.318	.887	.872	.727	.027	.782	.207	3	.765
minepump_spec2_product26_true-unreach-call.cil.c	timeout	904	890	3476918272		174	4.65	.009	876	true	12.1	6.38	360960000		1	.662	.001	.005	.133			true	10.5	5.81	374550528		.622	.705	1.52	.288	.592	.573	.292	.034	.326	.358	true	10.0	5.66	329994240		7	.388	1.01	1.91	.323	.944	.935	.270	.027	.331	.279	2	.304
minepump_spec2_product27_true-unreach-call.cil.c	timeout	905	891	5102567424		185	5.20	.011	877	true	11.2	6.01	386252800		1	.910	.00	.005	.120			true	10.5	5.82	366497792		.685	.890	1.66	.285	.761	.740	.361	.061	.422	.484	true	10.8	6.14	344924160		9	.520	.628	2.06	.725	.541	.525	.355	.029	.432	.304	3	.397
minepump_spec2_product28_true-unreach-call.cil.c	timeout	906	892	5102956544		182	4.81	.010	878	true	13.2	7.04	427876352		1	.595	.00	.005	.050			true	9.39	5.24	351055872		.674	.511	1.20	.312	.420	.406	.223	.024	.247	.266	true	10.3	5.84	337154048		8	.514	.573	1.97	.303	.491	.479	.317	.027	.401	.304	2	.354
minepump_spec2_product29_true-unreach-call.cil.c	timeout	905	888	5171830784		196	5.17	.013	874	true	10.9	5.84	369860608		1	.669		.005				true	12.6	6.84	391368704		.625	1.06	2.41	.505	.918	.900	.536	.075	.611	.659	true	10.4	5.88	340717568		7	.420	.620	2.10	.339	.541	.523	.334	.038	.403	.253	3	.379
minepump_spec2_product30_true-unreach-call.cil.c	timeout	905	890	3416641536		172	4.92	.008	876	true	10.9	5.83	340209664		1	.719		.005				true	12.3	6.81	382623744		.711	1.22	2.48	.503	1.03	1.01	.563	.059	.622	.700	true	10.5	6.02	344412160		7	.500	.993	2.23	.455	.881	.866	.727	.026	.788	.294	2	.759
minepump_spec2_product31_true-unreach-call.cil.c	timeout	906	891	3685392384		177	5.18	.006	874	true	13.1	6.98	422047744		1	.814	.00	.006	.050			true	11.7	6.42	373841920		.550	1.01	2.31	.537	.890	.870	.486	.078	.564	.590	true	11.4	6.49	341286912		7	.544	1.12	2.39	.446	.519	.507	.344	.032	.413	.360	2	.380
minepump_spec2_product32_true-unreach-call.cil.c	timeout	905	891	3714400256		177	5.23	.028	877	true	14.2	7.59	449175552		1	.863	.007	.005	.189			true	11.1	6.21	384741376		.564	1.01	2.28	.549	.819	.794	.439	.076	.515	.557	true	11.7	6.67	346365952		8	.558	.689	2.66	1.02	.595	.579	.394	.039	.479	.470	2	.443
minepump_spec2_product37_true-unreach-call.cil.c	timeout	904	891	3333160960		81	5.00	52.8	811	true	30.5	15.7	673435648		1	1.31	.00	2.62	.170	6.21	2.09	true	12.5	6.80	375992320		.707	1.24	2.53	.524	1.11	1.08	.637	.152	.789	.813	true	10.5	5.94	341729280		7	.396	.610	2.14	.830	.513	.491	.299	.039	.366	.251	3	.349
minepump_spec2_product38_true-unreach-call.cil.c	timeout	904	888	3378577408		79	4.93	56.7	805	true	28.8	14.8	644308992		1	1.40	.00	2.38	.305	6.15	1.01	true	12.7	6.93	370417664		.748	1.32	2.58	.477	1.14	1.11	.576	.112	.688	.745	true	10.7	6.02	339132416		6	.457	.650	2.06	.379	.536	.512	.340	.033	.408	.194	2	.380
minepump_spec2_product39_true-unreach-call.cil.c	timeout	908	890	3669274624		84	5.18	423	437	true	43.6	22.4	905129984		3	2.11	.282	.005	.842	8.90	4.58	true	12.2	6.71	381329408		.811	1.20	2.36	.410	1.03	1.00	.550	.127	.677	.697	true	10.3	5.90	348037120		8	.544	.659	2.18	.395	.563	.550	.361	.036	.438	.284	2	.405
minepump_spec2_product40_true-unreach-call.cil.c	timeout	905	891	3218694144		75	5.18	231	633	true	47.5	24.2	929607680		3	1.99	.749	.005	1.44	11.3	3.45	true	11.9	6.49	381091840		.777	1.18	2.22	.380	1.02	.991	.596	.119	.715	.741	true	11.7	6.71	348930048		9	.646	.790	2.59	.504	.673	.640	.434	.038	.534	.399	3	.483
minepump_spec2_product45_true-unreach-call.cil.c	timeout	905	890	3306201088		72	5.22	52.2	812	true	36.5	18.8	811896832		1	1.72	.00	3.21	1.15	7.17	2.09	true	13.7	7.54	402903040		.806	1.45	3.11	.628	1.29	1.23	.724	.116	.840	.927	true	11.1	6.30	344760320		7	.475	.693	2.47	.466	.617	.604	.415	.055	.498	.338	3	.474
minepump_spec2_product46_true-unreach-call.cil.c	timeout	904	890	3252150272		70	5.03	48.6	815	true	32.3	16.6	730230784		1	1.66	.00	2.84	.458	7.39	1.25	true	12.8	7.14	398368768		.647	1.45	2.89	.469	1.26	1.21	.761	.140	.901	.940	true	11.2	6.33	350736384		6	.556	1.09	2.33	.429	.998	.971	.372	.037	.441	.306	2	.825
minepump_spec2_product47_true-unreach-call.cil.c	timeout	907	893	3630395392		75	4.69	418	445	true	51.3	26.3	927309824		2	1.96	.358	.006	.811	9.13	8.19	true	12.7	6.95	396726272		.705	1.49	2.83	.430	1.28	1.24	.755	.128	.883	.909	true	12.2	7.16	361148416		9	.827	.874	2.88	.887	.765	.743	.527	.050	.653	.447	3	.585
minepump_spec2_product48_true-unreach-call.cil.c	timeout	905	892	3433390080		70	5.36	283	580	true	51.8	26.4	937910272		3	2.24	1.25	.005	1.76	10.9	4.32	true	13.3	7.23	390991872		.767	1.48	2.92	.465	1.28	1.24	.659	.141	.800	.869	true	11.4	6.49	351203328		8	.647	1.18	2.56	.476	1.02	1.00	.397	.038	.493	.366	2	.442
minepump_spec2_product49_true-unreach-call.cil.c	timeout	905	892	2987986944		70	4.60	482	385	true	294	148	4420190208		18	3.04	13.2	.005	15.3	37.9	70.3	true	12.5	6.87	374673408		.694	1.38	2.64	.450	1.23	1.17	.724	.088	.812	.858	true	13.0	7.52	363151360		11	.983	.951	3.14	1.14	.834	.809	.559	.046	.680	.491	2	.614
minepump_spec2_product50_true-unreach-call.cil.c	timeout	906	891	2938494976		68	4.83	486	382	true	166	83.9	3087749120		13	3.04	6.19	.013	6.89	27.1	33.5	true	12.2	6.61	387309568		.679	1.32	2.56	.461	1.18	1.16	.683	.115	.798	.863	true	15.0	9.09	372252672		16	1.46	1.14	4.03	.946	.980	.954	.677	.064	.881	1.26	2	.758
minepump_spec2_product51_true-unreach-call.cil.c	timeout	904	891	2938683392		65	4.69	612	255	true	228	115	3559358464		15	3.00	12.1	.019	9.71	29.8	52.9	true	12.7	6.89	380669952		.702	1.42	2.70	.522	1.24	1.22	.719	.156	.875	.927	true	11.8	6.77	350023680		9	.714	.791	2.71	.454	.703	.686	.470	.034	.571	.405	3	.514
minepump_spec2_product52_true-unreach-call.cil.c	timeout	904	892	2956214272		60	4.52	503	367	true	233	117	3705622528		15	2.87	12.8	.008	11.3	32.1	50.5	true	12.8	7.04	380223488		.645	1.44	2.65	.532	1.29	1.26	.670	.176	.846	.922	true	11.8	6.83	351842304		8	.668	1.19	2.75	.587	1.08	1.06	.494	.040	.590	.358	2	.889
minepump_spec2_product53_true-unreach-call.cil.c	timeout	905	891	3439304704		72	5.83	51.5	810	true	34.8	17.9	833396736		1	1.59	.00	.016	.110	7.94	1.59	true	16.4	8.87	448663552		.443	1.97	4.69	.735	1.71	1.66	.978	.208	1.19	1.25	true	11.8	6.65	347627520		6	.559	1.17	2.69	.619	1.06	1.02	.831	.035	.892	.269	2	.874
minepump_spec2_product54_true-unreach-call.cil.c	timeout	904	891	3442237440		71	5.92	49.4	812	true	34.6	17.8	793952256		1	1.84	.00	2.80	.171	7.88	1.45	true	15.0	8.10	424935424		.437	1.64	4.08	.688	1.47	1.43	.777	.125	.902	.943	true	13.4	7.56	355598336		7	.744	1.33	3.29	.701	1.22	1.20	.945	.049	1.05	.496	2	1.01
minepump_spec2_product55_true-unreach-call.cil.c	timeout	904	890	3304284160		67	5.67	324	538	true	46.0	23.6	888889344		2	2.12	.353	.010	1.24	10.7	2.49	true	15.7	8.52	462737408		.421	2.09	4.47	.685	1.87	1.80	.983	.254	1.24	1.38	true	12.4	6.90	359993344		6	.557	.824	2.78	.615	.614	.581	.385	.047	.463	.298	2	.437
minepump_spec2_product56_true-unreach-call.cil.c	timeout	904	891	3195736064		65	5.71	244	621	true	46.8	23.9	920461312		3	2.14	.561	.004	.858	11.1	2.98	true	15.3	8.28	432824320		.433	1.88	4.19	.948	1.66	1.58	.856	.223	1.08	1.17	true	12.0	6.76	363229184		6	.568	1.14	2.73	.656	1.01	.982	.447	.042	.527	.258	2	.496
minepump_spec2_product57_true-unreach-call.cil.c	timeout	905	891	2955567104		59	5.00	452	418	true	331	166	4577607680		18	2.83	16.5	.006	16.9	38.2	83.6	true	15.9	8.73	407339008		1.12	2.04	3.85	.610	1.85	1.79	1.01	.195	1.21	1.28	true	13.3	7.74	368205824		11	1.14	1.13	3.24	.581	.990	.965	.646	.061	.778	.534	2	.717
minepump_spec2_product58_true-unreach-call.cil.c	timeout	905	892	2950946816		59	4.90	461	409	true	152	76.7	2914271232		12	2.49	6.00	.005	6.66	26.3	28.3	true	14.5	7.92	395030528		.854	1.87	3.55	.652	1.65	1.62	1.03	.126	1.16	1.20	true	11.7	6.70	359030784		7	.695	.796	2.75	.555	.718	.704	.451	.039	.534	.397	2	.499
minepump_spec2_product59_true-unreach-call.cil.c	timeout	906	891	3013025792		59	5.14	570	299	true	164	82.8	3004932096		12	3.28	7.57	.004	8.23	26.6	30.0	true	16.1	8.73	432955392		.929	2.32	4.11	.656	2.09	2.03	1.06	.358	1.42	1.50	true	12.0	6.95	353013760		7	.663	1.24	2.79	.553	1.13	1.12	.498	.044	.597	.417	2	.932
minepump_spec2_product60_true-unreach-call.cil.c	timeout	906	892	3018571776		55	4.68	494	376	true	149	75.3	2732097536		11	2.75	6.53	.006	6.05	28.4	24.0	true	12.8	7.08	379568128		.795	1.47	2.89	.569	1.30	1.26	.742	.125	.867	.916	true	12.0	6.94	344604672		7	.668	1.30	2.79	.493	1.19	1.17	.466	.056	.569	.419	2	.531
minepump_spec2_product61_true-unreach-call.cil.c	timeout	905	890	3275739136		63	5.98	54.3	809	true	42.2	21.6	917012480		1	1.88	.001	3.76	.692	9.62	1.67	true	17.4	9.36	446492672		.672	1.91	5.06	1.03	1.58	1.48	.865	.148	1.01	1.06	true	13.6	7.56	362139648		6	.775	1.28	3.35	.690	.733	.696	.467	.049	.559	.392	2	.525
minepump_spec2_product62_true-unreach-call.cil.c	timeout	905	891	3345309696		64	5.74	46.4	816	true	42.1	21.6	910143488		1	2.08	.00	4.05	.202	9.49	1.97	true	18.4	9.85	453656576		.624	2.94	5.52	.944	2.16	2.06	1.26	.187	1.44	1.51	true	13.9	7.80	368975872		7	.981	1.09	3.22	.799	.904	.880	.620	.060	.729	.472	3	.692
minepump_spec2_product63_true-unreach-call.cil.c	timeout	905	891	3470020608		63	6.51	390	469	true	46.9	23.9	890085376		2	1.72	.322	.005	1.20	11.3	2.21	true	16.9	9.17	432779264		.594	2.01	4.88	.915	1.76	1.72	1.11	.182	1.29	1.36	true	15.5	8.78	379392000		9	1.04	1.62	4.25	.799	1.48	1.44	.718	.069	.864	.727	3	.796
minepump_spec2_product64_true-unreach-call.cil.c	timeout	904	890	3236515840		59	5.81	206	658	true	49.8	25.3	892903424		2	2.17	.197	.005	1.91	11.7	2.61	true	17.7	9.56	440827904		.565	2.53	5.30	1.17	1.99	1.94	1.18	.239	1.42	1.46	true	15.4	8.85	372490240		8	.952	1.32	4.34	1.30	1.13	1.11	.767	.063	.886	.624	2	.845
minepump_spec3_product33_true-unreach-call.cil.c	timeout	907	894	5384511488		114	4.74	82.4	775	true	21.8	11.3	566882304		1	.635	.035	1.85	.059	4.02	.965	true	9.37	5.20	353390592		.556	.594	1.17	.288	.492	.471	.278	.063	.341	.272	true	8.51	4.79	315158528		4	.307	.083	1.09	.586	.009	.003	.00	.00	.021	.116	2
minepump_spec3_product34_true-unreach-call.cil.c	timeout	907	894	5222469632		110	4.66	94.2	764	true	24.4	12.7	672866304		1	1.38	.146	2.29	.336	4.17	.882	true	8.86	4.96	354365440		.484	.458	1.06	.282	.379	.369	.203	.044	.247	.170	true	9.05	5.11	312332288		4	.287	.092	1.33	.789	.019	.002	.00	.00	.029	.124	2
minepump_spec3_product37_true-unreach-call.cil.c	timeout	905	892	3481702400		80	4.79	59.9	807	true	28.5	14.7	624021504		1	1.47	.166	2.24	.103	5.84	.970	true	11.9	6.57	380395520		.592	1.21	2.30	.444	1.11	1.09	.621	.206	.827	.636	true	9.67	5.46	339656704		4	.448	.131	1.57	.429	.017	.001	.00	.00	.044	.156	2
minepump_spec3_product38_true-unreach-call.cil.c	timeout	905	892	3293220864		75	5.02	51.3	815	true	26.5	13.6	619044864		1	1.16	.285	.005	.133	5.15	1.01	true	11.7	6.43	374476800		.551	1.09	2.21	.496	.982	.954	.519	.192	.711	.574	true	9.30	5.21	336809984		4	.342	.126	1.54	.860	.026	.001	.00	.00	.032	.165	2
minepump_spec3_product41_true-unreach-call.cil.c	timeout	906	889	5189541888		98	4.81	75.4	778	true	26.0	13.5	598880256		1	1.15	.246	2.10	.500	5.11	.990	true	10.5	5.81	361381888		.521	.907	1.64	.325	.816	.793	.436	.121	.557	.373	true	8.88	5.00	327487488		4	.332	.091	1.24	.345	.013	.00	.00	.00	.020	.139	2
minepump_spec3_product42_true-unreach-call.cil.c	timeout	906	891	5134413824		94	4.99	70.7	786	true	23.0	12.0	587591680		1	.702	.142	2.02	.064	4.44	1.02	true	9.98	5.55	360525824		.505	.935	1.70	.377	.822	.800	.465	.109	.574	.375	true	8.83	4.96	320503808		4	.324	.099	1.22	.646	.018	.002	.00	.00	.026	.164	2
minepump_spec3_product45_true-unreach-call.cil.c	timeout	905	891	3420004352		71	5.19	54.7	811	true	30.5	15.7	701358080		1	1.16	.065	2.55	.165	6.82	1.59	true	10.2	5.72	363061248		.553	.779	1.74	.414	.670	.648	.417	.079	.496	.285	true	9.78	5.46	329523200		4	.459	.139	1.60	.819	.015	.003	.00	.00	.029	.189	2
minepump_spec3_product46_true-unreach-call.cil.c	timeout	905	890	3255439360		67	5.09	55.6	810	true	32.4	16.8	748572672		1	1.26	.084	2.72	.484	6.78	1.72	true	10.3	5.77	364728320		.643	.846	1.78	.414	.714	.685	.431	.088	.519	.361	true	9.54	5.36	334577664		4	.445	.099	1.62	.408	.017	.001	.00	.00	.028	.194	2
minepump_spec3_product49_true-unreach-call.cil.c	timeout	905	892	3548614656		78	4.94	242	622	true	28.2	14.5	651935744		1	1.17	.131	2.47	.129	5.90	1.50	true	10.2	5.60	369561600		.676	.593	1.37	.359	.482	.466	.262	.045	.307	.241	true	10.8	6.13	354439168		6	.864	.150	1.83	.511	.025	.001	.00	.00	.074	.369	1
minepump_spec3_product50_true-unreach-call.cil.c	timeout	905	892	3554709504		77	5.07	247	617	true	29.7	15.3	717832192		1	1.29	.612	.004	.404	6.16	1.09	true	9.10	5.13	362258432		.509	.467	1.29	.379	.391	.360	.180	.022	.202	.140	true	9.83	5.56	343805952		4	.498	.167	1.60	.362	.017	.001	.00	.00	.043	.208	1
minepump_spec3_product53_true-unreach-call.cil.c	timeout	906	891	3233095680		65	5.73	324	540	true	37.5	19.3	800215040		1	1.97	.037	3.35	.057	8.36	1.42	true	12.0	6.61	374280192		.195	1.18	2.63	.677	.555	.526	.299	.040	.339	.262	true	12.8	7.17	358436864		6	1.01	.212	2.58	.707	.073	.005	.00	.00	.053	.486	1
minepump_spec3_product54_true-unreach-call.cil.c	timeout	906	891	3173109760		63	5.35	327	538	true	37.3	19.1	826155008		1	2.50	.285	3.26	.175	7.77	1.30	true	11.2	6.13	378531840		.609	.781	2.12	.602	.604	.585	.373	.037	.410	.324	true	13.1	7.25	363880448		6	1.19	.166	2.56	.681	.041	.001	.00	.00	.079	.552	1
minepump_spec3_product57_true-unreach-call.cil.c	timeout	906	892	2958458880		56	4.60	563	308	true	29.8	15.3	703479808		1	1.34	.065	2.50	.055	6.47	1.93	true	11.3	6.30	365920256		.577	.784	1.97	.454	.659	.627	.382	.079	.461	.327	true	19.8	13.0	374546432		25	3.62	.191	5.76	.769	.045	.005	.00	.00	.459	3.48	1
minepump_spec3_product58_true-unreach-call.cil.c	timeout	905	891	3007283200		54	4.48	583	288	true	30.2	15.5	715059200		1	1.26	.085	2.59	.097	6.94	1.28	true	10.8	5.99	375500800		.602	.813	1.86	.409	.670	.653	.415	.064	.479	.360	true	10.9	6.32	348749824		7	.811	.169	2.13	.492	.019	.002	.00	.00	.055	.461	2
minepump_spec3_product61_true-unreach-call.cil.c	timeout	904	891	3059204096		51	5.64	508	361	true	35.9	18.4	844152832		1	1.42	.274	3.00	.210	8.49	1.26	true	12.6	6.85	390729728		.203	1.00	3.09	1.06	.829	.806	.498	.099	.597	.433	true	12.7	7.24	366534656		7	1.09	.201	2.79	1.16	.035	.004	.00	.00	.057	.531	2
minepump_spec3_product62_true-unreach-call.cil.c	timeout	905	890	3065163776		52	5.35	502	366	true	36.8	18.9	877318144		1	1.39	.211	.005	.612	8.16	1.70	true	11.5	6.32	380256256		.184	.878	2.88	.985	.682	.649	.407	.076	.483	.324	true	14.1	7.95	371740672		6	1.23	.255	3.16	.805	.040	.002	.00	.00	.076	.537	1
minepump_spec4_product01_true-unreach-call.cil.c	timeout	906	893	5232406528		228	5.27	.012	878	true	9.82	5.34	356442112		1	.507	.00	.005	.058			true	7.96	4.42	332353536		.500	.146	.491	.144	.091	.078	.029	.001	.030	.033	true	8.08	4.47	297955328		2	.092	.055	.411	.165	.007	.003	.00	.00	.002	.027	2
minepump_spec4_product02_true-unreach-call.cil.c	timeout	906	893	5091274752		195	4.93	.010	879	true	10.0	5.39	353120256		1	.743		.005				true	8.06	4.51	335642624		.389	.126	.482	.149	.084	.079	.025	.001	.026	.032	true	7.55	4.21	303431680		2	.101	.064	.419	.150	.007	.001	.00	.00	.005	.033	2
minepump_spec4_product03_true-unreach-call.cil.c	timeout	906	891	5119328256		198	5.09	.010	877	true	10.3	5.52	346304512		1	.546	.00	.013	.030			true	8.05	4.54	335073280		.497	.147	.498	.170	.105	.096	.039	.003	.042	.039	true	7.50	4.18	308068352		2	.097	.056	.437	.159	.015	.001	.00	.00	.003	.030	2
minepump_spec4_product04_true-unreach-call.cil.c	timeout	906	892	5117038592		189	5.03	.009	878	true	9.87	5.32	359936000		1	.862		.012				true	7.64	4.30	333873152		.425	.164	.489	.143	.098	.090	.041	.001	.042	.039	true	7.77	4.33	297320448		2	.090	.064	.386	.177	.008	.001	.00	.00	.003	.029	2
minepump_spec4_product05_true-unreach-call.cil.c	timeout	906	891	5114183680		223	5.34	.011	875	true	10.0	5.42	356909056		1	.540	.00	.005	.029			true	9.34	5.25	341929984		.537	.335	.872	.231	.231	.221	.114	.011	.125	.097	true	8.37	4.67	316198912		4	.240	.075	1.08	.643	.022	.001	.00	.00	.025	.105	2
minepump_spec4_product06_true-unreach-call.cil.c	timeout	906	892	5099470848		200	5.06	.011	878	true	9.57	5.18	362233856		1	.536	.00	.004	.036			true	8.71	4.86	350384128		.462	.334	.863	.216	.249	.240	.126	.010	.136	.104	true	8.53	4.79	314925056		5	.232	.094	1.23	.265	.013	.004	.00	.00	.010	.141	3
minepump_spec4_product07_true-unreach-call.cil.c	timeout	906	892	5119406080		204	5.35	.017	876	true	9.98	5.37	351150080		1	.700	.00	.004	.022			true	8.80	4.87	343789568		.459	.346	.886	.246	.261	.247	.126	.020	.146	.109	true	8.70	4.82	316239872		5	.294	.065	1.16	.253	.009	.003	.00	.00	.011	.126	3
minepump_spec4_product08_true-unreach-call.cil.c	timeout	906	888	5195653120		201	5.56	.013	872	true	10.6	5.71	361705472		1	.491	.005	.006	.051			true	8.24	4.65	350117888		.474	.341	.837	.209	.271	.261	.147	.020	.167	.116	true	8.17	4.52	314380288		4	.258	.097	1.07	.621	.020	.001	.00	.00	.022	.121	2
minepump_spec4_product09_true-unreach-call.cil.c	timeout	906	890	5129732096		222	5.25	.015	875	true	9.71	5.23	341217280		1	.716		.005				true	7.89	4.41	332464128		.481	.159	.522	.178	.106	.099	.040	.001	.041	.046	true	7.56	4.24	304205824		2	.102	.051	.387	.172	.005	.001	.00	.00	.002	.028	2
minepump_spec4_product10_true-unreach-call.cil.c	timeout	906	892	5130715136		197	4.85	.009	878	true	10.3	5.57	340140032		1	.566	.00	.010	.041			true	7.63	4.27	335458304		.333	.175	.476	.133	.109	.102	.035	.002	.037	.040	true	7.58	4.23	299413504		2	.094	.461	.808	.164	.006	.001	.00	.00	.003	.031	2
minepump_spec4_product11_true-unreach-call.cil.c	timeout	906	892	5103501312		199	5.20	.020	877	true	10.0	5.35	347951104		1	.629	.001	.008	.062			true	8.29	4.58	334721024		.523	.178	.500	.146	.124	.116	.055	.00	.055	.052	true	7.62	4.27	305176576		2	.092	.048	.366	.152	.007	.002	.00	.00	.003	.033	2
minepump_spec4_product12_true-unreach-call.cil.c	timeout	905	892	3681026048		185	5.07	.006	877	true	10.2	5.49	343019520		1	.638	.001	.011	.046			true	8.32	4.59	340140032		.490	.157	.546	.170	.114	.096	.043	.003	.046	.043	true	7.85	4.37	301187072		2	.105	.063	.778	.566	.005	.001	.00	.00	.003	.030	2
minepump_spec4_product13_true-unreach-call.cil.c	timeout	906	891	5113839616		223	5.34	.015	875	true	9.39	5.07	343339008		1	.598	.001	.004	.051			true	8.29	4.58	339984384		.570	.286	.729	.198	.222	.214	.116	.008	.124	.096	true	8.48	4.72	312823808		4	.738	.081	.679	.239	.019	.002	.00	.00	.026	.106	2
minepump_spec4_product14_true-unreach-call.cil.c	timeout	906	892	5120053248		198	5.05	.005	877	true	10.2	5.53	340963328		1	.573		.004				true	8.89	4.91	336723968		.585	.353	.810	.213	.279	.269	.150	.011	.161	.113	true	8.71	4.85	308482048		5	.236	.073	1.23	.226	.014	.002	.00	.00	.013	.141	3
minepump_spec4_product15_true-unreach-call.cil.c	timeout	906	888	5193592832		210	5.55	.015	869	true	9.95	5.36	359391232		1	.784		.017				true	8.21	4.56	352137216		.520	.347	.825	.220	.285	.276	.151	.017	.168	.120	true	8.31	4.65	315219968		5	.594	.081	.704	.240	.009	.001	.00	.00	.013	.119	3
minepump_spec4_product16_true-unreach-call.cil.c	timeout	906	892	5130743808		201	5.46	.012	877	true	9.79	5.28	340938752		1	.649		.014				true	8.50	4.72	344580096		.480	.359	.853	.225	.286	.270	.135	.017	.152	.108	true	8.47	4.75	324042752		4	.292	.083	1.10	.244	.022	.002	.00	.00	.023	.118	2
minepump_spec4_product17_true-unreach-call.cil.c	timeout	906	888	5235511296		225	5.40	.013	872	true	9.68	5.21	350441472		1	.368		.008				true	9.36	5.18	345214976		.469	.368	.918	.244	.289	.272	.135	.011	.146	.107	true	8.42	4.69	317566976		5	.288	.093	1.15	.647	.011	.001	.00	.00	.023	.158	3
minepump_spec4_product18_true-unreach-call.cil.c	timeout	906	889	5175848960		191	4.87	.017	875	true	10.1	5.44	361889792		1	.632	.001	.020	.023			true	8.87	4.94	351150080		.559	.341	.836	.224	.262	.248	.123	.008	.131	.091	true	8.41	4.74	318599168		4	.280	.087	1.19	.244	.010	.002	.00	.00	.022	.117	2
minepump_spec4_product19_true-unreach-call.cil.c	timeout	906	892	5098049536		202	5.38	.018	876	true	9.91	5.31	362385408		1	.589		.007				true	8.55	4.77	338046976		.534	.410	.942	.238	.332	.323	.153	.031	.184	.149	true	8.57	4.76	328728576		5	.243	.086	1.15	.260	.009	.001	.00	.00	.010	.130	3
minepump_spec4_product20_true-unreach-call.cil.c	timeout	906	890	5141032960		203	5.54	.014	874	true	10.0	5.40	351240192		1	.738		.005				true	8.44	4.67	350904320		.481	.345	.872	.235	.284	.277	.140	.024	.164	.112	true	8.65	4.88	316383232		4	.310	.067	1.11	.620	.012	.001	.00	.00	.025	.131	2
minepump_spec4_product21_true-unreach-call.cil.c	timeout	907	890	5203595264		226	5.65	.009	873	true	9.93	5.33	364568576		1	.247		.005				true	9.90	5.50	374452224		.290	.470	1.61	.346	.374	.350	.189	.013	.202	.134	true	9.22	5.14	329695232		4	.352	.090	1.42	.378	.025	.001	.00	.00	.026	.154	2
minepump_spec4_product22_true-unreach-call.cil.c	timeout	906	892	5113077760		195	5.29	.014	877	true	10.8	5.77	365150208		1	.912	.00	.011	.112			true	9.94	5.50	358088704		.435	.501	1.36	.392	.371	.358	.197	.012	.209	.129	true	9.03	5.07	323022848		4	.777	.109	.970	.355	.009	.001	.00	.00	.466	.160	2
minepump_spec4_product23_true-unreach-call.cil.c	timeout	906	889	5155328000		203	5.66	.011	874	true	11.0	5.86	351170560		1	.711	.00	.005	.079			true	9.63	5.42	361668608		.551	.486	1.25	.346	.396	.378	.216	.030	.246	.153	true	9.19	5.16	326230016		4	.344	.110	1.43	.324	.025	.001	.00	.00	.028	.168	2
minepump_spec4_product24_true-unreach-call.cil.c	timeout	906	891	5136867328		198	5.64	.006	875	true	11.8	6.33	350609408		1	.698	.00	.005	.022			true	9.54	5.35	356052992		.612	.418	1.24	.365	.339	.322	.191	.030	.221	.143	true	9.18	5.07	324009984		4	.360	.520	1.30	.304	.017	.002	.00	.00	.020	.145	2
minepump_spec4_product25_true-unreach-call.cil.c	timeout	906	892	5161005056		224	5.39	.017	876	true	9.32	5.01	349265920		1	.528		.005				true	8.38	4.68	343691264		.467	.311	.869	.280	.237	.229	.109	.009	.118	.088	true	8.69	4.85	314245120		5	.301	.108	1.19	.255	.012	.003	.00	.00	.022	.124	3
minepump_spec4_product26_true-unreach-call.cil.c	timeout	906	891	5115670528		195	5.14	.011	877	true	9.64	5.20	348868608		1	.483		.005				true	8.73	4.84	349196288		.553	.387	.851	.203	.316	.305	.156	.012	.168	.132	true	8.36	4.67	316182528		4	.282	.080	1.07	.246	.010	.001	.00	.00	.023	.125	2
minepump_spec4_product27_true-unreach-call.cil.c	timeout	906	891	5108039680		206	5.48	.017	876	true	9.98	5.36	359116800		1	.434		.012				true	8.98	5.01	346906624		.573	.386	.882	.197	.301	.290	.143	.026	.169	.114	true	8.91	4.90	316035072		5	.270	.097	1.34	.257	.017	.004	.00	.00	.013	.156	3
minepump_spec4_product28_true-unreach-call.cil.c	timeout	907	892	5118230528		199	5.41	.022	876	true	10.1	5.42	340271104		1	.606	.001	.015	.063			true	8.59	4.77	345137152		.504	.384	.877	.243	.287	.275	.151	.025	.176	.128	true	8.57	4.80	316846080		4	.319	.079	1.12	.246	.017	.00	.00	.00	.024	.110	2
minepump_spec4_product29_true-unreach-call.cil.c	timeout	906	890	5206351872		226	6.11	.014	872	true	10.5	5.69	363950080		1	.399		.013				true	9.22	5.15	361062400		.581	.416	1.13	.281	.341	.334	.173	.011	.184	.114	true	8.88	5.01	323031040		4	.716	.093	.926	.384	.011	.002	.00	.00	.024	.124	2
minepump_spec4_product30_true-unreach-call.cil.c	timeout	906	892	5128073216		197	4.57	.014	877	true	10.7	5.84	371507200		1	.401		.006				true	9.53	5.27	357543936		.640	.436	1.17	.330	.355	.336	.198	.023	.221	.159	true	8.64	4.90	323293184		4	.681	.092	.917	.305	.007	.001	.00	.00	.023	.144	2
minepump_spec4_product31_true-unreach-call.cil.c	timeout	906	889	5172875264		195	5.36	.017	874	true	10.7	5.79	360468480		1	.862	.002	.008	.049			true	9.96	5.55	359563264		.484	.512	1.28	.308	.411	.395	.217	.041	.258	.193	true	9.07	5.06	323465216		4	.759	.088	.959	.311	.018	.003	.00	.00	.034	.158	2
minepump_spec4_product32_true-unreach-call.cil.c	timeout	906	892	5092839424		204	5.58	.015	876	true	11.0	5.87	360112128		1	1.20		.006				true	9.30	5.17	358592512		.646	.500	1.15	.273	.417	.397	.206	.024	.230	.150	true	9.12	5.13	326823936		4	.368	.099	1.43	.309	.011	.001	.00	.00	.022	.164	2
minepump_spec4_product49_true-unreach-call.cil.c	timeout	906	889	5168111616		93	5.43	92.3	763	true	180	90.7	3150860288		15	3.02	3.69	.010	8.47	29.2	38.8	true	9.76	5.35	356974592		.595	.553	1.37	.328	.482	.466	.255	.046	.301	.140	true	9.86	5.67	339316736		5	.596	.149	1.76	.488	.015	.002	.00	.00	.059	.281	1
minepump_spec4_product50_true-unreach-call.cil.c	timeout	906	891	5115121664		91	5.72	88.2	769	true	241	121	4078383104		17	3.23	5.10	.025	11.6	30.8	62.7	true	9.82	5.47	371200000		.548	.559	1.39	.345	.461	.447	.258	.029	.287	.129	true	8.97	5.03	327958528		3	.371	.468	1.44	.428	.014	.002	.00	.00	.027	.131	1
minepump_spec4_product51_true-unreach-call.cil.c	timeout	907	893	3657801728		82	5.34	418	443	true	230	116	3965968384		16	3.04	13.0	.012	10.5	28.0	54.8	true	11.2	6.18	385073152		.608	.880	1.99	.488	.748	.727	.398	.080	.478	.202	true	9.66	5.40	334012416		4	.466	.111	1.56	.808	.012	.002	.00	.00	.034	.158	1
minepump_spec4_product52_true-unreach-call.cil.c	timeout	904	891	3327643648		75	5.06	312	551	true	139	70.1	2245005312		11	3.19	4.19	.011	5.57	24.5	25.5	true	10.8	5.98	384180224		.543	.941	1.99	.459	.799	.688	.418	.080	.498	.214	true	10.1	5.71	348073984		3	.606	.149	1.63	.474	.028	.004	.00	.00	.031	.121	0
minepump_spec4_product53_true-unreach-call.cil.c	timeout	905	892	3732959232		78	5.86	61.0	799	true	148	74.8	2718486528		12	3.07	2.74	.006	6.61	25.6	29.6	true	13.0	7.09	377946112		.789	.986	2.34	.499	.839	.806	.466	.077	.543	.253	true	11.8	6.64	360988672		5	.755	.154	2.34	.671	.040	.003	.00	.00	.059	.349	1
minepump_spec4_product54_true-unreach-call.cil.c	timeout	905	891	3714043904		77	6.12	67.8	790	true	176	88.7	2995793920		13	3.14	3.52	.017	8.21	28.8	37.4	true	12.8	7.01	406687744		.244	1.41	3.30	.996	1.23	1.18	.743	.166	.909	.480	true	9.88	5.54	344739840		3	.419	.124	1.87	.941	.021	.001	.00	.00	.034	.146	1
minepump_spec4_product55_true-unreach-call.cil.c	timeout	906	892	3637100544		74	5.97	385	474	true	141	71.2	2515992576		10	3.30	4.34	.012	5.61	23.3	26.7	true	13.2	7.17	401891328		.621	1.36	3.01	.641	1.20	1.17	.779	.114	.893	.287	true	9.97	5.57	341389312		3	.423	.585	1.77	.505	.032	.001	.00	.00	.041	.150	1
minepump_spec4_product56_true-unreach-call.cil.c	timeout	904	891	3320840192		68	5.53	316	547	true	176	88.7	3227058176		12	2.88	6.52	.006	9.07	27.8	35.0	true	11.9	6.49	382189568		.261	1.11	2.69	.440	.949	.915	.551	.128	.679	.300	true	11.8	6.68	356573184		6	.834	.131	2.38	1.13	.022	.002	.00	.00	.046	.374	1
minepump_spec4_product57_true-unreach-call.cil.c	timeout	905	891	3689918464		78	5.71	61.5	798	true	241	121	3806273536		16	2.64	4.94	.004	12.0	35.3	59.0	true	11.4	6.30	371458048		.609	1.00	2.10	.465	.851	.828	.509	.097	.606	.247	true	9.56	5.39	335065088		3	.443	.153	1.55	.391	.048	.002	.00	.00	.031	.141	1
minepump_spec4_product58_true-unreach-call.cil.c	timeout	906	892	3683807232		77	5.53	64.1	798	true	206	103	3668402176		14	2.99	4.83	.017	10.3	29.7	48.0	true	12.6	6.91	378753024		.719	1.11	2.39	.479	.922	.896	.540	.101	.641	.294	true	9.98	5.56	342339584		3	.476	.149	1.55	.440	.028	.001	.00	.00	.035	.144	1
minepump_spec4_product59_true-unreach-call.cil.c	timeout	907	893	3580981248		74	5.63	415	447	true	199	100	3237326848		13	3.00	7.77	.010	9.04	26.7	46.5	true	11.5	6.41	374251520		.656	1.18	2.17	.413	1.06	.990	.643	.122	.765	.294	true	10.4	5.80	345120768		4	.561	.145	1.75	.378	.023	.003	.00	.00	.037	.239	1
minepump_spec4_product60_true-unreach-call.cil.c	timeout	906	891	3203076096		66	5.23	325	539	true	203	102	3531526144		13	3.01	6.87	.034	9.30	27.4	48.4	true	11.5	6.37	386019328		.223	1.09	2.66	.837	1.00	.981	.615	.117	.732	.312	true	10.2	5.65	340938752		3	.510	.108	1.67	.935	.012	.00	.00	.00	.045	.154	1
minepump_spec4_product61_true-unreach-call.cil.c	timeout	906	891	3650867200		69	6.11	74.1	786	true	149	74.9	2712330240		11	3.39	3.09	.012	8.18	26.7	25.2	true	14.7	7.97	413380608		.272	1.61	3.88	.592	1.45	1.36	.796	.167	.963	.550	true	10.5	5.90	345223168		3	.449	.593	2.09	.598	.014	.001	.00	.00	.030	.164	1
minepump_spec4_product62_true-unreach-call.cil.c	timeout	905	890	3572269056		67	6.46	81.8	778	true	152	76.8	2606301184		11	3.98	2.83	.007	7.44	29.4	24.5	true	14.1	7.70	421801984		.244	1.69	3.99	1.13	1.52	1.46	.848	.244	1.09	.550	true	10.5	5.92	347103232		3	.448	.157	2.10	1.03	.019	.001	.00	.00	.030	.156	1
minepump_spec4_product63_true-unreach-call.cil.c	timeout	913	899	5247086592						true	110	55.7	2333605888		8	3.09	3.62	.006	4.91	22.0	15.0	true	15.7	8.50	431091712		.264	1.97	4.51	1.16	1.73	1.68	.795	.447	1.24	.783	true	10.4	5.84	352833536		3	.483	.167	2.02	.541	.029	.003	.00	.00	.028	.178	1
minepump_spec4_product64_true-unreach-call.cil.c	timeout	904	890	3485556736		63	6.51	293	567	true	157	79.5	2722811904		10	2.96	6.03	.004	7.18	26.3	29.3	true	13.4	7.47	403771392		.282	1.84	3.60	.679	1.40	1.32	.719	.225	.944	.613	true	10.5	5.88	357105664		3	.505	.193	1.91	.788	.015	.001	.00	.00	.029	.189	1
minepump_spec5_product01_true-unreach-call.cil.c	timeout	906	892	5097181184		191	4.76	.012	878	true	10.2	5.46	344145920		1	.476	.001	.005	.092			true	8.05	4.47	338948096		.404	.231	.650	.206	.183	.173	.095	.006	.101	.115	true	8.23	4.61	316084224		1	.047	.748	1.20	.231	.678	.668	.567	.014	.583	.023	0	.589
minepump_spec5_product02_true-unreach-call.cil.c	timeout	905	891	5108150272		179	5.02	.021	877	true	9.98	5.39	363708416		1	.619	.00	.006	.041			true	7.86	4.42	343351296		.430	.254	.674	.230	.208	.194	.101	.009	.110	.121	true	8.25	4.61	313528320		1	.047	.803	1.29	.231	.722	.715	.637	.011	.650	.029	0	.653
minepump_spec5_product03_true-unreach-call.cil.c	timeout	905	889	5141774336		183	4.86	.015	875	true	12.1	6.46	384008192		1	.578	.00	.014	.023			true	8.20	4.57	341000192		.413	.291	.673	.175	.232	.219	.111	.008	.119	.133	true	8.13	4.58	311054336		1	.047	.644	1.18	.276	.580	.569	.090	.004	.095	.027	0	.109
minepump_spec5_product04_true-unreach-call.cil.c	timeout	905	891	3691892736		173	5.04	.014	877	true	11.9	6.28	345800704		1	.893	.00	.004	.048			true	8.34	4.69	340914176		.485	.279	.682	.193	.224	.207	.107	.006	.113	.131	true	7.95	4.47	310976512		1	.039	.255	1.15	.262	.195	.193	.111	.009	.122	.031	0	.126
minepump_spec5_product05_true-unreach-call.cil.c	timeout	906	892	5113929728		196	5.39	.010	877	true	9.69	5.18	355135488		1	.349		.006				true	8.86	4.96	337461248		.513	.402	.878	.213	.308	.300	.191	.012	.203	.217	true	8.65	4.79	315514880		1	.045	.351	1.37	.267	.294	.280	.176	.013	.190	.030	0	.195
minepump_spec5_product06_true-unreach-call.cil.c	timeout	905	891	3699761152		173	4.73	.009	877	true	11.1	5.94	353800192		1	.660	.00	.005	.057			true	8.40	4.69	336453632		.467	.371	.853	.232	.310	.292	.163	.015	.178	.192	true	9.23	5.05	310206464		1	.049	.376	1.48	.257	.313	.299	.190	.017	.208	.029	0	.214
minepump_spec5_product07_true-unreach-call.cil.c	timeout	906	890	5156306944		184	5.17	.009	875	true	12.4	6.60	391757824		1	.593	.00	.005	.036			true	8.44	4.74	342401024		.459	.384	.858	.226	.312	.303	.205	.012	.217	.230	true	8.02	4.52	315379712		1	.051	.366	1.19	.258	.317	.299	.187	.008	.196	.031	0	.204
minepump_spec5_product08_true-unreach-call.cil.c	timeout	906	893	5137575936		177	5.12	.012	878	true	12.0	6.45	365473792		1	.797	.00	.009	.075			true	8.74	4.85	338518016		.525	.400	.863	.245	.312	.303	.178	.013	.191	.216	true	8.63	4.83	314654720		1	.044	.366	1.44	.260	.273	.266	.149	.011	.161	.044	0	.166
minepump_spec5_product09_true-unreach-call.cil.c	timeout	906	891	5108625408		189	4.93	.007	877	true	10.3	5.54	352563200		1	.595	.001	.005	.057			true	7.91	4.46	336580608		.353	.265	.676	.207	.196	.185	.099	.008	.107	.118	true	8.03	4.44	303685632		1	.039	.260	1.15	.231	.198	.193	.097	.008	.106	.038	0	.113
minepump_spec5_product10_true-unreach-call.cil.c	timeout	906	892	5322633216		179	5.16	.011	877	true	10.3	5.57	341204992		1	.766	.00	.010	.084			true	8.24	4.63	334168064		.434	.289	.703	.206	.232	.223	.117	.009	.126	.140	true	7.81	4.38	307326976		1	.048	.629	1.06	.184	.558	.550	.463	.009	.473	.023	0	.480
minepump_spec5_product11_true-unreach-call.cil.c	timeout	906	892	5119651840		183	4.65	.014	878	true	10.5	5.62	351772672		1	.947		.013				true	8.46	4.71	338214912		.543	.258	.721	.219	.201	.188	.096	.007	.103	.119	true	8.35	4.69	305295360		1	.044	.731	1.25	.256	.659	.641	.109	.007	.117	.026	0	.122
minepump_spec5_product12_true-unreach-call.cil.c	timeout	906	892	3667542016		172	5.21	.012	878	true	11.7	6.18	352477184		1	.735	.001	.013	.022			true	7.97	4.49	343535616		.420	.269	.666	.202	.211	.206	.096	.007	.103	.119	true	7.94	4.36	308428800		1	.039	.643	1.13	.242	.557	.552	.473	.010	.485	.040	0	.488
minepump_spec5_product13_true-unreach-call.cil.c	timeout	906	892	5114486784		192	5.13	.013	877	true	10.6	5.71	365129728		1	.477	.00	.003	.056			true	8.49	4.73	344403968		.462	.339	.840	.238	.274	.263	.161	.012	.173	.184	true	8.31	4.64	313372672		1	.046	.353	1.39	.701	.296	.288	.183	.011	.195	.037	0	.201
minepump_spec5_product14_true-unreach-call.cil.c	timeout	906	892	5135319040		177	4.93	.013	878	true	10.8	5.80	361889792		1	.730	.001	.009	.078			true	8.76	4.86	340783104		.494	.338	.828	.245	.284	.278	.165	.015	.180	.193	true	8.51	4.72	315854848		1	.047	.396	1.43	.239	.323	.321	.173	.016	.190	.032	0	.200
minepump_spec5_product15_true-unreach-call.cil.c	timeout	906	892	5141508096		182	5.12	.012	878	true	10.9	5.88	351961088		1	.761	.00	.009	.387			true	8.05	4.49	340967424		.390	.352	.867	.281	.285	.279	.167	.013	.180	.198	true	8.39	4.73	306720768		1	.048	.358	1.32	.258	.288	.278	.169	.012	.182	.031	0	.192
minepump_spec5_product16_true-unreach-call.cil.c	timeout	906	892	5142224896		180	5.42	.010	877	true	11.3	6.00	346800128		1	.649	.001	.005	.081			true	8.51	4.82	350691328		.392	.370	.885	.246	.283	.277	.168	.011	.179	.197	true	8.34	4.71	313262080		1	.046	.731	1.31	.233	.663	.645	.509	.013	.523	.031	0	.533
minepump_spec5_product17_true-unreach-call.cil.c	timeout	906	888	5188898816		195	5.23	.010	873	true	10.8	5.78	373063680		1	.605	.00	.014	.023			true	8.83	4.90	344961024		.484	.401	.919	.245	.335	.328	.199	.017	.216	.232	true	8.72	4.90	314417152		1	.055	.369	1.40	.272	.305	.300	.199	.013	.214	.036	0	.219
minepump_spec5_product18_true-unreach-call.cil.c	timeout	910	894	5173440512		176	4.70	.009	881	true	10.3	5.54	362782720		1	.791		.005				true	8.86	4.96	340332544		.518	.386	.882	.220	.319	.310	.197	.013	.210	.220	true	8.62	4.85	308224000		1	.057	.420	1.52	.804	.325	.317	.199	.009	.210	.041	0	.215
minepump_spec5_product19_true-unreach-call.cil.c	timeout	906	889	5204885504		181	5.50	.019	874	true	11.9	6.34	354787328		1	.587	.001	.011	.030			true	8.74	4.89	354967552		.464	.434	.967	.250	.381	.368	.222	.028	.250	.268	true	8.73	4.87	310599680		1	.052	.929	1.54	.252	.824	.812	.721	.015	.737	.044	0	.739
minepump_spec5_product20_true-unreach-call.cil.c	timeout	906	888	5206736896		185	5.37	.014	873	true	11.2	6.05	374566912		1	.778	.00	.008	.099			true	8.86	4.94	349044736		.552	.513	1.04	.257	.430	.417	.260	.023	.283	.292	true	8.68	4.84	310067200		1	.053	.382	1.37	.264	.311	.299	.173	.011	.186	.032	0	.198
minepump_spec5_product21_true-unreach-call.cil.c	timeout	906	890	5134893056		192	5.31	.010	872	true	11.3	6.01	342376448		1	.895		.011				true	9.50	5.32	348663808		.088	.497	1.69	.358	.388	.375	.244	.023	.267	.283	true	9.66	5.35	332771328		1	.056	.564	1.81	.804	.461	.436	.295	.021	.318	.043	0	.321
minepump_spec5_product22_true-unreach-call.cil.c	timeout	905	887	5208567808		180	5.49	.010	872	true	11.7	6.30	379412480		1	1.05	.00	.019	.100			true	9.08	5.09	349995008		.489	.549	1.23	.325	.444	.430	.260	.017	.277	.288	true	9.29	5.18	326180864		1	.055	.531	1.68	.773	.394	.373	.235	.020	.256	.041	0	.262
minepump_spec5_product23_true-unreach-call.cil.c	timeout	906	892	5132849152		180	5.51	.013	876	true	12.1	6.46	387649536		1	1.04	.001	.006	.040			true	9.05	5.06	349786112		.439	.518	1.15	.256	.437	.426	.283	.019	.302	.317	true	9.55	5.30	329732096		1	.056	.503	1.80	.899	.392	.376	.253	.020	.274	.044	0	.281
minepump_spec5_product24_true-unreach-call.cil.c	timeout	906	892	5136318464		181	5.53	.006	877	true	11.9	6.34	382943232		1	1.06	.00	.014	.151			true	9.13	5.07	349081600		.568	.560	1.18	.295	.469	.450	.279	.018	.297	.316	true	9.55	5.32	334794752		1	.057	.504	1.70	.839	.414	.399	.262	.021	.285	.042	0	.289
minepump_spec5_product25_true-unreach-call.cil.c	timeout	906	892	5117915136		196	5.24	.012	877	true	9.96	5.39	360345600		1	.740	.00	.008	.122			true	9.15	5.07	345149440		.498	.417	.921	.249	.361	.349	.235	.013	.248	.262	true	8.94	4.97	319295488		1	.048	.466	1.53	.326	.360	.349	.225	.015	.242	.037	0	.244
minepump_spec5_product26_true-unreach-call.cil.c	timeout	905	891	3708538880		174	4.84	.012	877	true	11.0	5.92	352837632		1	.750	.00	.015	.085			true	8.42	4.73	345079808		.449	.407	.896	.249	.338	.335	.222	.011	.233	.248	true	8.67	4.83	311070720		1	.049	.414	1.46	.743	.342	.334	.219	.017	.237	.034	0	.240
minepump_spec5_product27_true-unreach-call.cil.c	timeout	905	888	5222174720		189	5.40	.011	873	true	12.0	6.38	384757760		1	.739	.00	.009	.078			true	7.98	4.49	341483520		.384	.387	.860	.237	.322	.314	.191	.012	.203	.219	true	8.51	4.77	314744832		1	.050	.760	1.38	.288	.693	.685	.586	.014	.601	.034	0	.608
minepump_spec5_product28_true-unreach-call.cil.c	timeout	906	888	5221629952		182	5.38	.012	873	true	11.7	6.28	379379712		1	.979	.001	.004	.097			true	8.70	4.86	346832896		.486	.378	.882	.221	.298	.286	.157	.013	.170	.186	true	8.53	4.75	309792768		1	.049	.403	1.38	.264	.332	.322	.227	.014	.242	.036	0	.245
minepump_spec5_product29_true-unreach-call.cil.c	timeout	906	891	5130698752		196	5.37	.016	875	true	11.7	6.24	374779904		1	.840	.001	.009	.027			true	9.65	5.33	348971008		.506	.649	1.37	.339	.557	.548	.360	.020	.380	.400	true	9.55	5.30	323420160		1	.057	.686	1.86	.779	.581	.567	.416	.020	.437	.050	0	.451
minepump_spec5_product30_true-unreach-call.cil.c	timeout	905	888	5197209600		177	5.29	.006	873	true	11.8	6.24	357842944		1	.749	.00	.025	.265			true	9.07	5.04	350539776		.528	.519	1.15	.320	.421	.396	.260	.020	.280	.304	true	9.52	5.26	331419648		1	.054	.948	1.72	.376	.836	.828	.684	.019	.704	.039	0	.708
minepump_spec5_product31_true-unreach-call.cil.c	timeout	905	891	5135753216		183	5.18	.010	876	true	11.5	6.12	375132160		1	.986		.009				true	9.44	5.23	349634560		.429	.655	1.29	.283	.562	.553	.383	.023	.406	.420	true	9.68	5.38	323325952		1	.061	.491	1.75	.831	.398	.381	.251	.021	.274	.042	0	.276
minepump_spec5_product32_true-unreach-call.cil.c	timeout	906	888	5257560064		181	5.15	.017	872	true	12.9	6.84	398938112		1	.986	.001	.005	.049			true	8.88	4.92	354185216		.538	.503	1.14	.295	.417	.410	.261	.019	.280	.302	true	9.27	5.19	322174976		1	.054	.546	1.72	.720	.440	.420	.283	.020	.304	.042	0	.310
minepump_spec5_product33_true-unreach-call.cil.c	timeout	909	894	5215121408		116	4.80	83.3	775	true	23.8	12.4	591372288		1	.827	.060	2.32	.153	4.60	.861	true	8.87	4.93	350531584		.461	.410	1.03	.272	.328	.317	.161	.027	.188	.210	true	9.53	5.40	333987840		6	.872	.476	1.32	.303	.411	.400	.254	.017	.310	.236	1	.279
minepump_spec5_product34_true-unreach-call.cil.c	timeout	907	892	5101244416		105	4.70	65.8	793	true	23.6	12.3	615116800		1	.860	.095	2.00	.043	4.36	.957	true	8.73	4.87	352722944		.519	.463	1.02	.252	.386	.377	.190	.037	.227	.252	true	8.91	5.05	320352256		3	.323	.294	1.38	.695	.234	.221	.136	.012	.184	.111	1	.151
minepump_spec5_product35_true-unreach-call.cil.c	timeout	906	893	5113446400		104	5.02	75.9	783	true	62.8	31.8	1193754624		6	1.83	1.77	9.13	2.27	12.3	8.10	true	9.03	5.03	347824128		.511	.590	1.16	.241	.502	.481	.281	.057	.338	.361	true	9.18	5.14	322179072		3	.298	.814	1.45	.261	.714	.704	.149	.014	.187	.111	1	.168
minepump_spec5_product36_true-unreach-call.cil.c	timeout	905	892	1925718016		60	3.45	703	172	true	55.3	28.1	1033682944		4	1.84	1.78	5.49	1.93	10.7	6.34	true	13.2	7.31	387104768		.866	1.85	2.98	.401	1.72	1.68	.929	.303	1.23	1.31	true	13.2	8.28	362897408		20	1.57	1.19	3.42	.468	1.08	1.07	.854	.034	1.02	1.28	1	.904
minepump_spec5_product37_true-unreach-call.cil.c	timeout	904	892	2905546752		65	4.52	561	309	true	30.0	15.5	661860352		1	1.40	.110	2.68	.339	6.29	1.21	true	12.4	6.87	385724416		.568	1.53	2.81	.503	1.30	1.25	.717	.165	.882	.931	true	14.1	8.48	367190016		14	1.39	.931	3.55	.577	.817	.786	.567	.045	.723	1.01	1	.624
minepump_spec5_product38_true-unreach-call.cil.c	timeout	906	892	2921250816		64	4.65	556	315	true	27.6	14.2	688541696		1	1.09	.100	.006	.079	5.26	2.10	true	13.4	7.23	394772480		.693	1.71	3.02	.515	1.56	1.52	.831	.228	1.06	1.13	true	13.7	8.35	358588416		14	1.55	.907	3.42	.572	.790	.764	.538	.037	.707	.992	1	.583
minepump_spec5_product39_true-unreach-call.cil.c	timeout	904	891	2942156800		62	4.29	601	268	true	68.0	34.5	1331023872		5	2.34	1.51	9.56	1.99	13.9	8.86	true	13.1	7.25	381267968		.672	1.69	2.99	.485	1.53	1.50	.872	.248	1.12	1.19	true	14.2	8.64	358133760		14	1.39	.964	3.75	.958	.831	.806	.572	.048	.740	1.07	1	.630
minepump_spec5_product40_true-unreach-call.cil.c	timeout	905	892	2142195712		57	4.30	668	205	true	421	212	4662988800		20	3.50	38.4	.005	20.5	38.8	101	true	12.5	6.87	389263360		.568	1.63	2.84	.460	1.48	1.44	.868	.228	1.10	1.17	true	12.0	7.02	353730560		10	.926	.859	2.81	.517	.748	.719	.492	.040	.583	.575	1	.539
minepump_spec5_product41_true-unreach-call.cil.c	timeout	905	892	3516014592		84	4.30	439	426	true	26.9	13.9	602103808		1	.961	.043	2.26	.148	5.44	.987	true	10.3	5.72	367943680		.482	1.08	1.91	.314	.967	.949	.582	.118	.700	.728	true	9.47	5.38	326545408		3	.359	.444	1.60	.325	.350	.339	.221	.018	.265	.128	1	.247
minepump_spec5_product42_true-unreach-call.cil.c	timeout	907	888	3601924096		83	4.51	430	431	true	24.2	12.5	614031360		1	.858	.127	2.06	.131	3.21	2.90	true	11.2	6.24	367595520		.617	1.10	2.14	.412	.960	.940	.532	.118	.650	.686	true	10.3	5.99	338231296		6	.590	.573	2.03	.353	.473	.455	.314	.021	.389	.315	1	.343
minepump_spec5_product43_true-unreach-call.cil.c	timeout	907	893	3231801344		76	4.43	489	378	true	66.0	33.5	1175670784		5	2.18	2.17	8.91	2.73	12.9	7.65	true	11.1	6.15	367345664		.595	1.27	2.16	.390	1.16	1.12	.648	.155	.803	.863	true	12.0	7.16	358100992		11	1.42	.775	2.32	.462	.633	.621	.439	.029	.536	.605	2	.474
minepump_spec5_product44_true-unreach-call.cil.c	timeout	905	892	1972707328		55	3.40	692	183	true	44.2	22.5	896372736		3	1.54	1.17	.006	1.44	7.72	5.52	true	13.4	7.56	390955008		.710	2.23	3.43	.482	2.06	2.04	1.20	.369	1.57	1.64	true	17.8	11.8	378540032		21	4.07	1.14	4.24	.585	1.03	1.01	.727	.056	1.01	1.88	0	.794
minepump_spec5_product45_true-unreach-call.cil.c	timeout	905	892	2064257024		52	4.26	675	199	true	33.2	17.1	730206208		1	1.27	.821	2.96	.318	7.18	1.57	true	13.1	7.20	395165696		.632	1.66	3.07	.605	1.49	1.46	.872	.201	1.07	1.14	true	15.8	9.77	363167744		14	1.88	1.66	4.36	.627	1.44	1.43	.682	.054	.865	1.31	1	.748
minepump_spec5_product46_true-unreach-call.cil.c	timeout	905	892	2046054400		51	4.24	670	205	true	27.9	14.4	660959232		1	1.34	.113	2.27	.097	5.94	1.24	true	14.3	7.99	405118976		.887	2.18	3.72	.513	1.99	1.96	1.32	.225	1.55	1.59	true	16.1	9.77	374644736		14	2.09	1.58	4.16	.545	1.41	1.40	.764	.050	.928	1.30	1	1.21
minepump_spec5_product47_true-unreach-call.cil.c	timeout	905	891	2129080320		50	4.62	693	179	true	84.5	42.7	1557684224		6	2.78	2.07	.012	2.77	16.5	11.4	true	16.5	9.01	425435136		1.01	2.59	4.16	.469	2.38	2.33	1.49	.390	1.88	1.93	true	13.5	8.02	367632384		10	1.06	.966	3.52	1.08	.802	.785	.531	.047	.649	.841	1	.583
minepump_spec5_product48_true-unreach-call.cil.c	timeout	906	891	3014717440		54	4.60	616	254	true	226	114	3390763008		15	3.69	19.3	.008	10.8	30.3	40.8	true	12.7	7.09	388050944		.603	1.78	3.08	.507	1.66	1.65	.924	.322	1.25	1.29	true	13.1	7.88	359178240		10	1.12	1.36	3.34	.533	.832	.790	.576	.049	.695	.791	1	.632
minepump_spec5_product49_true-unreach-call.cil.c	timeout	906	893	5126254592		91	5.03	73.3	786	true	27.7	14.3	632975360		1	1.16	.078	2.53	.116	5.62	1.20	true	11.3	6.26	382406656		.571	1.15	2.22	.321	1.02	.982	.578	.087	.665	.710	true	9.93	5.58	329957376		3	.324	.933	1.85	.397	.808	.795	.664	.020	.710	.137	1	.691
minepump_spec5_product50_true-unreach-call.cil.c	timeout	906	892	5121679360		89	5.47	78.4	779	true	29.1	15.0	662024192		1	1.17	.112	2.60	.124	6.33	1.18	true	11.4	6.32	383238144		.607	1.10	2.29	.456	.975	.934	.490	.100	.590	.660	true	11.4	6.50	352714752		5	.617	.716	2.51	.455	.606	.574	.401	.035	.506	.432	1	.445
minepump_spec5_product51_true-unreach-call.cil.c	timeout	908	893	5143244800		90	5.84	99.6	757	true	60.2	30.6	1041088512		3	2.44	1.76	6.12	1.38	12.8	6.38	true	11.4	6.36	374075392		.721	1.10	2.15	.411	.977	.958	.533	.118	.651	.696	true	11.4	6.52	334032896		6	.630	.650	2.50	.911	.547	.530	.353	.034	.441	.422	2	.407
minepump_spec5_product52_true-unreach-call.cil.c	timeout	904	892	2944012288		60	4.50	610	261	true	61.8	31.4	1037090816		3	2.22	1.40	6.05	1.68	12.8	6.78	true	11.3	6.28	372670464		.570	1.09	2.21	.496	.952	.920	.503	.121	.624	.657	true	14.3	8.82	364855296		13	1.49	1.00	3.90	.664	.878	.854	.620	.047	.772	1.14	1	.675
minepump_spec5_product53_true-unreach-call.cil.c	timeout	906	893	5203808256		78	6.03	77.5	782	true	33.0	16.9	804737024		1	1.48	.390	3.04	.237	7.35	1.13	true	14.1	7.59	401190912		.372	1.38	3.48	.696	1.20	1.16	.663	.148	.811	.849	true	10.5	5.97	345522176		3	.398	.575	2.25	.942	.476	.457	.323	.021	.367	.185	1	.351
minepump_spec5_product54_true-unreach-call.cil.c	timeout	905	891	3763580928		75	6.22	64.5	793	true	35.7	18.3	812285952		1	2.03	.795	2.85	.221	7.30	1.09	true	14.7	7.86	401428480		.388	1.59	3.90	1.14	1.34	1.29	.753	.173	.926	.975	true	12.5	7.26	366194688		5	.748	1.22	3.08	.708	1.06	1.05	.440	.043	.534	.377	1	.910
minepump_spec5_product55_true-unreach-call.cil.c	timeout	906	891	5246029824		78	6.49	73.8	783	true	72.3	36.6	1451524096		5	2.60	2.36	.004	1.51	16.6	6.94	true	14.4	7.86	403410944		.663	1.87	3.57	.606	1.69	1.64	.885	.315	1.20	1.26	true	12.6	7.30	370466816		5	.827	.780	3.03	.685	.640	.611	.434	.033	.520	.360	1	.476
minepump_spec5_product56_true-unreach-call.cil.c	timeout	904	890	3074801664		56	5.47	537	330	true	59.0	29.8	1028972544		3	2.43	1.04	5.71	1.32	13.1	5.67	true	14.3	7.82	414220288		.230	1.65	3.74	1.08	1.49	1.45	.897	.203	1.10	1.14	true	14.9	8.64	381685760		8	1.27	1.56	3.98	.831	1.38	1.34	.666	.051	.788	.677	1	.721
minepump_spec5_product57_true-unreach-call.cil.c	timeout	905	891	2997850112		58	4.93	557	311	true	32.8	16.8	808603648		1	1.33	.166	3.12	.479	7.13	1.88	true	12.1	6.66	377188352		.657	1.24	2.42	.475	1.12	1.09	.663	.092	.755	.809	true	11.7	6.76	349650944		5	.794	.724	2.58	.475	.606	.591	.411	.036	.526	.381	1	.454
minepump_spec5_product58_true-unreach-call.cil.c	timeout	904	891	2969849856		58	4.84	594	275	true	31.4	16.2	717971456		1	1.26	.077	.005	.083	7.58	1.33	true	11.2	6.18	376287232		.511	1.11	2.23	.411	.953	.933	.495	.105	.600	.643	true	11.9	6.83	355926016		5	.732	1.41	2.72	.490	1.25	1.23	1.05	.037	1.14	.349	1	1.09
minepump_spec5_product59_true-unreach-call.cil.c	timeout	905	891	3017904128		57	5.15	615	253	true	63.0	32.1	1175068672		4	2.50	2.51	.006	1.38	13.6	5.44	true	11.0	6.14	366407680		.591	1.15	2.17	.339	1.00	.979	.568	.105	.673	.707	true	12.0	6.82	350248960		6	.834	.754	2.64	.948	.645	.632	.434	.037	.529	.370	2	.480
minepump_spec5_product60_true-unreach-call.cil.c	timeout	904	891	2986418176		55	4.73	555	314	true	253	127	4128813056		14	3.00	15.6	.013	10.8	29.2	61.2	true	12.2	6.70	372383744		.726	1.20	2.31	.442	1.06	1.01	.600	.139	.739	.778	true	12.5	7.12	349827072		5	.767	.773	2.82	1.07	.689	.675	.491	.038	.594	.393	1	.535
minepump_spec5_product61_true-unreach-call.cil.c	timeout	905	891	3058290688		55	5.69	495	372	true	42.9	21.9	891396096		1	2.45	.780	4.13	.335	8.09	2.75	true	14.8	8.05	415129600		.308	1.56	3.91	1.23	1.37	1.32	.766	.177	.943	1.00	true	11.8	6.62	362262528		3	.896	.700	2.37	.651	.534	.507	.357	.033	.420	.311	1	.397
minepump_spec5_product62_true-unreach-call.cil.c	timeout	905	891	3078393856		55	5.30	517	350	true	42.5	21.8	998920192		1	1.96	.852	3.90	.187	8.84	2.93	true	14.1	7.56	415444992		.263	1.54	3.63	.766	1.37	1.34	.883	.094	.977	1.01	true	13.8	7.92	367714304		5	.924	.999	3.63	.745	.869	.829	.578	.045	.681	.519	1	.627
minepump_spec5_product63_true-unreach-call.cil.c	timeout	905	891	3053686784		54	5.95	589	275	true	61.5	31.2	1046536192		3	2.74	.979	7.00	1.16	14.7	4.87	true	15.4	8.30	386637824		.291	1.83	4.32	.793	1.64	1.55	.901	.214	1.11	1.17	true	14.1	8.01	369418240		5	.884	.988	3.64	1.25	.810	.783	.574	.049	.683	.495	1	.627
minepump_spec5_product64_true-unreach-call.cil.c	timeout	904	890	3070738432		51	5.65	519	347	true	289	145	4451389440		14	3.42	15.9	.003	16.5	37.7	63.0	true	13.8	7.54	399405056		.731	1.53	3.34	.772	1.31	1.27	.783	.145	.928	.960	true	14.3	8.20	371257344		5	.915	.954	3.75	.766	.815	.764	.522	.048	.628	.546	1	.586
minepump_spec5_productSimulator_true-unreach-call.cil.c	timeout	905	888	2367770624		45	9.91	665	196	true	95.0	48.0	1703079936		4	4.49	1.29	.005	1.17	25.3	6.32	true	22.9	13.0	586473472		.776	3.68	8.53	1.97	3.19	3.11	1.68	.703	2.38	2.48	true	27.8	17.6	631816192		21	4.54	2.20	9.31	1.95	1.87	1.82	1.30	.136	1.60	2.79	2	1.46
test/programs/benchmarks/product-lines/	status	cputime (s)	walltime (s)	memUsage	host	k	BMC formula creation (s)	SMT check (s)	Bounds check (s)	status	cputime (s)	walltime (s)	memUsage	host	k	BMC formula creation (s)	SMT check (s)	Invariant generation (s)	Bounds check (s)	Induction formula creation (s)	Induction check (s)	status	cputime (s)	walltime (s)	memUsage	host	Refinement (s)	Precision adjustment (s)	CPA algorithm (s)	Post operator (s)	Prec operator (s)	Abstraction (s)	Solving (s)	Model enumeration (s)	SMT without itp (s)	Boolean abstraction (s)	status	cputime (s)	walltime (s)	memUsage	host	Attempted forced coverings	Refinement (s)	Precision adjustment (s)	CPA algorithm (s)	Post operator (s)	Prec operator (s)	Abstraction (s)	Solving (s)	Model enumeration (s)	SMT without itp (s)	Forced covering (s)	Successful forced coverings	Boolean abstraction (s)
total tasks	597	291000	283000	1453467607040		90438	2830	32400	168000	597	167000	95600	1496831770624		1250	1240	392	10400	478	3530	4310	597	176000	168000	656674717696		4080	74100	77200	1490	73900	73800	4670	67600	72300	70500	597	139000	132000	733538619392		9562	15200	925	16200	1290	765	733	353	293	1070	12800	1647	650
correct results	228	3960	2240	116006129664		849	578	25.1	64.9	457	29600	15000	537933135872		1224	1100	389	3370	475	3530	4310	426	16700	13300	245151154176		1560	8530	9970	679	8410	8380	1400	6670	8070	7580	438	13600	10300	245715308544		1893	2830	767	5580	783	661	641	303	260	668	3350	499	567
correct true	94	2060	1100	53746565120		618	387	16.3	60.6	323	22300	11300	400274239488		993	810	351	2490	453	2790	4080	305	10100	7910	156128415744		913	4960	5840	407	4890	4870	1010	3630	4640	4300	308	9160	7120	145485107200		1611	1950	457	4040	398	396	384	194	136	426	2810	420	334
correct false	134	1900	1130	62259564544		231	192	8.89	4.27	134	7260	3690	137658896384		231	292	37.3	884	22.4	738	227	121	6610	5440	89022738432		646	3560	4130	272	3520	3510	389	3040	3430	3280	130	4490	3180	100230201344		282	877	310	1550	386	266	257	109	124	242	541	79	233
incorrect results	0									0												0															0
incorrect true	0									0												0															0
incorrect false	0									0												0															0
score (597 tasks, max score: 929)	322									780												731															746
Run set	bmc-bitprecise.BMC.ProductLines									k-induction-bitprecise.k-Induction.ProductLines												predicateAnalysis-bitprecise.PredicateAbstraction.ProductLines															impact-bitprecise.Impact.ProductLines